This post is an attempt to explain in simple terms how to interpret claims of the form “this theorem is correct because it was checked in Lean”. The summary is: there is an important signal that can be extracted from Lean code, but if this code is AI-generated then you need to do some tests first. We explain the tests, and note that in many cases (such as the OpenAI theorem dump) these tests have not yet been systematically done.
[...]
It is worth noting that of the 290 OpenAI theorems which come with Lean code, around 38 of them have the property that the Lean code does not even state, let alone prove, the main theorem of the paper. And OpenAI never claimed that it did! They just said “here is some Lean code which goes with this paper”. Sometimes the code just states and proves some intermediate results — my impression is that OpenAI decided to go live when some of the formalizations were incomplete, so just dumped what they had. To give a concrete example: paper 194 claims to prove Lech’s multiplicity conjecture in commutative algebra, with no restriction on dimension, residue field or characteristic; this question has been open since 1960. The headline theorem in the corresponding Lean code can be checked to be Corollary 5.4 of the paper — already an impressive achievement, but not the headline result.
[...]
When Anthropic formalized a proof of Fermat’s Last Theorem in Lean, they asked me to take a look at the 13 million lines of code which they had generated. I downloaded it onto my machine, dumped it into a sandbox (because who knows what AI-generated code will do, it can in theory delete all your files) and attempted to compile it; I very quickly ran out of memory. I told Anthropic that I was unable to make any claims about what they had done until I could see the code base compiling, and they gave me temporary access to a machine with 96 cores and 500 gigs of ram. I could then compile the code.
Of course, with a more reasonably-sized codebase it is possible to compile the code on a reasonably-sized machine. For example OpenAI’s resolution of the Navier-Stokes problem is 640K lines of code and compiles fine on my laptop.
[...]
Even if the Lean code compiles and passes all these tests, and is thus overwhelmingly likely to be a correct proof of a theorem, this does not mean that any corresponding pdf also contains a correct proof! The Navier–Stokes lost in translation paper demonstrates the opposite in fact, for the Navier-Stokes write-up; whilst all the tests above have been run for the Navier–Stokes work, there are instances where the pdf proof and the Lean proof diverge. In these cases, who knows if the pdf proof is OK! My understanding is that some experts have been using AI to informalise the Lean proof back into English in order to read the argument, rather than ploughing through the slop in the pdf.
[...]
“It’s true because it’s checked in Lean” can be made to make sense. But one has to do some work beyond “the Lean code compiles”. Your frontier AI model can do all of this work. But it needs to be done, and (depending on the amount of Lean code in the proof) it may be computationally costly.
From the article:
[...]
[...]
[...]
[...]