Comment by mlmonkey
17 hours ago
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?
Proof and program are twins. Formalized theorems can be incompatible for exactly the same reasons that programming APIs can be incompatible.
What were the agents based on?
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.
[flagged]
Producing a formalized proof from a non-formalized proof in a paper or book should not be considered a violation of copyright.
1 reply →
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.
> Of course you can include two or five or ten equivalent formulations (like textbooks sometimes do) but still, not everything under the sun.
Note that mathlib currently includes duplicates of many theorems; I believe deduplication is an active goal (if not one seeing much labor right now).
Yes and no. With enough compute, probably, but doing this does not necessarily yield a reusable library. See https://xenaproject.wordpress.com/2026/10/16/how-to-formaliz...
_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.
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.
[dead]