#formalization — Public Fediverse posts
Live and recent posts from across the Fediverse tagged #formalization, aggregated by home.social.
-
Just dropped two new papers into the arxiv:
https://arxiv.org/abs/2607.12461
http://arxiv.org/abs/2607.17421
This caps off an extraordinary arc, the true seed of which was harshly interrupted by Covid, curling over multiple personal life changes, ending during a dawn in the dominance of AI-augmented mathematics.
Aside from the significant progress on one of my personal favourites ---indeed a *classic* Erdos problem--- what might be of wider interest is our use of (semiautomatically generated) Lean to corroborate the fidelity of computationally-aided proof methods (in this case, a nontrivial variant of flag algebras).
Oh, and let me extend my congratulations to all the Eoins.
#eoins #combinatorics #generativeAI #formalization #semiautomatic #lean #covid
-
Just dropped two new papers into the arxiv:
https://arxiv.org/abs/2607.12461
http://arxiv.org/abs/2607.17421
This caps off an extraordinary arc, the true seed of which was harshly interrupted by Covid, curling over multiple personal life changes, ending during a dawn in the dominance of AI-augmented mathematics.
Aside from the significant progress on one of my personal favourites ---indeed a *classic* Erdos problem--- what might be of wider interest is our use of (semiautomatically generated) Lean to corroborate the fidelity of computationally-aided proof methods (in this case, a nontrivial variant of flag algebras).
Oh, and let me extend my congratulations to all the Eoins.
#eoins #combinatorics #generativeAI #formalization #semiautomatic #lean #covid
-
The past two months, I helped coordinate the "Phase Transitions..." research semester programme at CWI (https://www.cwi.nl/en/events/research-semester-programmes/phasecap-phase-transitions-in-combinatorics-algorithms-probability/). It ended last Friday, and still I feel "hungover" from the intensive blur of activities/developments/ideas. Very grateful to my team --Feri, Jop, Serte, Carla, Noela, Guus-- we did it!
In parallel, during the same two months, after the dawn of recognition of what has arrived (after a tip from Jeroen), I underwent a kind of phase transition myself. Avowed refusenik in March (see https://mathstodon.xyz/@kangmeister/115252549665766971); an "anti-Gemini" research working group in April; compulsive button-pressing in May. (And yes, I *know* it is easy to set it up for pressing fewer buttons...)
That poetic part of me (or whatever remains of it) is allured by the term, "cognitive surrender", if only to help in my search for the right words to describe the sharp changes underway in various facets of mathematical life/growth.
#CWI #combinatorics #algorithms #probability #conferences #generativeAI #formalization #lean #scientificpublishing
-
The past two months, I helped coordinate the "Phase Transitions..." research semester programme at CWI (https://www.cwi.nl/en/events/research-semester-programmes/phasecap-phase-transitions-in-combinatorics-algorithms-probability/). It ended last Friday, and still I feel "hungover" from the intensive blur of activities/developments/ideas. Very grateful to my team --Feri, Jop, Serte, Carla, Noela, Guus-- we did it!
In parallel, during the same two months, after the dawn of recognition of what has arrived (after a tip from Jeroen), I underwent a kind of phase transition myself. Avowed refusenik in March (see https://mathstodon.xyz/@kangmeister/115252549665766971); an "anti-Gemini" research working group in April; compulsive button-pressing in May. (And yes, I *know* it is easy to set it up for pressing fewer buttons...)
That poetic part of me (or whatever remains of it) is allured by the term, "cognitive surrender", if only to help in my search for the right words to describe the sharp changes underway in various facets of mathematical life/growth.
#CWI #combinatorics #algorithms #probability #conferences #generativeAI #formalization #lean #scientificpublishing
-
Half a year ago, I filled in some sorry's for the massive project [1] to formalize the Fields-medal winning proof that sphere packing in dimension 8 is optimized by the E8-lattice. Last week it was announced that all remaining sorry's were filled by Gauss, an autoformalization agent. Gauss was able to build on the blueprint and other scaffolding built by the community. A few days later, Gauss also formalized the proof in dimension 24, this time working directly from the published paper, without mayor community input [3].
Since Lean verifies the generated proofs, hallucinations are not a problem.
The community now processes the generated proofs to make sure it satisfies the community standards and remains usable in the future [2].[1] https://thefundamentaltheor3m.github.io/Sphere-Packing-Lean/
-
Half a year ago, I filled in some sorry's for the massive project [1] to formalize the Fields-medal winning proof that sphere packing in dimension 8 is optimized by the E8-lattice. Last week it was announced that all remaining sorry's were filled by Gauss, an autoformalization agent. Gauss was able to build on the blueprint and other scaffolding built by the community. A few days later, Gauss also formalized the proof in dimension 24, this time working directly from the published paper, without mayor community input [3].
Since Lean verifies the generated proofs, hallucinations are not a problem.
The community now processes the generated proofs to make sure it satisfies the community standards and remains usable in the future [2].[1] https://thefundamentaltheor3m.github.io/Sphere-Packing-Lean/
-
The formal specification. This paper develops the mathematical operators for multi-scale recursive dynamics—connecting quantum, neural, and cosmic domains through a unified formalism.
https://doi.org/10.5281/zenodo.15784341
#Mathematics #CrossScale #Formalization -
The formal specification. This paper develops the mathematical operators for multi-scale recursive dynamics—connecting quantum, neural, and cosmic domains through a unified formalism.
https://doi.org/10.5281/zenodo.15784341
#Mathematics #CrossScale #Formalization -
We're working on a tool for standardizing hypothesis formulation. We've put together a bibliography of previous work on the topic. Are we missing any important papers?
Feel free to edit or comment: https://docs.google.com/document/d/1fJeVJZaX1v8Cmw8ibDzq0WtUolSQ8ZcPyg-kafFQEf8/edit?usp=sharing
#hypothesis #HypothesisStandardization #hypothesizer #formalization #NHST #TheoryDevelopment #OpenScience @openscience
-
We're working on a tool for standardizing hypothesis formulation. We've put together a bibliography of previous work on the topic. Are we missing any important papers?
Feel free to edit or comment: https://docs.google.com/document/d/1fJeVJZaX1v8Cmw8ibDzq0WtUolSQ8ZcPyg-kafFQEf8/edit?usp=sharing
#hypothesis #HypothesisStandardization #hypothesizer #formalization #NHST #TheoryDevelopment #OpenScience @openscience
-
Robert Rosen's approach of grounding formalization in science in the ultimate formalization, math, is as self-similar as thinking about thought.
His use of "category theory" provides a mathematical analogy to analogies.
I must confess that I need a lot of time to understand his writings - I keep learning new things every time I read it again.
-
Robert Rosen's approach of grounding formalization in science in the ultimate formalization, math, is as self-similar as thinking about thought.
His use of "category theory" provides a mathematical analogy to analogies.
I must confess that I need a lot of time to understand his writings - I keep learning new things every time I read it again.
-
I'm happy to report that my expository note (https://arxiv.org/abs/2408.11501), which has previously been kindly mentioned on here by @ecavallo and @jonmsterling, has been accepted to the TYPES 2024 post-proceedings 🙂
-
I'm happy to report that my expository note (https://arxiv.org/abs/2408.11501), which has previously been kindly mentioned on here by @ecavallo and @jonmsterling, has been accepted to the TYPES 2024 post-proceedings 🙂
-
Call for Papers
16th International Conference on Interactive Theorem Proving — ITP'25Reykjavik, Iceland
27 September – 3 October 2025https://icetcs.github.io/frocos-itp-tableaux25/itp/
ITP is concerned with all aspects of interactive theorem proving, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and the formalization of mathematics.
- Abstract submission deadline: 12 March 2025
- Paper submission deadline: 19 March 2025
- Author notification: 23 May 2025
- Camera-ready copy due: 27 June 2025#formalization #theoremproving #proofassistants #verification #CfP
-
Call for Papers
16th International Conference on Interactive Theorem Proving — ITP'25Reykjavik, Iceland
27 September – 3 October 2025https://icetcs.github.io/frocos-itp-tableaux25/itp/
ITP is concerned with all aspects of interactive theorem proving, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and the formalization of mathematics.
- Abstract submission deadline: 12 March 2025
- Paper submission deadline: 19 March 2025
- Author notification: 23 May 2025
- Camera-ready copy due: 27 June 2025#formalization #theoremproving #proofassistants #verification #CfP
-
I’ve been thinking about formalization of maths a bit and for what I usually do in algebra and combinatorics this all seems rather straightforward albeit time consuming.
But then I’m reading a topology book where the proofs go like: Imagine a 4d-ball of clay where push your finger in to form 3 openings with this and that property and then identify the 3d-boundary of the inside of hole 1 with …
Will it be possible to formalize this? Will we discover many errors?
-
I’ve been thinking about formalization of maths a bit and for what I usually do in algebra and combinatorics this all seems rather straightforward albeit time consuming.
But then I’m reading a topology book where the proofs go like: Imagine a 4d-ball of clay where push your finger in to form 3 openings with this and that property and then identify the 3d-boundary of the inside of hole 1 with …
Will it be possible to formalize this? Will we discover many errors?
-
Last Thursday I learned a bit of Lean4 from @MoritzFirsching and now the fortune cookie says “you have bet on the right horse”. 😳
Coincidence?
I think yes.
-
@janhoglund Anything that requires a reasoning subject (e.g., synthetic reasoning, any target oriented usage of analogies) is out of scope for #formalization (i.e., a #mechanism - no new #knowledge without the re-appraisal of believes in the light of new evidence (i.e, #abduction or #retroduction. Without "sociology of knowledge" the very idea of "objectivity of knowledge", in the Popperian sense, doesn't work (e.g., #Haack S. "Epistemology with a knowing subject." 1979). #philosophy #ai
-
@janhoglund Anything that requires a reasoning subject (e.g., synthetic reasoning, any target oriented usage of analogies) is out of scope for #formalization (i.e., a #mechanism - no new #knowledge without the re-appraisal of believes in the light of new evidence (i.e, #abduction or #retroduction. Without "sociology of knowledge" the very idea of "objectivity of knowledge", in the Popperian sense, doesn't work (e.g., #Haack S. "Epistemology with a knowing subject." 1979). #philosophy #ai
-
@corbden So, this whole complex of ideas (#philosophy)a is connected to (among others) the concepts of #incompleteness (#Gödel #Goedel), #creativity #cognition #psychology #aesthetics #pedagogy #learning #AI #AGI and the limits of #algorithms and #formalization.
There are known instances of physical entities for which it can be shown that they are not computable. I think human beings are like that and AGIs must be like that. The limits of the Turing-computable are not the limits of the possible.
