Researcher describes use of swarm of AI agents to assemble formalization from 500+ sources
2 Oct 27 12:55 PM · 11d ago · 10 comments · 1 source · development 2 of 2
Jonath Laurent from Axiom MTS explains that the formalization was approached using agents tasked with processing sources scattered across more than 500 articles and books. A key challenge was assembling everything into a coherent whole, since the same informal concept can be formalized in slightly different but incompatible ways.
“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.”
jonath_laurentDean Cureton Core contributor to Lean formalizationVasily Ilin Core contributor to Lean formalizationBhavik Mehta Core contributor to Lean formalizationNiels Voss Core contributor to Lean formalizationAxiom MTS Organization leading the formalization project
The whole story articlespostscomments the bright band is this development · numbered dots are the others · click one to jump
What people said 15 voices · verbatim
-
we are moving forward steadily :) https://github.com/marcinjangrzybowski/cubical-bis/blob/inte... (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…
-
_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 (https://en.wikipedia.org/wiki/General_Problem_Solver).LLMs can do smarter searches, and will likely find proofs for most of them, but are not guaranteed to find a proof.
-
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…
-
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.One challenge is assembling everything into a coherent whole, since the same informal concept can be formalised in slightly different but…
-
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.Probably this will be done in some form in the coming…
-
Yes and no. With enough compute, probably, but doing this does not necessarily yield a reusable library. See
-
Somehow the classification of finite simple groups makes me feel uneasy as a mathematician, but I suppose this helps quell that feeling.
-
This is phenomenal, super important for me. I have always had my concerns about the classification, and the verification that such a monumental proof is correct gives me great confidence about the way we have been doing mathematics so far.
-
I’m not sure what axiom maths business model is, seems like excesses of AI boom era.No one’s gonna care for formalizing a 10,000 page math proof with 46M lines of Lean code, unless it is very cheap to do, which seems unlikely.
-
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.
-
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.
-
Simplifying and composing these proofs with other proofs should probably be the next goal. And formalizing within other computational proof paradigms.
-
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.
-
Note they found one gap (and filled it) in the previously accepted 1,000+ page proof. So that's pretty cool.
-
The stronger AI become the easier it should be to develop and move to alternative foundations.
All 2 developments of Finite Simple Groups Classification Formalized in Lean… →
Hacker NewsNewswiresMastodon