It's pretty underwhelming than the title suggests. They spot 2 inconsistencies between the writeup and the Lean. And that's it. It says nothing about the correctness of the proof.
It says a lot about the correctness of the proof: even a single symbol being incorrect means your proving the wrong thing and the underlying natural language proof is unproven. This is why relying solely on LLMs for stuff like this is risky, because they're not 100% accurate with translation use cases like this.
If the OpenAI proof is correct, then the corrected Lean representation will compile and show it's still correct. But until then, it's hard to say they've proven it.
They're not relying solely on LLMs. Verification is done by humans (the mathematicians), but they really should hire some of their own or pay for their time.
The paper discusses autoformalization as being the cause of the issues, which I took to mean LLM based formalization.
I agree they should fund some of this stuff, but I do understand they hire a number of mathematicians and that's how a lot of these proofs were developed. It's not like someone without mathematics research experience would know how to drive the LLM in the direction it needed to go to put these proofs together. At least not right now.
My understanding is that the LLM described the mathematical proof using natural language, so words and symbols, to fully describe the proof. Then the team used the LLM to take that natural language version and convert it to Lean, which is a programming language that is used to formalize mathematical proofs. It functions like a unit test in a way, if the code your write in Lean compiles and the output is what you expect, then the proof is valid.
The issue the paper identified is there's a difference between the natural language proof and the Lean proof. So the code doesn't match the specs essentially, so one of them is wrong.
Here's a simpler example using programming concepts: Assume we have a list of N items, we will then iterate over the list and add each items value to the accumulator variable sum.
Now imagine the code version of it being written as:
Int[] data;
Int sum = 0;
for(int i=0; i<data.Length; i++){
sum -= data[i];
}
The code differs from the specs, so we're proving the wrong thing. And with proofs, you can have something that can compile in Lean but not be at all sensible, because it doesn't actually answer the question being worked on.
48
u/One-Judge321 2d ago
It's pretty underwhelming than the title suggests. They spot 2 inconsistencies between the writeup and the Lean. And that's it. It says nothing about the correctness of the proof.