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.
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.
One challenge is assembling everything into a coherent whole, since the same informal concept can be formalised in slightly different but incompatible ways.
As someone with a highly uneven and kinda basic maths background, I'd have thought that simplification of a proof, and pulling things into a coherent whole would be exactly what computers excel at, but everything I've seen (or heard) suggests that's not really the case. Are you able to explain why?
When two sources formalized the same object in incompatible ways, did the swarm mostly emit translation lemmas between them, or did someone pick a canonical definition and have downstream proofs rewritten to match? The second feels like where the "coherent whole" cost actually sits, and I'm curious how much of the 500-source effort was that reconciliation versus line-by-line translation.
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 months.
The really interesting aspect of this, IMHO, is discovering what theorem formulations combine together well as a whole. It's much akin to a software architecture problem.
Metamath has done quite a bit or primary research into this. Theorems often have a slightly non-standard, but more general form.
One can ask things like, "what is the equivalent of functional programming?" Or, "is there global state?" It's a perspective on reverse mathematics.
_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.
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.
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.
They didn't discover a missing sporadic group. The big gap in the proof (the quasithin case) happened because it was covered in a 600-page unpublished manuscript that under further investigation turned out to be incomplete.
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.
Last week I blew my whole Claude Max weekly budget having Opus translate from Mathlib to Coq-HoTT. It was so beautiful I can't wait to do it again this week.
No Type Theory won: Per Martin-Löf is still alive and should be able to confirm his work lives in some form in Lean. Zermelo and Fraenkel would be utterly confused, however.
What you mean it say is that Lean is not a HoTT, and Mathlib has tons of classical reasoning (excluded middle, axiom of choice).
I don't think it's too late at all for HoTT. In fact, I think the AI companies will find trying to crank out more new math which is out of distribution in a funky way a highly useful exercise.
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
Well, the point of the _computer_ formalization is that it's checkable.
An error in the formalization would be a bug in lean. Which, as we know, certainly seems plausible (I've mused on if these giant proofs are incentivizing LLMs to find lean bugs to exploit), but at least it's a smaller surface area.
In general checking that the definitions are correct isn't that hard and assuming at least one of the lean kernels you verify with is correct (which tbf is an assumption, the implementations are based on each other so could have a common bug) that's all you need to verify.
In this case the statement is unusually complicated but still much much easier to verify than the proof itself.
The papers describing lean and it's core operations are deliberately small. The kernel of a theorem prover is meant to be such that a human can check it for correctness. The kernel does not include things like type inference or execution. It literally checks the proof and that's all and everything needs to match exactly. It's fairly trivial to write such a thing.
Humans have to establish trust in this.
After that, the rest of the language is written. Yes it is possible the type inference engine is broken but in that case the kernel will reject it
Depends if you include a few decades of improvements in lean itself. Non-AI proof automation is much better than it was even a year ago and so some fiddly results can now be done with `by grind`.
Also don't discount the fact that people would learn how to do this kind of project, currently no one really knows how to decide what definitions work best, what should be reducible, what should be part of a public api and what should be local to a module, etc.
I would bet no. Because the original proof is so distributed, with parts of it being very old, and with parts of it being, as a first attempt, not the most concise or lucid route to the result, we were rapidly approaching a world where the empirical knowledge of how/why the result holds was literally dying.
The article refers to its use of the "first-generation proof". It would seem this proof is too large to be truly known by one person, and the group of people who "collectively knew" it grew old and started to die. Since its original formulation, mathematicians began to compile, consolidate, and revise the proof into a 2nd generation digested form (estimated to be 5000 pages instead of tens of thousands). But that effort was still so monumental in its own right that a 3rd gen proof project began to digest the 2nd gen proof before the 2nd gen proof was even finished. I believe both the 2nd and 3rd gen projects are still ongoing.
It will be interesting to see how small the proof gets once we finish learning how to obtain these results "efficiently" with the benefit of hindsight.
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.
>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.
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.
Maybe my understanding of Lean is wrong; I'm thinking of it as a programming language but for Math.
One challenge is assembling everything into a coherent whole, since the same informal concept can be formalised in slightly different but incompatible ways.
Probably this will be done in some form in the coming months.
Metamath has done quite a bit or primary research into this. Theorems often have a slightly non-standard, but more general form.
One can ask things like, "what is the equivalent of functional programming?" Or, "is there global state?" It's a perspective on reverse mathematics.
Note that mathlib currently includes duplicates of many theorems; I believe deduplication is an active goal (if not one seeing much labor right now).
LLMs can do smarter searches, and will likely find proofs for most of them, but are not guaranteed to find a proof.
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.
What you mean it say is that Lean is not a HoTT, and Mathlib has tons of classical reasoning (excluded middle, axiom of choice).
I don't think it's too late at all for HoTT. In fact, I think the AI companies will find trying to crank out more new math which is out of distribution in a funky way a highly useful exercise.
An error in the formalization would be a bug in lean. Which, as we know, certainly seems plausible (I've mused on if these giant proofs are incentivizing LLMs to find lean bugs to exploit), but at least it's a smaller surface area.
In this case the statement is unusually complicated but still much much easier to verify than the proof itself.
Humans have to establish trust in this.
After that, the rest of the language is written. Yes it is possible the type inference engine is broken but in that case the kernel will reject it
Also don't discount the fact that people would learn how to do this kind of project, currently no one really knows how to decide what definitions work best, what should be reducible, what should be part of a public api and what should be local to a module, etc.
The article refers to its use of the "first-generation proof". It would seem this proof is too large to be truly known by one person, and the group of people who "collectively knew" it grew old and started to die. Since its original formulation, mathematicians began to compile, consolidate, and revise the proof into a 2nd generation digested form (estimated to be 5000 pages instead of tens of thousands). But that effort was still so monumental in its own right that a 3rd gen proof project began to digest the 2nd gen proof before the 2nd gen proof was even finished. I believe both the 2nd and 3rd gen projects are still ongoing.
It will be interesting to see how small the proof gets once we finish learning how to obtain these results "efficiently" with the benefit of hindsight.
https://en.wikipedia.org/wiki/Monster_group
>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.
[1]https://axiommath.ai/research/the-enormous-theorem-formalize...