Makes me sad that the homotopical foundation people never got their shit together and now formalization is so mature but it's still done in set theoretic foundations.
we are moving forward steadily :)
<a href="https://github.com/marcinjangrzybowski/cubical-bis/blob/integrate-lorenzo-premetric-fast-rationals/Cubical/AnalysisC/SCOPE_ROADMAP.md" rel="nofollow">https://github.com/marcinjangrzybowski/cubical-bis/blob/inte...</a>
(see table in the middle of doc)
mind, that it is fully constructive implementation, you can get arbitrary precision aproximation to every real expression.
for now WIP, but soon will be aviable in cubical-library :)
also our related TYPES2026 presentation: <a href="https://types2026.cse.chalmers.se/slides/51.pdf" rel="nofollow">https://types2026.cse.chalmers.se/slides/51.pdf</a>
The stronger AI become the easier it should be to develop and move to alternative foundations.
Out of curiosity: is it possible to take a frontier model and just let it loose on all math textbooks out there, converting each and every proof/theorem/lemma/etc. into Lean? A frontier model should be able to do that, right? And it's a one-time task: do it once and it's there for eternity, available as a library to be used in other proofs.<p>Maybe my understanding of Lean is wrong; I'm thinking of it as a programming language but for Math.
Axiom MTS here. What you describe is pretty close to how we formalised this proof, which is scattered across more than 500 articles and books: a swarm of agents was tasked with going through all these sources.<p>One challenge is assembling everything into a coherent whole, since the same informal concept can be formalised in slightly different but incompatible ways.
Yes, but thing is, for a lot of basic stuff there are myriad ways in which it is formulated, so humans have to decide which of them goes in the library. Of course you can include two or five or ten equivalent formulations (like textbooks sometimes do) but still, not everything under the sun.<p>Probably this will be done in some form in the coming months.
Yes and no. With enough compute, probably, but doing this does not necessarily yield a reusable library. See <a href="https://xenaproject.wordpress.com/2026/10/16/how-to-formalize-all-of-mathematics/" rel="nofollow">https://xenaproject.wordpress.com/2026/10/16/how-to-formaliz...</a>
_If_ you have formalized a provable theorem in Lean, a simple bread-first search can prove it. It will take lots (and lots, and lots, and lots…) of time, though (<a href="https://en.wikipedia.org/wiki/General_Problem_Solver" rel="nofollow">https://en.wikipedia.org/wiki/General_Problem_Solver</a>).<p>LLMs can do smarter searches, and will likely find proofs for most of them, but are not guaranteed to find a proof.
Write a few proofs with it and then come back to this
I think people assume that it would end up not being usable by humans without a lot of hand-holding. Though maybe that's wrong, and somebody should try it.
This seems like a very good use of auto-formalization, because in the past mathematicians have incorrectly believed that they were finished with the classification only discover a missing class/sporadic group.<p>The original proof was a collaboration of ~100 mathematicians, if Tao is correct then we should expect to see more such collaborations in the future like we do in e.g. physics.
Groups were my gateway drug into abstract algebra. A friend clued me into symmetry being everywhere and Groups are how symmetry is formalized, and it’s been a crazy journey understanding all that. The frontier models can tie those abstract concepts to plain English examples and answer questions decently well, it’s never been a better time to pick up the field solo and see what it has to offer us
Note they found one gap (and filled it) in the previously accepted 1,000+ page proof. So that's pretty cool.
Somehow the classification of finite simple groups makes me feel uneasy as a mathematician, but I suppose this helps quell that feeling.<p><a href="https://en.wikipedia.org/wiki/Monster_group" rel="nofollow">https://en.wikipedia.org/wiki/Monster_group</a>
The formalization is 43.1M lines of Lean.
Filling in well-known gaps like this is the kind of thing the AI companies should be doing, not trying to scoop research in progress.
LLM formalization is not as useful as human formalization, but nice to know that the Classification is correct
Page has some kind of redirect bug that steals the back button, may want to open it in a new tab to avoid that.
I'm surprised they only found one gap. I would have expected multiple (fixable) gaps would have been uncovered, especially since the result was spread over many papers by many different people.
In [1] they claim:<p>>However, there were 34 noteworthy deviations from the published record that needed to be resolved, the most substantial of which related to the Unbalanced Group Theorem.<p>[1]<a href="https://axiommath.ai/research/the-enormous-theorem-formalized/" rel="nofollow">https://axiommath.ai/research/the-enormous-theorem-formalize...</a>
Many many gaps had been found and patched (by humans) already over the last forty years.
Looking at the visualizations made me wonder if the embeddings themselves can be used to suggest, if not derive, mathematical results. I realize it depends on the quality of the embeddings.
[flagged]
based if true