Aside from the usual squabbling about AI, it seems the bombshell claim is this:
"In particular, we show that the formalised Lean proof does not correspond to the NL proof of blow-up of solutions to the Navier-Stokes equations."
So these authors seem to be claiming that OpenAI has not really proven Navier-Stokes at all. If I get their idea correctly, they are claiming that the LLM has not formalized the original "natural language" idea of Navier-Stokes correctly. If true, it would mean that their purported Lean proof is not actually a proof of Navier-Stokes at all, but something that is an incorrect translation of the original natural language idea. If correct, this is a really bold claim and I would like to see if other researchers agree.
No one is disputing that the Lean formaization of Navier-Stokes is correct, so we should have high confidence that the generated Lean proof is valid.
The authors are claiming that the Lean proof is not the same proof as the NL one. Therefore, we shouldn't yet have confidence that the NL proof is valid.
This is an important claim which the math community will need to work through. However, the Lean proof alone is sufficient for OpenAI to (reasonably confidently, leaving aside questions of academic manners) claim to have proven NS.
So, the AI wrote a NL proof of Navier-Stokes, then incorrectly auto-formalised it to Lean, but still ended up with a verifiable proof of Navier-Stokes? That seems... strange?
This same thing happened back in the 10 advances in math and CS release a month or two ago. The non sofic group construction relied on false prior literature. They realized this and fixed it in the lean program but didn't modify it in the writeup, so the written proof was both incorrect as stated and did not correspond to the lean proof. I was surprised how little press it got at the time, it seems like a huge risk factor.
I don't know if we can really be clear about the order of things, but I think even without AI maths is filled with "someone provides a proof of X, and the proof itself is wrong/incomplete but X itself is true".
"Incomplete" proofs might be a way of viewing this. You have a NL argument to prove X. It turns out the NL proof has holes you can drive a truck through. So... you go around and patch the holes.
The resulting proof is different! You can start off with a bad proof and find a correct proof. Sometimes.
EDIT: for French speakers (maybe autodub gets you there) I saw a very nice simple case of this recently. A commonly stated proof for a relatively simple theory. The proof has a giant hole in it, and completing it requires some work [0])
Or the AI wrote a NL proof of Navier-Stokes, began rewrite in Lean, then discovered a false / handwavy / easier to write in Lean / etc approach of some parts of the proof, and modified it accordingly. Since there wasn't any backpass from Lean to NL to include any changes it did due to any of the above reasons, the proofs aren't identical. That's what I think is most likely.
If the reason for the differences was done intentionally in Lean (as opposed to hallucinate e.g. m+4 vs m+5 as mentioned in remark 3.2), then a simple recording of differences, and then afterwards pass back any changes to the original NL would fix the issue. If it was hallucinated, then there is no guarantee it wouldn't keep hallucinating, and thus you might never end up with the same proof no matter how many passes you do back and forth (see remark 3.4).
It's not actually the same model that solved the problem that did the translation. Astra did the translation after the intenral model produced the NL Proof. As for the discrepancies, It's not necessarily right to think of this as 'incorrect formalisation'. Maybe it was essentially a 'proof refactoring'. Maybe Astra thought some parts could be easier expressed in a certain way, or maybe aspects of the NL proof were kind of handwavey etc.
Trying to map this observation to code and appreciate them starting with very simple examples (that Astra screw-fixed into lean.)
But in a simplified way this is close to promting the model to create a set with the members 1,2,1,5 and it correctly creates {1,2,5} in code. So The initial "proof" / instruction was wrong and it silently fixed that. ( Which is one of the failure modes they're describing)
I would expect it's the other way around. The AI wrote a Proof of NS in lean and write up a NL proof based on the lean one. The authors claim that openAI did NL -> Lean, but that is unsubstantiated.
> 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.
This seems pretty clear that they found the proof first and then mechanized it afterwards.
Or maybe the AI didn’t write Lean proof at all, or rather, not the LLM at least. But instead OpenAI has an internal traditional reinforcement model that is able to stumble on the Lean proof by the share amount of compute power available to them thousand monkeys on a thousand typewriter style. And then pretend LLM did it because that is what they are selling.
>No one is disputing that the Lean formaization of Navier-Stokes is correct, so we should have high confidence that the generated Lean proof is valid.
These authors don't seem to be disputing that this Lean formalization of Navier-Stokes is correct. I don't think that gives us any new information about whether the generated Lean proof is or isn't a valid proof of this N-S blowup thing.
The thing is that Navier-Stokes has a definition split off separate from the formalization, and that is what has been completed. People have looked at the definition of the final statement. This paper only mentions the proof and intermediate statement, not the final statement. The most likely case to me is that intermediate statements do not match, but the end result still holds.
Seems kinda odd then that it didn't occur to OpenAI to iterate until they reached a fixedpoint for both the informal & formal development b/c it's obvious that correspondence should have been part of their training pipeline.
Jesus Christ, so many people here who have no clue what they are talking about.
A proof of a theorem is different from the statement of the theorem. OpenAI has a Lean proof of the statement. That is all they need. There may be many different proofs of this statement, including NL proofs. It does not matter that these NL proofs may or may not be different from the Lean proof, at least for the correctness of the Lean proof. But of course the NL proof may be wrong. But who cares?
It reminds me of how provably secure software was all the rage for awhile. Until people found that the idealized system/lemmas were so far from reality that the proved security was worse than meaningless because it gave a false sense of security.
In order to prove security, you must first simulate the universe.
Why would they do that, knowing that the one known to be correct is the Lean one? Just to claim that the (correct) Lean proof did not translate well to English? That would be weak, and a colossal waste of energy and time.
> Jesus Christ, so many people here who have no clue what they are talking about.
Indeed. If only some of those people would see the irony.
What matters most of all, as any first year student of mathematics would know, is whether the formal problem statement corresponds to the NL statement. TFA specifically states that at least some of the allegedly proven formal statements DO NOT.
No. What the paper says is that in principle, translating NL statements to Lean statements is hard. Nobody doubts that, translating informal to formal text cannot be formally proven correct, so...
Does the paper give a single example of one of the OpenAI solved theorems with a Lean certificate where the Lean statement does not correspond to the actual statement from the mathematical literature? I don't think so, but in case I am wrong, feel free to provide that example.
If I understand the abstract correctly (big caveat), they aren't saying they didn't prove it. They're saying they gave two proofs, one in natural language and one in Lean, that are not equivalent to each other. I assume the main significance is that the Lean proof is not a formal verification of the natural language one and the natural language proof is not a readable explanation of the Lean one. Both of those things can be desirable, so to complete the set we'd get 4 proofs.
But just to clarify: is either of them actually addressing the real Navier-Stokes, or will it turn out we'll end up with two pairs of proofs about something irrelevant to the actual problem?
From computer science perspective the conclusion is obvious: untenable to have two representations without an exact translation or machine checked correspondence between then. All we have is a vibe translation using the LLM. The methodology should obviously be improved.
and clearly the computer science perspective is: get rid of the humans and express everything directly in lean so the computers can keep getting work done!
If I understand well, they mean that the thing they proved in lean is not Navier Stokes. And they don't make any statement about whether the natural language proof is correct or not.
I read them as making a much weaker claim than this: not that the Lean proof isn't valid, just that it is not actually a formalization of the natural-language proof in the PDF they provided alongside it. I haven't heard any PDE people claim that the Lean proof is invalid, and I have heard things from a lot of them that imply that they think it is valid. (I'm a former research mathematician, but this is very far from my specialty, so I'm not really equipped to evaluate this claim myself.)
The claim is about the equivalence between two proofs and says nothing about the correctness of either proof. This seems to be confusing a lot of people.
Navier-Stokes is an equation, not a theorem, so there is no such thing as "a proof of Navier-Stokes". The equation is a partial-differential-equation model of viscous fluid flow. Its correctness has never been in doubt: we know it cannot possibly be an exact description of real fluid flow, that it's a pretty good approximate description, and that there exist well-behaved solutions for a number of initial conditions.
What OpenAI purports to have proven, as I understand it, is that certain initial conditions to that equation, plus "forcing" over time (which could be a literal force acting on the fluid such as stirring it with a spoon or some other extrinsic effect) only have finite (and therefore physically plausible) solutions for a finite period of time, after which singularities appear, with the velocity or pressure of some of the fluid approaching infinity as you approach the finite time limit.
I think we can be pretty confident that the L∃∀N proof is really about Navier-Stokes. The question is whether what it says about Navier-Stokes is what we think it says.
NS is continuous approximation to what is otherwise a discrete system. Particle collisions are discrete time events that are averaged over time. NS loses accuracy for very, very, very very low fluid densities and energies.
AI "proving" that this approximation can numerically "blow" up does not mean the approximation loses validity.
If I'm understanding correctly, this is questioning the equivalence between the natural language proof and the lean proof, but not the correctness of the lean proof?
If the lean proof doesn't match the natural language one (which is the one the AI generated to solve the problem), it sounds like the lean proof isn't verifying the intended claim?
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."
The material is interesting, but unless the statement that is proved in lean is not blowup for Navier-Stokes, then it's still proven.
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?
Not quite — the formal statement of the problem in Lean may be correct, and therefore the Lean proof gives quite a lot of confidence that the statement is true. It's just that the proof given in natural language doesn't necessarily match up with the Lean proof, so the natural language proof might be unsound even though the statement it's proving is true.
That assumes the natural language paper came first and then was formalized in lean. I haven't looked too deeply into how these labs solve these problems (or if they even specify this publicly) but you could also start with lean and then write the natural language proof based on it.
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.
> If the lean proof doesn't match the natural language one (which is the one the AI generated to solve the problem), it sounds like the lean proof isn't verifying the intended claim?
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.
> The natural language proof was derived from the lean code, badly.
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.
It's not that much of a stretch: give the LLM a top-level proposition for the thing you want to prove and have it hack away at it. Each sub-step is verified in lean so you know it's correct. But, the linked post definitely suggests otherwise.
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.
An incredible number of people think that it is reasoning in lean. Argued with several people on this topic. I think they read headlines about lean being used by LLMs and assume it is being used to write the proof.
That makes some sense. Given that the vast majority of math in its training data is going to be in NL/latex, I just assumed that the core reasoning happens in NL with occasional LEAN checks to ensure validity.
I'm pretty sure Mathlib has had enough human authored definitions to formalize the basic calculus necessary to state Navier-Stokes for quite some time? Some other problems admittedly need quite a bit of machinery built up to even try to say what the question is, but every undergrad learns multiple approaches to formally define everything necessary to write down a PDE.
They do not. Maybe if they take Lean classes? Maybe starting this year they will but my youngest kid is on their like 5th math class in undergrad and hasn't had any lean at all. Not all undergrad math majors even take PDEs; applied maybe, unless you are doing applied discrete math (graphs, combinatorics).
Not Lean specifically, but IMO it's pretty straightforward if you've done math and some programming (and at least my school required some programming).
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.
Indeed. The natural language proof is incorrect but the Lean proof is correct.
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.
Yes — because there are many non-equivalent statements that are easier to prove.
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.
This paper is a large amount of nothing. First, natural language is not as precise as lean, so you have multiple ways to translate a NL argument to Lean. As shown in Fig 1, the LLM did a decent job at translating the argument about roots in a succint way.
Moreover, the paper claims that the NL arguments of Navier-Stokes are stronger than the Lean ones. My understanding is that the translator LLM got lazy and wrote the minimal amount of code that satisfied the theorem without the extra stronger claims.
It is common in mathematical papers to say "And by the way, this actually proves [stronger claim]", but this is something an AI with a precise goal of performing a translation would never do, as it's goal is to translate the proof, not to quality mathematics.
The paper shows that the Lean proof and the prose (pdf) proof do not match exactly. But if the Lean theorem Lean accepted is equivalent to original problem statement published by the Clay Institute, this mismatch is of no consequence to the validity of the proof itself. That's not a trivial if: stating the problem precisely is often as hard as the proof. Validation efforts should concentrate on whether the Lean theorem is equivalent to the one published by the Clay Institute.
That said, a gap between the Lean proof and the pdf is annoying for interpretability, and interpretation is a valid aim, but that does not factor into the proof's validity.
> That's not a trivial if: stating the problem precisely is often as hard as the proof.
Really? You think 300 lines of Lean code [1] is just as hard as the proof (or even remotely close)? Also note, as the README says [2], that the theorem was written independently by formal conjectures, not by the LLM.
- The lean kernel could always have a bug.
- The formalized statement may not correspond to what _mathematicians_ "actually
wanted"
It seems natural to make the argument of, "Well, even if you make the argument
that the proof can have mistakes, it's surely easier to check the problem
statement of something rather than the solution".
(A "nice property" is that, the agent doesn't need to even get "subarguments
correct" according to the _second_ criteria - maybe in the natural proof it
invents an object subtly different from the formal one, but it all checks out.
If you guarantee that the _original_ statement corresponds, then the only
possibility is the lean kernel. So it doesn't recurse infinitely, in this case).
But "definitions" are always a really weird thing that I don't think we have
good theories for? How do you quantify how much descriptive power you need to
express a question? Often times in math, the hard part is getting the definition
right - but what if the definition itself starts to become so complex and
unverifiable that no one can correspond that to anything? Well, it seems like
many interesting long-standing math problems have "relatively" simple problem
statements, in such a way that you could formalize it to lean easily, but not
sure if there's really a silver bullet w/ lean or if it's going to be turtles
all the way down.
It probably doesn't matter as long as AI keeps skyrocketing on the much more
general property that is "intelligence", but still. Interesting to think about.
(Well, this is where AIT gets actually interesting, but still, I don't think its
a generalized theory of semantics.)
Given the high-level description of the examples, I think it's less of a "mis-translation" as it is the LLM tweaking the proof as it formalized it. Going between m+4 and m+5 is a pretty different thing than the sort of ambiguities that generally arise in parsing natural-language mathematical statements.
Hm, looking through here, I don't see where they state what it is that OpenAI actually proved instead of Navier-Stokes blowup with forcing. I see where they do this for some other particular statements used along the way, but not for the headline result.
I've had discussions around this with theorem prover types (OPLSS, highly recommend for people who can take the two weeks off)
The sort of head canon for any of the automated proof systems is that lean saying a proof is correct is "if lean is correct then the proof is correct".
One can get the temptation to try and prove lean correctness with lean but I believe _that_ is impossible due to the incompleteness theory.
_But_ the discussions I had, everyone was kind of in agreement with the idea that you could continue to shrink down the "kernel" of lean with lean (or whatever proof system really) so that in the end the thing you have to trust is pretty small.
Well, I believe the incompleteness theorems speak about provability, not about how the proofs themselves are expressed.
We know as a consequence of Goedel theorems (at least I believe so), that there is no algorithm that would take a statement and output a proof if it is provable or a counterexample if it is not. However, AI provers never give anything for sure, so I think there is no contradiction here.
Not quite. If the statement is provable, an algorithm can find the proof by just looking at all possible proofs, in order of length. (It's assumed that that a valid proof can be algorithmically confirmed to be valid - there's an algorithm that when given a purported proof will eventually output "valid" if it is in fact valid.) The algorithm will find a proof eventually, if there is one. If there is a (provable) counterexample, the algorithm will similarly eventually find that. What Goedel's incompleteness theorem says is that such a search algorithm may never terminate - never finding a proof, and never finding a counterexample.
(The algorithms described above are of course completely impractical, taking time exponential in the length of the proof (of theorem or counterexample).)
The incompleteness theorems state that every sufficiently complicated logic lets you construct a statement that is effectively "this statement has no proof," so either there exists true statements that lack proofs (incompleteness) or there exists false statements with proofs (incorrectness).
Just all the useful proofs. You can get arbitrarily more complicated and uninteresting theorem statements by making meta statements about the system you are doing proofs in. At some level the system can't answer questions about itself.
The incompleteness theorem says that there are statements which can be neither proven true nor false in a given axiomatic system. If there is a proof to write in lean, then the statement is already outside the bounds of incompleteness.
I recently spent 3 weeks with claude formalizing a CS paper about a borrow checker in lean, for a personal project.
The formalization went through, but there were _several_ mistakes in the original paper that it uncovered, from type setting errors to (many) formulas that quantified over all resources as printed, but actually applied to only arising resources in the calculus..
So the formalization did give me a formally verified borrow checker that I could use to build a programming language on top of, but it was _not_ exactly the borrow calculus that was printed in the paper.
I expect this is the most common experience when mechanizing a printed paper. There are a lot of skipped steps and handwaving.
As a second rate scientist, nothing makes me happier than finding a "hot" paper in my field, reading it, converting it to code, and demonstrating the authors made systematic errors that mean the paper is more likely false than true.
I've been criticized for doing this, but to me it emphasizes how much attention goes to the hot, wrong papers.
This is the common experience in replicating a published paper by hand ... it is common to find "obvious" aspects that are anything but.
The scary thing is when AIs generate unreadable formal proofs and then effectively lie (or fabulate, to be polite-ish) about the natural language version of the steps. Since the natural language version is arguably the most important aspect of a solution to a flagship problem, this fabulation deflates the value of the solution while the existence of the solution discourages further work on the problem.
I have hopes that this is primarily a matter of needing more engineering work on ergonomic formal languages and better building a language that "looks like math." e.g. when doing linear algebra stuff, a linear combination might be defined as a finitely supported function from an index set to your space, which is fine, but ugly and maybe conceptually overwhelming on first meeting, so I did some toying with little macros and eventually a small python Lean -> HTML renderer to do some basic transformations to make it look more like typical math notation with like \Sigma_{i \in I} a_i, or with a_0+...+a_n, etc. (to... not fantastic success, but I think there's still something to the idea).
I think a lot of math notation isn't wrong given a context, so in theory we should be able to translate it into something formal. Maybe also generate living documents where you can e.g. write `h : some_claim := by details(by rw[nat_mul_comm]; ...)` and the renderer hides details just like you'd write "obviously" in a traditional text. If the reader wants, they could then expand the details. etc. I found that many codex-generated proofs could be improved by telling it that I want a sequence of steps
have next_step := by <I don't care>
have therefore := by <still don't care>
So that the human proof appears as the left side, and I just ignore the right side as petty details. Again, not fantastic success, but better. Otherwise it goes very... Leanish by default.
Lean's VSCode plugin is I think only starting to explore the idea of a proper IDE for math. There's probably still tons of unexplored potential for like that fused with Matlab or whatever.
I enjoy running into those details when implementing papers, since it usually leads to improved understanding of the subject and an ability to approach the matter with more rigor in some way that I had not noticed before. It does also involve a lot of work and lost sleep though.
We should be very careful about relinquishing sorting through such details to AI.
Claude could not fix them without a lot of help, so i did not relinquish sorting through those details in general. Just the drudgery of grinding through proof obligations.
Humans will have to wade through mountains of slop to decipher the argument. Alternatively, they could just ignore it like Mochizuki's ABC proof prior to the Scholze/Stix refutation.
I think this highlights that, at the very least, coverage of AI-generated proofs should describe them as "claims" to solve problems, until, like all other works, the community has had time to review and digest them.
The idea that an AI company is beyond peer review is harmful.
As far as I understand it, nobody is disputing the correctness of the Lean proof, or that it proves the conjecture it actually claims to prove. That's sufficient to consider the problem "solved". The natural language proof is a "nice to have".
The claim in TFA is that the formalization(in Lean) of the problem does not correspond to the natural language statement of the problem, such that the statement proven is not the conjecture for which proof is required for the problem to be considered "solved".
Does that contradict what I said? In that quote, it says that the NL proof does not correspond to the Lean proof. However, the statement of the theorem in Lean is independent from the NL proof. It comes from a DeepMind repository, which as far as I'm aware has been accepted by the community as a valid formalization of the original Clay Institute statement.
I would say it's released in the spirit of open source. "Peer review" in the narrow sense exists primarily to assign prestige in academia; but there's nothing stopping anyone from "peer reviewing" the GitHub repository.
So they could also dump a 100 quadrillion line proof in Bourbaki notation and call it a day?
The proof was released in the spirit of being first at all costs without any attempt to clean it up. I doubt that OpenAI mathematicians could give a coherent talk about it, certainly not using a blackboard.
What kind of prestige? Peer review is anonymous unpaid work.
A good review does not merely check the correctness of logical arguments, it gives suggestions for the exposition, citing the correct references, putting everything in the right context, etc.
All of the reasons you listed for peer review are valid. The broader point is that peer review can happen outside of academic journals, and nobody has an incentive to submit to them who isn't trying to play the academic prestige game. For a significant example, see the history of Perelman's proof of the Poincaré conjecture.
> journals are not the arbiter of truth and getting published in them is something only academics have an incentive to do
Good, I just wanted to point out that peer review isn't primarily an arbitrage of truth, it is also to make sure the exposition is nice to read. When you get a reviewer who actually cares, you receive lots of feedback that isn't related to the correctness of Lemma 3.14.15 and stuff like that.
This is an equivalent of a company producing security software, open sourcing their code, and then claiming that since no one has found any serious bugs, their software is secure.
No. The way to build confidence that your software is well made, you do a proper external security audit and obtain the requisite certificate from a proper auditing firm.
It's also incorrect to think peer review in mathematics is low quality (like it is in some other fields). Certainly, when major results are in place, editors ensure that high quality peer reviewers are recruited and do their job properly. Like all human processes this fails sometimes, but not enough to not do it.
>then claiming that since no one has found any serious bugs, their software is secure.
which specific openai statements does this part of your analogy map to?
in the "sharing ai progress in mathematics" blog, openai simply says "results", and never once claims that all of them are unquestionably true. instead, they state they want to evaluate the results. their github states that the results are "different stages of verification" and also says "Some of the unformalized results could have issues"
that is the opposite of "claiming [...] their software is secure", to use your analogy.
I didn't say peer review is low quality; just that it's not necessary or sufficient to determine the truth. Ultimately the OpenAI proof stands or falls on things that have been audited externally, namely the formalization of the problem in Lean and the correctness of the Lean software. There's no incentive for OpenAI to submit to a peer-reviewed journal when they don't need to play the academic prestige game. TFA is an example of peer review in action: they're analyzing the proof and finding points to criticize.
this happens in approximately every scientific field. ive never heard it described as "idea that they are beyond peer review".
openai themselves specifically call out that there may be issues with their results. journalists and laypeople just happen to skip that part, like they do with ~all physics, health, astronomy, etc results.
Because they want to release everything on github so everyone can peer review it themselves
This is far more efficient and they’re telling the academic industry to grow up
Sister comments are saying that academics dont like the Lean programming language and see a lack of human language described proof. Doesn’t sound like something I should care about but I’m watching for a better human language description of the problem as this discussion evolves
I've seen a lot of breathless reporting about various mathematical things being "proven" on the basis of the LLM-generated Lean formulation compiling. We probably wouldn't declare that for a human-written proof until peers had checked the proof for errors
This. The proof of Fermat’s Last Theorem took 15+ months to check. It’s absurd to see the media reporting that these big problems are solved based off of a news release and a hastily and mostly AI-written manuscript, and OpenAI et al. are all too happy to run with said breathless reporting.
Wiles' proof was informal and couldn't be checked by a computer. In this case, the experts need to check 300 lines of Lean code (mostly comments) and confirm that it formalizes the problem statement correctly. There are papers building on the solution and analyzing it for more general versions of the problem, which suggests that the PDE community has already accepted it and moved on.
there's breathless reporting of just about everything scientific. physics, astronomy, archaeology, etc. have this sort of thing all the time.
yet i have never seen anyone say "the idea that physicists are beyond peer review is harmful" because some mainstream news articles published a piece about dark energy or whatever.
Anyone who doesn't understand peer review (its intended workings, its negative effects by implementation flaws, etc.) automatically assumes expression is beyond academic peer review, so thats potentially a lot of people...
So my guess is that they have the AI system attempt to prove the theorem in natural language, then try to generate a Lean proof for it, and in that process they end up with a slightly different solution as the autoformalizer is essentially rewriting the NL proof to make it formalizable? Do we just need a "reverse pass" to re-align the NL proof with the Lean code?
Also, it doesn't seem that they are questioning the truthfulness of either proof, just that they are different?
Generating the lean proof first is a viable approach as well followed by an explanatory pass.
Actually, they are questioning whether the natural language description of the proof is either not faithful to the formal proof, or simply wrong, or both.
Because it is really hard to read and the level of detail is so high that even lemmas that you can read may have such enormous levels of detail that makes real understanding difficult given that humans have limited working memory.
The same JavaScript code compiles to different machine representations under different browser engines; yet webdevelopers don't need to learn assembly.
There is an abstract javascript machine which can obviously be translated to hardware instructions. "Obvious" in the mathematical research sense, as in the statement is flat out wrong under closer inspection. Websites regularly crash under memory pressure.
But they are good enough most of the time, and that's the key. With more resource a more correct program can be created, but cost-benefit calculations show a ceiling. A local pet store does not have the money to pay 2000 hours of formal verification work, and usually a WordPress site is good enough.
Mathematicians work with their brains. They have finite time to understand papers. Formalists say that all theorems could be reduced to logical axioms, but most of time it's jumping at a much higher level, because no one has time for minute details. Proofs are theoretically right or wrong, but in practice there are "slightly wrong" proofs, where there are some minute errors that "feels" like can be correcte, and most of the time it can be. This ambiguity is not a problem, but a feature of mathematics, because it means more time can be spent to move faster at a higher level of abstraction, but this would be lost with Lean.
Same reason humans write code not only for a compiler to translate into machine code but also so other humans can understand what we write, learn from it, modify it etc...
From the first example, it seems like this paper is so contrived. They pose a statement (y = x^3 - x^2 - 1 + 1 when x > -1) which is true, then provide incorrect reasoning but swapping the multiplicity of -1 and 1, then ask it to provide a proof. Essentially, they are running an injection attack; they give it 90% correct information, then it expects in good faith that -1 and 1 are not swapped, so it takes it verbatim. I don't see how the fact that ChatGPT can sometimes get this wrong, especially when the user is the bad actor trying to trick the computer and isn't actually trying to find a proof, is at all relevant to the Navier-Stokes solution.
> In particular, we highlight that the problem of resolving ambiguities in mathematical NL text, which is necessary in order to provide semantically faithful translation
This is what I've been wondering about with LLM proofs. Math is logical, but mathematical writing is still natural language: symbols get overloaded, conventions go unstated, and a lot rides on context. So a model can translate a statement into a formal system and prove it, and the proof can check out, while the statement it proved isn't quite the one the mathematician meant. I read this article as a caution that some of the LLM proofs announced so far may not hold up once a human checks what was actually proved. Is that a fair reading?
Natural language is ambiguous, but the Lean formalization is very well defined and unambiguous.
It's not the form language that is the real problem here. It's the ambiguity on the other side and the extreme difficulty of doing a useful and accurate translation.
This shouldn’t be a surprising result. We’ve known almost since LLMs became a thing that they can “prefer” modifying the terms or context of a problem when they can’t solve it directly (what one might call “cheating” if there were any volition involved). Often that happens in a way that isn’t immediately obvious to the user.
Before it was dropping databases or deleting repositories. Now it’s subtly changing the meaning of math problems to get a correct but irrelevant answer.
> 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.
So it suggests that the formalization/verification step may have fixed some issues in the natural language proof, and either such differences were never noticed or the corrections weren't ported back to the NLP.
Indeed. I've never used AI to translate between natural language and Lean but I have gone from English to Golang, Python, Typescript and SQL and its interpretations can be... creative, let's say.
Aside from the usual squabbling about AI, it seems the bombshell claim is this:
"In particular, we show that the formalised Lean proof does not correspond to the NL proof of blow-up of solutions to the Navier-Stokes equations."
So these authors seem to be claiming that OpenAI has not really proven Navier-Stokes at all. If I get their idea correctly, they are claiming that the LLM has not formalized the original "natural language" idea of Navier-Stokes correctly. If true, it would mean that their purported Lean proof is not actually a proof of Navier-Stokes at all, but something that is an incorrect translation of the original natural language idea. If correct, this is a really bold claim and I would like to see if other researchers agree.
No, they're not claiming that.
No one is disputing that the Lean formaization of Navier-Stokes is correct, so we should have high confidence that the generated Lean proof is valid.
The authors are claiming that the Lean proof is not the same proof as the NL one. Therefore, we shouldn't yet have confidence that the NL proof is valid.
This is an important claim which the math community will need to work through. However, the Lean proof alone is sufficient for OpenAI to (reasonably confidently, leaving aside questions of academic manners) claim to have proven NS.
So, the AI wrote a NL proof of Navier-Stokes, then incorrectly auto-formalised it to Lean, but still ended up with a verifiable proof of Navier-Stokes? That seems... strange?
This same thing happened back in the 10 advances in math and CS release a month or two ago. The non sofic group construction relied on false prior literature. They realized this and fixed it in the lean program but didn't modify it in the writeup, so the written proof was both incorrect as stated and did not correspond to the lean proof. I was surprised how little press it got at the time, it seems like a huge risk factor.
I don't know if we can really be clear about the order of things, but I think even without AI maths is filled with "someone provides a proof of X, and the proof itself is wrong/incomplete but X itself is true".
"Incomplete" proofs might be a way of viewing this. You have a NL argument to prove X. It turns out the NL proof has holes you can drive a truck through. So... you go around and patch the holes.
The resulting proof is different! You can start off with a bad proof and find a correct proof. Sometimes.
EDIT: for French speakers (maybe autodub gets you there) I saw a very nice simple case of this recently. A commonly stated proof for a relatively simple theory. The proof has a giant hole in it, and completing it requires some work [0])
[0] https://www.youtube.com/watch?v=kQBu6NH1u3I
Or the AI wrote a NL proof of Navier-Stokes, began rewrite in Lean, then discovered a false / handwavy / easier to write in Lean / etc approach of some parts of the proof, and modified it accordingly. Since there wasn't any backpass from Lean to NL to include any changes it did due to any of the above reasons, the proofs aren't identical. That's what I think is most likely.
If the reason for the differences was done intentionally in Lean (as opposed to hallucinate e.g. m+4 vs m+5 as mentioned in remark 3.2), then a simple recording of differences, and then afterwards pass back any changes to the original NL would fix the issue. If it was hallucinated, then there is no guarantee it wouldn't keep hallucinating, and thus you might never end up with the same proof no matter how many passes you do back and forth (see remark 3.4).
It's not actually the same model that solved the problem that did the translation. Astra did the translation after the intenral model produced the NL Proof. As for the discrepancies, It's not necessarily right to think of this as 'incorrect formalisation'. Maybe it was essentially a 'proof refactoring'. Maybe Astra thought some parts could be easier expressed in a certain way, or maybe aspects of the NL proof were kind of handwavey etc.
Trying to map this observation to code and appreciate them starting with very simple examples (that Astra screw-fixed into lean.) But in a simplified way this is close to promting the model to create a set with the members 1,2,1,5 and it correctly creates {1,2,5} in code. So The initial "proof" / instruction was wrong and it silently fixed that. ( Which is one of the failure modes they're describing)
If you’ve tried any formalizing in codex Astra often works solely in Lean
it's the result of thinking carefully about the translation process.
humans as a whole have always known the weakness of natural language is in its precision. In a way this isn't strange that this issue has come up.
I would expect it's the other way around. The AI wrote a Proof of NS in lean and write up a NL proof based on the lean one. The authors claim that openAI did NL -> Lean, but that is unsubstantiated.
The OpenAI announcement says
> 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.
This seems pretty clear that they found the proof first and then mechanized it afterwards.
Or maybe the AI didn’t write Lean proof at all, or rather, not the LLM at least. But instead OpenAI has an internal traditional reinforcement model that is able to stumble on the Lean proof by the share amount of compute power available to them thousand monkeys on a thousand typewriter style. And then pretend LLM did it because that is what they are selling.
Not necessarily monkeys but thinking in Lean first is quite plausible
>No one is disputing that the Lean formaization of Navier-Stokes is correct, so we should have high confidence that the generated Lean proof is valid.
These authors don't seem to be disputing that this Lean formalization of Navier-Stokes is correct. I don't think that gives us any new information about whether the generated Lean proof is or isn't a valid proof of this N-S blowup thing.
If it doesn't correspond to the original proof then you don't know what it is actually formalizing. It could be a buggy proof of ⊥.
The thing is that Navier-Stokes has a definition split off separate from the formalization, and that is what has been completed. People have looked at the definition of the final statement. This paper only mentions the proof and intermediate statement, not the final statement. The most likely case to me is that intermediate statements do not match, but the end result still holds.
Seems kinda odd then that it didn't occur to OpenAI to iterate until they reached a fixedpoint for both the informal & formal development b/c it's obvious that correspondence should have been part of their training pipeline.
Jesus Christ, so many people here who have no clue what they are talking about.
A proof of a theorem is different from the statement of the theorem. OpenAI has a Lean proof of the statement. That is all they need. There may be many different proofs of this statement, including NL proofs. It does not matter that these NL proofs may or may not be different from the Lean proof, at least for the correctness of the Lean proof. But of course the NL proof may be wrong. But who cares?
It reminds me of how provably secure software was all the rage for awhile. Until people found that the idealized system/lemmas were so far from reality that the proved security was worse than meaningless because it gave a false sense of security.
In order to prove security, you must first simulate the universe.
> the NL proof may be wrong. But who cares?
The people trying to understand the proof are probably following the natural language version. So they care.
I wouldn’t be surprised at all if that’s how this paper (which I did not read) arose.
Why would they do that, knowing that the one known to be correct is the Lean one? Just to claim that the (correct) Lean proof did not translate well to English? That would be weak, and a colossal waste of energy and time.
> Jesus Christ, so many people here who have no clue what they are talking about.
Indeed. If only some of those people would see the irony.
What matters most of all, as any first year student of mathematics would know, is whether the formal problem statement corresponds to the NL statement. TFA specifically states that at least some of the allegedly proven formal statements DO NOT.
No. What the paper says is that in principle, translating NL statements to Lean statements is hard. Nobody doubts that, translating informal to formal text cannot be formally proven correct, so...
Does the paper give a single example of one of the OpenAI solved theorems with a Lean certificate where the Lean statement does not correspond to the actual statement from the mathematical literature? I don't think so, but in case I am wrong, feel free to provide that example.
If I understand the abstract correctly (big caveat), they aren't saying they didn't prove it. They're saying they gave two proofs, one in natural language and one in Lean, that are not equivalent to each other. I assume the main significance is that the Lean proof is not a formal verification of the natural language one and the natural language proof is not a readable explanation of the Lean one. Both of those things can be desirable, so to complete the set we'd get 4 proofs.
But just to clarify: is either of them actually addressing the real Navier-Stokes, or will it turn out we'll end up with two pairs of proofs about something irrelevant to the actual problem?
This is the formalization that was proven in Lean. As of now at least, it's believed to be a correct statement of the problem.
https://github.com/google-deepmind/formal-conjectures/blob/8...
Nobody is claiming they've misformalized Navier-Stokes.
From computer science perspective the conclusion is obvious: untenable to have two representations without an exact translation or machine checked correspondence between then. All we have is a vibe translation using the LLM. The methodology should obviously be improved.
and clearly the computer science perspective is: get rid of the humans and express everything directly in lean so the computers can keep getting work done!
;)
If I understand well, they mean that the thing they proved in lean is not Navier Stokes. And they don't make any statement about whether the natural language proof is correct or not.
I read them as making a much weaker claim than this: not that the Lean proof isn't valid, just that it is not actually a formalization of the natural-language proof in the PDF they provided alongside it. I haven't heard any PDE people claim that the Lean proof is invalid, and I have heard things from a lot of them that imply that they think it is valid. (I'm a former research mathematician, but this is very far from my specialty, so I'm not really equipped to evaluate this claim myself.)
The claim is about the equivalence between two proofs and says nothing about the correctness of either proof. This seems to be confusing a lot of people.
Navier-Stokes is an equation, not a theorem, so there is no such thing as "a proof of Navier-Stokes". The equation is a partial-differential-equation model of viscous fluid flow. Its correctness has never been in doubt: we know it cannot possibly be an exact description of real fluid flow, that it's a pretty good approximate description, and that there exist well-behaved solutions for a number of initial conditions.
What OpenAI purports to have proven, as I understand it, is that certain initial conditions to that equation, plus "forcing" over time (which could be a literal force acting on the fluid such as stirring it with a spoon or some other extrinsic effect) only have finite (and therefore physically plausible) solutions for a finite period of time, after which singularities appear, with the velocity or pressure of some of the fluid approaching infinity as you approach the finite time limit.
This is a result that Terry Tao conjectured in 02014, but without the forcing: http://arxiv.org/abs/1402.0290
I think we can be pretty confident that the L∃∀N proof is really about Navier-Stokes. The question is whether what it says about Navier-Stokes is what we think it says.
> has not formalized the original "natural language" idea of Navier-Stokes incorrectly
Did you mean “not…correctly”?
Nobody has proven or disproven NS equations.
NS is continuous approximation to what is otherwise a discrete system. Particle collisions are discrete time events that are averaged over time. NS loses accuracy for very, very, very very low fluid densities and energies.
AI "proving" that this approximation can numerically "blow" up does not mean the approximation loses validity.
For a refreshment of what is Navier-Stokes in a few words: https://p.migdal.pl/equations-explained-colorfully/#navier-s...
This is so lovely. I desperately wish I could color code all math!!
You can. Not only the code is there, but also an interactive editor.
I experimented with something similar with LLMs. They can kinda do it for some stuff.
More interesting, you can ask a vision model to color parts of speech in img2img and it works OK for frontier models.
Grows infinite hands
Hmm.
I don’t think that actually explains the idea of a momentum density transport equation well at all.
it's a lot of style over substance
If I'm understanding correctly, this is questioning the equivalence between the natural language proof and the lean proof, but not the correctness of the lean proof?
If the lean proof doesn't match the natural language one (which is the one the AI generated to solve the problem), it sounds like the lean proof isn't verifying the intended claim?
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."
The material is interesting, but unless the statement that is proved in lean is not blowup for Navier-Stokes, then it's still proven.
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?
Not quite — the formal statement of the problem in Lean may be correct, and therefore the Lean proof gives quite a lot of confidence that the statement is true. It's just that the proof given in natural language doesn't necessarily match up with the Lean proof, so the natural language proof might be unsound even though the statement it's proving is true.
I was having trouble wrapping my head around it but this cleared it up.
That assumes the natural language paper came first and then was formalized in lean. I haven't looked too deeply into how these labs solve these problems (or if they even specify this publicly) but you could also start with lean and then write the natural language proof based on it.
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.
> If the lean proof doesn't match the natural language one (which is the one the AI generated to solve the problem), it sounds like the lean proof isn't verifying the intended claim?
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.
> The natural language proof was derived from the lean code, badly.
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.
[1]: https://openai.com/index/navier-stokes-solution/
Yeah, I was surprised some people think LLMs are reasoning in Lean directly... all their training data is in NL.
It's not that much of a stretch: give the LLM a top-level proposition for the thing you want to prove and have it hack away at it. Each sub-step is verified in lean so you know it's correct. But, the linked post definitely suggests otherwise.
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.
An incredible number of people think that it is reasoning in lean. Argued with several people on this topic. I think they read headlines about lean being used by LLMs and assume it is being used to write the proof.
That makes some sense. Given that the vast majority of math in its training data is going to be in NL/latex, I just assumed that the core reasoning happens in NL with occasional LEAN checks to ensure validity.
The lean proof being correct is easy to verify, whether it proves the thing we care about is much harder.
If your code compiles, are you sure it's bug free?
I'm pretty sure Mathlib has had enough human authored definitions to formalize the basic calculus necessary to state Navier-Stokes for quite some time? Some other problems admittedly need quite a bit of machinery built up to even try to say what the question is, but every undergrad learns multiple approaches to formally define everything necessary to write down a PDE.
They do not. Maybe if they take Lean classes? Maybe starting this year they will but my youngest kid is on their like 5th math class in undergrad and hasn't had any lean at all. Not all undergrad math majors even take PDEs; applied maybe, unless you are doing applied discrete math (graphs, combinatorics).
Not Lean specifically, but IMO it's pretty straightforward if you've done math and some programming (and at least my school required some programming).
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.
I'm not sure if calculus of constructions comes naturally to people who didn't have some experience with functional programming.
Not a mathematician, but "pretty sure" might not be good enough to resolve this question.
Lucky that it was enough in this case. The theorem had been written by formal conjectures before the proof https://github.com/openai/NavierStokesAndEuler/blob/main/Com...
syntax vs semantics
It doesn't look like they've found an error in the NL proof either, just that they are different?
Indeed. The natural language proof is incorrect but the Lean proof is correct.
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.
How do you know the natural language proof is incorrect?
Yes — because there are many non-equivalent statements that are easier to prove.
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.
Yes, exactly. There's no real pressure on AI to get the natural language version of the proof correct, and no way to really judge it automatically.
Yes however, whether a natural language proof and a formal proof "correspond" is subjective.
This paper is a large amount of nothing. First, natural language is not as precise as lean, so you have multiple ways to translate a NL argument to Lean. As shown in Fig 1, the LLM did a decent job at translating the argument about roots in a succint way.
Moreover, the paper claims that the NL arguments of Navier-Stokes are stronger than the Lean ones. My understanding is that the translator LLM got lazy and wrote the minimal amount of code that satisfied the theorem without the extra stronger claims.
It is common in mathematical papers to say "And by the way, this actually proves [stronger claim]", but this is something an AI with a precise goal of performing a translation would never do, as it's goal is to translate the proof, not to quality mathematics.
The paper shows that the Lean proof and the prose (pdf) proof do not match exactly. But if the Lean theorem Lean accepted is equivalent to original problem statement published by the Clay Institute, this mismatch is of no consequence to the validity of the proof itself. That's not a trivial if: stating the problem precisely is often as hard as the proof. Validation efforts should concentrate on whether the Lean theorem is equivalent to the one published by the Clay Institute.
That said, a gap between the Lean proof and the pdf is annoying for interpretability, and interpretation is a valid aim, but that does not factor into the proof's validity.
> That's not a trivial if: stating the problem precisely is often as hard as the proof.
Really? You think 300 lines of Lean code [1] is just as hard as the proof (or even remotely close)? Also note, as the README says [2], that the theorem was written independently by formal conjectures, not by the LLM.
[1]:https://github.com/openai/NavierStokesAndEuler/blob/main/Com...
[2]: https://github.com/openai/NavierStokesAndEuler/blob/main/Com...
Quote from paper worth being aware of:
"Disclaimer: We do not make claims about the correctness of OpenAI’s NL proof, we only make statements about mistranslations into Lean."
Will we ever run into a theory of meaning crisis?
_Assuming_ two failure modes:
- The lean kernel could always have a bug. - The formalized statement may not correspond to what _mathematicians_ "actually wanted"
It seems natural to make the argument of, "Well, even if you make the argument that the proof can have mistakes, it's surely easier to check the problem statement of something rather than the solution".
(A "nice property" is that, the agent doesn't need to even get "subarguments correct" according to the _second_ criteria - maybe in the natural proof it invents an object subtly different from the formal one, but it all checks out. If you guarantee that the _original_ statement corresponds, then the only possibility is the lean kernel. So it doesn't recurse infinitely, in this case).
But "definitions" are always a really weird thing that I don't think we have good theories for? How do you quantify how much descriptive power you need to express a question? Often times in math, the hard part is getting the definition right - but what if the definition itself starts to become so complex and unverifiable that no one can correspond that to anything? Well, it seems like many interesting long-standing math problems have "relatively" simple problem statements, in such a way that you could formalize it to lean easily, but not sure if there's really a silver bullet w/ lean or if it's going to be turtles all the way down.
It probably doesn't matter as long as AI keeps skyrocketing on the much more general property that is "intelligence", but still. Interesting to think about.
(Well, this is where AIT gets actually interesting, but still, I don't think its a generalized theory of semantics.)
Given the high-level description of the examples, I think it's less of a "mis-translation" as it is the LLM tweaking the proof as it formalized it. Going between m+4 and m+5 is a pretty different thing than the sort of ambiguities that generally arise in parsing natural-language mathematical statements.
Hm, looking through here, I don't see where they state what it is that OpenAI actually proved instead of Navier-Stokes blowup with forcing. I see where they do this for some other particular statements used along the way, but not for the headline result.
I get the feeling a lot of people propose that we can write a verifier for every proof in lean.
Can someone tell me in simple terms why this doesn't conflict with the incompleteness theorems?
edit: thanks for the responses, i feel slightly less dumb now
I've had discussions around this with theorem prover types (OPLSS, highly recommend for people who can take the two weeks off)
The sort of head canon for any of the automated proof systems is that lean saying a proof is correct is "if lean is correct then the proof is correct".
One can get the temptation to try and prove lean correctness with lean but I believe _that_ is impossible due to the incompleteness theory.
_But_ the discussions I had, everyone was kind of in agreement with the idea that you could continue to shrink down the "kernel" of lean with lean (or whatever proof system really) so that in the end the thing you have to trust is pretty small.
Well, I believe the incompleteness theorems speak about provability, not about how the proofs themselves are expressed.
We know as a consequence of Goedel theorems (at least I believe so), that there is no algorithm that would take a statement and output a proof if it is provable or a counterexample if it is not. However, AI provers never give anything for sure, so I think there is no contradiction here.
Not quite. If the statement is provable, an algorithm can find the proof by just looking at all possible proofs, in order of length. (It's assumed that that a valid proof can be algorithmically confirmed to be valid - there's an algorithm that when given a purported proof will eventually output "valid" if it is in fact valid.) The algorithm will find a proof eventually, if there is one. If there is a (provable) counterexample, the algorithm will similarly eventually find that. What Goedel's incompleteness theorem says is that such a search algorithm may never terminate - never finding a proof, and never finding a counterexample.
(The algorithms described above are of course completely impractical, taking time exponential in the length of the proof (of theorem or counterexample).)
The incompleteness theorems state that every sufficiently complicated logic lets you construct a statement that is effectively "this statement has no proof," so either there exists true statements that lack proofs (incompleteness) or there exists false statements with proofs (incorrectness).
Just all the useful proofs. You can get arbitrarily more complicated and uninteresting theorem statements by making meta statements about the system you are doing proofs in. At some level the system can't answer questions about itself.
The incompleteness theorem says that there are statements which can be neither proven true nor false in a given axiomatic system. If there is a proof to write in lean, then the statement is already outside the bounds of incompleteness.
I recently spent 3 weeks with claude formalizing a CS paper about a borrow checker in lean, for a personal project.
The formalization went through, but there were _several_ mistakes in the original paper that it uncovered, from type setting errors to (many) formulas that quantified over all resources as printed, but actually applied to only arising resources in the calculus..
So the formalization did give me a formally verified borrow checker that I could use to build a programming language on top of, but it was _not_ exactly the borrow calculus that was printed in the paper.
I expect this is the most common experience when mechanizing a printed paper. There are a lot of skipped steps and handwaving.
As a second rate scientist, nothing makes me happier than finding a "hot" paper in my field, reading it, converting it to code, and demonstrating the authors made systematic errors that mean the paper is more likely false than true.
I've been criticized for doing this, but to me it emphasizes how much attention goes to the hot, wrong papers.
This is the common experience in replicating a published paper by hand ... it is common to find "obvious" aspects that are anything but.
The scary thing is when AIs generate unreadable formal proofs and then effectively lie (or fabulate, to be polite-ish) about the natural language version of the steps. Since the natural language version is arguably the most important aspect of a solution to a flagship problem, this fabulation deflates the value of the solution while the existence of the solution discourages further work on the problem.
I have hopes that this is primarily a matter of needing more engineering work on ergonomic formal languages and better building a language that "looks like math." e.g. when doing linear algebra stuff, a linear combination might be defined as a finitely supported function from an index set to your space, which is fine, but ugly and maybe conceptually overwhelming on first meeting, so I did some toying with little macros and eventually a small python Lean -> HTML renderer to do some basic transformations to make it look more like typical math notation with like \Sigma_{i \in I} a_i, or with a_0+...+a_n, etc. (to... not fantastic success, but I think there's still something to the idea).
I think a lot of math notation isn't wrong given a context, so in theory we should be able to translate it into something formal. Maybe also generate living documents where you can e.g. write `h : some_claim := by details(by rw[nat_mul_comm]; ...)` and the renderer hides details just like you'd write "obviously" in a traditional text. If the reader wants, they could then expand the details. etc. I found that many codex-generated proofs could be improved by telling it that I want a sequence of steps
So that the human proof appears as the left side, and I just ignore the right side as petty details. Again, not fantastic success, but better. Otherwise it goes very... Leanish by default.Lean's VSCode plugin is I think only starting to explore the idea of a proper IDE for math. There's probably still tons of unexplored potential for like that fused with Matlab or whatever.
I enjoy running into those details when implementing papers, since it usually leads to improved understanding of the subject and an ability to approach the matter with more rigor in some way that I had not noticed before. It does also involve a lot of work and lost sleep though.
We should be very careful about relinquishing sorting through such details to AI.
Claude could not fix them without a lot of help, so i did not relinquish sorting through those details in general. Just the drudgery of grinding through proof obligations.
It was a piston in a non-compressible fluid so to speak (ie. storm in a glass of water)
Two leading experts on Navier Stokes still do not know whether their methods were used:
https://terrytao.wordpress.com/2026/10/04/on-classical-solut...
Humans will have to wade through mountains of slop to decipher the argument. Alternatively, they could just ignore it like Mochizuki's ABC proof prior to the Scholze/Stix refutation.
I think this highlights that, at the very least, coverage of AI-generated proofs should describe them as "claims" to solve problems, until, like all other works, the community has had time to review and digest them.
The idea that an AI company is beyond peer review is harmful.
As far as I understand it, nobody is disputing the correctness of the Lean proof, or that it proves the conjecture it actually claims to prove. That's sufficient to consider the problem "solved". The natural language proof is a "nice to have".
The claim in TFA is that the formalization(in Lean) of the problem does not correspond to the natural language statement of the problem, such that the statement proven is not the conjecture for which proof is required for the problem to be considered "solved".
>the statement proven is not the conjecture for which proof is required for the problem to be considered "solved".
that's not the claim. the formal statement of the problem for the NS proof was written by humans not autoformalized.
That's not the claim made in TFA. See the sibling comments, in particular about the DeepMind formalization.
[flagged]
Please make your substantive points without swipes. This is in the site guidelines: https://news.ycombinator.com/newsguidelines.html.
Does that contradict what I said? In that quote, it says that the NL proof does not correspond to the Lean proof. However, the statement of the theorem in Lean is independent from the NL proof. It comes from a DeepMind repository, which as far as I'm aware has been accepted by the community as a valid formalization of the original Clay Institute statement.
https://github.com/google-deepmind/formal-conjectures/blob/8...
Both proofs may be correct, and the problem may indeed be solved. My point is that it should not be assumed.
> Maybe read the original article before replying, at a minimum.
Maybe read the comment before replying, at a minimum.
>The idea that an AI company is beyond peer review is harmful.
i havent seen this sentiment expressed anywhere, have you?
isn't this comment chain on a submission about openai's claims being reviewed?
OpenAI has expressed this sentiment by not submitting to or saying they will submit their results to peer reviewed journals.
I would say it's released in the spirit of open source. "Peer review" in the narrow sense exists primarily to assign prestige in academia; but there's nothing stopping anyone from "peer reviewing" the GitHub repository.
I would say it's released in the spirit of machine learning's competitive landscape (which is the culture this emerged from).
So they could also dump a 100 quadrillion line proof in Bourbaki notation and call it a day?
The proof was released in the spirit of being first at all costs without any attempt to clean it up. I doubt that OpenAI mathematicians could give a coherent talk about it, certainly not using a blackboard.
Sure, why not? They can publish whatever they want, then the public can choose to ignore it, criticize it, or accept it.
What kind of prestige? Peer review is anonymous unpaid work.
A good review does not merely check the correctness of logical arguments, it gives suggestions for the exposition, citing the correct references, putting everything in the right context, etc.
> What kind of prestige? Peer review is anonymous unpaid work.
Prestige to the reviewed, not to the reviewer.
All of the reasons you listed for peer review are valid. The broader point is that peer review can happen outside of academic journals, and nobody has an incentive to submit to them who isn't trying to play the academic prestige game. For a significant example, see the history of Perelman's proof of the Poincaré conjecture.
> journals are not the arbiter of truth and getting published in them is something only academics have an incentive to do
Good, I just wanted to point out that peer review isn't primarily an arbitrage of truth, it is also to make sure the exposition is nice to read. When you get a reviewer who actually cares, you receive lots of feedback that isn't related to the correctness of Lemma 3.14.15 and stuff like that.
This is an equivalent of a company producing security software, open sourcing their code, and then claiming that since no one has found any serious bugs, their software is secure.
No. The way to build confidence that your software is well made, you do a proper external security audit and obtain the requisite certificate from a proper auditing firm.
It's also incorrect to think peer review in mathematics is low quality (like it is in some other fields). Certainly, when major results are in place, editors ensure that high quality peer reviewers are recruited and do their job properly. Like all human processes this fails sometimes, but not enough to not do it.
>then claiming that since no one has found any serious bugs, their software is secure.
which specific openai statements does this part of your analogy map to?
in the "sharing ai progress in mathematics" blog, openai simply says "results", and never once claims that all of them are unquestionably true. instead, they state they want to evaluate the results. their github states that the results are "different stages of verification" and also says "Some of the unformalized results could have issues"
that is the opposite of "claiming [...] their software is secure", to use your analogy.
I didn't say peer review is low quality; just that it's not necessary or sufficient to determine the truth. Ultimately the OpenAI proof stands or falls on things that have been audited externally, namely the formalization of the problem in Lean and the correctness of the Lean software. There's no incentive for OpenAI to submit to a peer-reviewed journal when they don't need to play the academic prestige game. TFA is an example of peer review in action: they're analyzing the proof and finding points to criticize.
not submitting to whatever journal is quite different than saying they are "beyond peer review"
are people not reviewing openai claims right now?
People described the problems as solved the minute they were made public.
this happens in approximately every scientific field. ive never heard it described as "idea that they are beyond peer review".
openai themselves specifically call out that there may be issues with their results. journalists and laypeople just happen to skip that part, like they do with ~all physics, health, astronomy, etc results.
You are confusing two levels of indirection here.
Peer review is a proxy for correctness.
Peer review journal is a proxy for quality peer review, or at least it was, once upon a time.
Because they want to release everything on github so everyone can peer review it themselves
This is far more efficient and they’re telling the academic industry to grow up
Sister comments are saying that academics dont like the Lean programming language and see a lack of human language described proof. Doesn’t sound like something I should care about but I’m watching for a better human language description of the problem as this discussion evolves
"not interested in" != "beyond"
I've seen a lot of breathless reporting about various mathematical things being "proven" on the basis of the LLM-generated Lean formulation compiling. We probably wouldn't declare that for a human-written proof until peers had checked the proof for errors
This. The proof of Fermat’s Last Theorem took 15+ months to check. It’s absurd to see the media reporting that these big problems are solved based off of a news release and a hastily and mostly AI-written manuscript, and OpenAI et al. are all too happy to run with said breathless reporting.
Wiles' proof was informal and couldn't be checked by a computer. In this case, the experts need to check 300 lines of Lean code (mostly comments) and confirm that it formalizes the problem statement correctly. There are papers building on the solution and analyzing it for more general versions of the problem, which suggests that the PDE community has already accepted it and moved on.
there's breathless reporting of just about everything scientific. physics, astronomy, archaeology, etc. have this sort of thing all the time.
yet i have never seen anyone say "the idea that physicists are beyond peer review is harmful" because some mainstream news articles published a piece about dark energy or whatever.
Exactly. Coverage here is "OpenAI has solved problem X", not "OpenAI has claimed to solve problem X."
Anyone who doesn't understand peer review (its intended workings, its negative effects by implementation flaws, etc.) automatically assumes expression is beyond academic peer review, so thats potentially a lot of people...
So my guess is that they have the AI system attempt to prove the theorem in natural language, then try to generate a Lean proof for it, and in that process they end up with a slightly different solution as the autoformalizer is essentially rewriting the NL proof to make it formalizable? Do we just need a "reverse pass" to re-align the NL proof with the Lean code?
Also, it doesn't seem that they are questioning the truthfulness of either proof, just that they are different?
Generating the lean proof first is a viable approach as well followed by an explanatory pass.
Actually, they are questioning whether the natural language description of the proof is either not faithful to the formal proof, or simply wrong, or both.
Not a mathematician. Why not just always use LEAN? Why use natural language at all?
Because it is really hard to read and the level of detail is so high that even lemmas that you can read may have such enormous levels of detail that makes real understanding difficult given that humans have limited working memory.
Why not always write machine code? Why use programming languages at all?
If a programming language compiler isn't guaranteed to be re-producible, then yeah, you'd have to revert to machine code.
The same JavaScript code compiles to different machine representations under different browser engines; yet webdevelopers don't need to learn assembly.
There is an abstract javascript machine which can obviously be translated to hardware instructions. "Obvious" in the mathematical research sense, as in the statement is flat out wrong under closer inspection. Websites regularly crash under memory pressure.
But they are good enough most of the time, and that's the key. With more resource a more correct program can be created, but cost-benefit calculations show a ceiling. A local pet store does not have the money to pay 2000 hours of formal verification work, and usually a WordPress site is good enough.
Mathematicians work with their brains. They have finite time to understand papers. Formalists say that all theorems could be reduced to logical axioms, but most of time it's jumping at a much higher level, because no one has time for minute details. Proofs are theoretically right or wrong, but in practice there are "slightly wrong" proofs, where there are some minute errors that "feels" like can be correcte, and most of the time it can be. This ambiguity is not a problem, but a feature of mathematics, because it means more time can be spent to move faster at a higher level of abstraction, but this would be lost with Lean.
Lean is a write only programming language.
Same reason humans write code not only for a compiler to translate into machine code but also so other humans can understand what we write, learn from it, modify it etc...
Not only that, we also have code comments and standalone documentation.
A programming language, when compiled, is a guaranteed reproducible result. If you recompile a program, you get the same thing each time.
The point of the article is that natural language is not these things.
Because people need to understand what is being proven.
The example in Figure 1 should help understand why... the NL version is much more approachable for humans.
If its ambiguous or wrong, then what are you understanding ?
Is not a natural language (NL) proof a demonstration of mastery and understanding?
If you understand the Lean, then you can create a NL proof. The LLM clearly doesn't understand the Lean code it produced.
ok
From the first example, it seems like this paper is so contrived. They pose a statement (y = x^3 - x^2 - 1 + 1 when x > -1) which is true, then provide incorrect reasoning but swapping the multiplicity of -1 and 1, then ask it to provide a proof. Essentially, they are running an injection attack; they give it 90% correct information, then it expects in good faith that -1 and 1 are not swapped, so it takes it verbatim. I don't see how the fact that ChatGPT can sometimes get this wrong, especially when the user is the bad actor trying to trick the computer and isn't actually trying to find a proof, is at all relevant to the Navier-Stokes solution.
I don't think that's an accurate summary of what this paper or its abstract actually claim.
Okay, but if they write another open letter or give another keynote proclaiming the end of the world then you owe me a beer.
TL;DR:
It seems the AI wrote code in Lean that proves there are solutions to Navier-Stokes that can blow up, but...
the AI's explanation of the code, in natural language, does not correspond to the Lean proof!
That is... so rich in irony.
> In particular, we highlight that the problem of resolving ambiguities in mathematical NL text, which is necessary in order to provide semantically faithful translation
This is what I've been wondering about with LLM proofs. Math is logical, but mathematical writing is still natural language: symbols get overloaded, conventions go unstated, and a lot rides on context. So a model can translate a statement into a formal system and prove it, and the proof can check out, while the statement it proved isn't quite the one the mathematician meant. I read this article as a caution that some of the LLM proofs announced so far may not hold up once a human checks what was actually proved. Is that a fair reading?
Edit out vulgarity
Natural language is ambiguous, but the Lean formalization is very well defined and unambiguous.
It's not the form language that is the real problem here. It's the ambiguity on the other side and the extreme difficulty of doing a useful and accurate translation.
> the downvotes will show many disagree
> gotcha bitch!
You may have misdiagnosed the problem.
This shouldn’t be a surprising result. We’ve known almost since LLMs became a thing that they can “prefer” modifying the terms or context of a problem when they can’t solve it directly (what one might call “cheating” if there were any volition involved). Often that happens in a way that isn’t immediately obvious to the user.
Before it was dropping databases or deleting repositories. Now it’s subtly changing the meaning of math problems to get a correct but irrelevant answer.
No one is disputing the correctness of the lean proof, the problem is that they did a bad job converting it to natural language.
Actually, as an earlier commenter noticed, it seems that the proof was done in natural language, and only then translated to Lean, as https://openai.com/index/navier-stokes-solution/ says:
> 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.
So it suggests that the formalization/verification step may have fixed some issues in the natural language proof, and either such differences were never noticed or the corrections weren't ported back to the NLP.
I am also not disputing the correctness of the Lean proof. I even emphasized this in my comment: “correct but irrelevant”.
Oh, well. I suppose I should avoid getting involved in these AI threads, but now it’s about half the forum.
Indeed. I've never used AI to translate between natural language and Lean but I have gone from English to Golang, Python, Typescript and SQL and its interpretations can be... creative, let's say.