From the paper: "A third possibility is that the NL proof provides stronger statements than what the formal proof actually establishes, with (of course) different proofs. The latter happens in OpenAI’s announced proof of blow-up of Navier Stokes equations."
What the examples seem to show is that the proof method is different between the natural language proof and the lean proof. Which, if the lean proof actually proves blowup, would suggest that the natural language proof is subtly wrong, but the strategy was close enough to be used to create a real lean proof.
A little worrying, but part of the purpose of formalizing things in Lean, it forces you to be more accurate than natural language does. It's surprisingly common for major theorems to have slight inaccuracies early on that can be repaired. Famously, the initial proof of Fermat's Last Theorem had a flaw that took a year to repair (though I think that's unusually difficult).
So the most fundamental question is: does the Lean theorem faithfully state the right theorem?
For what it's worth the initial lean specifications for the top-level theorems generally come from human written formalizations such as in https://github.com/leanprover-community/mathlib4/blob/021ce6... so we can be reasonably confident about their correctness.
No, the other way around. The natural language proof was derived from the lean code, badly. This is my experience with using claude and lean to prove things. Its natural language explanations drift a lot from the lean, both before and after. But the lean code is the lean code.
Was it? Are you claiming a LLM does reasoning in lean or what? Since this (and all the other proofs by OpenAI etc) have been in the reverse order [1]:
> The agents arrived at their resolution on Saturday, September 5, about 88 hours after the first agents were launched. Lean formalization and verification took an additional 17 hours via GPT‑6 Astra.
That is definitely interesting because how do you know the 88 hours of work are correct before you throw another 17 hours of lean formalization work on it? You could end up just finding out there was some hallucination in the original work.
If your code compiles, are you sure it's bug free?
Need to prove a forall statement? forall x, P(x) is the same as a function taking x and returning the proof that P(x) is true.
Need to prove an exists statement? Create the pair (x, h) that gives the actual x that proves the exists, along with a proof that it satisfies the property you claim.
Maybe the only weird thing is that there are types and sets, so sets are kind of automatically more of a "subset" of some type.
The actual Mathlib is more generic, but once you get a hang of writing definitions (as you do in intro proofs), I've found that you can pretty naturally translate whatever you'd have in your undergrad notes. And undergrad should cover defining integers, rationals, reals, relations, functions, sequences, limits, derivatives, integrals, etc. Even if they've never studied solving PDEs, they'd have to take multivariable calculus and know enough to be able to write one (assuming they take at least single variable analysis+linear algebra)?
The proofs can get involved and tedious with all of the extra bookkeeping, or techniques to try to reduce the bookkeeping (tactics, etc). But the definitions and statements are pretty much what you'd expect.
Humans have made similar mistakes too. A human writes a specification for how things should work, the human translates that into code, the code does not work, and finally the human fixes the code and forgets to fix the original spec.
So the Lean proves something and the question is whether that something is actually what we care about — or something similar, but ultimately not the question.