Posting the paper itself as it's more direct and substantial, but there's also a good Bluesky thread here that seems to summarize the key ideas. I recommend reading the whole thread, but here's the key bits:
The actual math in this paper is over the heads of non-mathematicians but the core argument is pretty easy to follow: AI theorem-prover formalizations can't actually be trusted to faithfully be the same argument as the natural-language paper they come attached to
the way openAI slopmath paper spam works is that each paper really comes as two things. one is the actual paper, which is an argument in English intended for humans (and LLMs) to read. the other is a "formalization", source code for a specialized programming language (Lean) that proves theorems.
It's generally accepted that if Lean code compiles, then the theorem that the code implements must be true. But the problem there is that there's no way to actually guarantee that a given pile of Lean code really is the same thing as the NL argument being made in a given paper.
The paper argues that this is literally undecidable: "Informally, providing semantically faithful AI autoformalisation is harder than any computational problem including the Halting problem." The only way to be sure is extensive manual checking.
Some of these Lean proofs are millions of lines long. So what OpenAI is doing is presenting a "result" that may or may not be the same as a huge git repo of Lean files. The paper demonstrates examples of incorrect proofs being "translated" into correct Lean by GPT!
Obviously this is over my head, but there are some blunt claims in this Twitter thread by Elliot Glazer, a mathematician and expert at formalization, that this doesn't affect whether the proof is right:
This Navier-Stokes mistranslation thing is a nothingburger. Like 5 of you are making a nuanced (frankly pedantic) point about readability issues that are being phrased in a way that sounds to non-math ppl like there are serious doubts the proof is correct. There is no such doubt.
...
They're the same proof. The disagreements between them are smaller than a typical pair of human presentations of the same proof.
...
If OpenAI presented its autoformalizer a wrong proof of Navier-Stokes, it would not have successfully formalized it. The proof is right and nearly identical to the Lean conversion.
So it sounds like his argument that there is no need to verify that the natural language proof and the formalized Lean proof are the same thing because... reasons?
It makes no sense to me. What even is the purpose of the formalized Lean proof if the natural language proof is already enough to solve the problem without the extra step of verifying that the formalized proof is actually a valid representation of it?
I'm not a mathematician, but I think they do check that the Lean proof is proving the correct problem, and the rest gets verified automatically. This is a lot easier than reviewing the entire proof. So that shows that it's true.
For the natural language proof, it's a bit odd that mathematicians can be somewhat casual about it, but my impression is that it's sort of like how you wouldn't consider a spelling error to invalidate someone's entire argument, provided that you otherwise understand the argument. It's assumed that minor mistakes can be corrected by the reader and are unlikely to make the proof invalid. Also, maybe it's okay if some statements in the proof are proven in a slightly different way? The goal is to understand the journey well enough to get to the same place, rather than to repeat the journey exactly.
The linked paper has concrete demonstrations of incorrect proofs that got mistranslated into compiling Lean proofs, to show that a compiling Lean proof doesn't necessarily imply that the thing the LLM is claiming to prove has actually been proven. And the fact that these concrete examples exist seems to contradict the tweet you linked where the guy seems to be implying that's not a thing that can happen and it's all a nothingburger.
[OP] LukeZaz | a day ago
Posting the paper itself as it's more direct and substantial, but there's also a good Bluesky thread here that seems to summarize the key ideas. I recommend reading the whole thread, but here's the key bits:
skybrian | 19 hours ago
Obviously this is over my head, but there are some blunt claims in this Twitter thread by Elliot Glazer, a mathematician and expert at formalization, that this doesn't affect whether the proof is right:
...
...
Rudism | 5 hours ago
So it sounds like his argument that there is no need to verify that the natural language proof and the formalized Lean proof are the same thing because... reasons?
It makes no sense to me. What even is the purpose of the formalized Lean proof if the natural language proof is already enough to solve the problem without the extra step of verifying that the formalized proof is actually a valid representation of it?
skybrian | 2 hours ago
I'm not a mathematician, but I think they do check that the Lean proof is proving the correct problem, and the rest gets verified automatically. This is a lot easier than reviewing the entire proof. So that shows that it's true.
For the natural language proof, it's a bit odd that mathematicians can be somewhat casual about it, but my impression is that it's sort of like how you wouldn't consider a spelling error to invalidate someone's entire argument, provided that you otherwise understand the argument. It's assumed that minor mistakes can be corrected by the reader and are unlikely to make the proof invalid. Also, maybe it's okay if some statements in the proof are proven in a slightly different way? The goal is to understand the journey well enough to get to the same place, rather than to repeat the journey exactly.
Rudism | an hour ago
The linked paper has concrete demonstrations of incorrect proofs that got mistranslated into compiling Lean proofs, to show that a compiling Lean proof doesn't necessarily imply that the thing the LLM is claiming to prove has actually been proven. And the fact that these concrete examples exist seems to contradict the tweet you linked where the guy seems to be implying that's not a thing that can happen and it's all a nothingburger.