Agreed. It'd be super cool to see a Firefox/Chrome extension look for Latex equations on sites you were browsing and then cross-reference them against wiki/etc. and give them the math-equivalent of syntax highlighting.
Even more so if it worked with PDFs.
I already have way too many projects on the backburner right now... wink wink nudge nudge to anyone who wants to take this.
Math was always difficult for me because I felt lecturers in general knew a lot more than they were telling me. Maths may be logical but at the end of the day mathematical notation is a natural language and can be very ambiguous. I think this is self evident but the downvotes will show many disagree. Can the present article be classified as “gotcha bitch!”? I think so.
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.
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.
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.
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.
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.
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.
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?
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?
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.
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.
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 struggle to solve it (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.
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.
> 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 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".
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.
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.
Yeah, and if you re-run the same program with the same bug, it will fail the same way each time. It is reproducible. What are you even trying to argue about?
And to the point of the original article. Each human interpreting natural language is a new environment. Each brain is a new compiler with different outcomes. Thus the ambiguity. Natural language isn't concrete enough to always have the same result when processed by different humans, or AI.
I guess I misunderstood the paper, that natural language proofs are not mastery/understanding because they can be flawed. Natural language can be misinterpreted enough that it is not a given to be correct.
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.
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).
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.
I think lean can verify it implements its own rules, but not that its own rules are sound (you can't prove a contradiction). If you are just prepared to trust that the rules are sound, then you would be able to trust leans implementation (if you had that Lean proof that it implements its own rules)
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 incorrectly, so 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.
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?
They are claiming that the NL proof and the Lean proof are not consistent though: the NL proof is not being validated by the Lean proof, and the Lean proof is not being "explained" by the NL proof.
Yes it could be that neither the NL proof nor the Lean proof correspond to the actual Navier Stokes problem. Here's a quote from the paper--
"Remark 3.4 (Further potential mistranslations of the Navier-Stokes proof). The above examples require careful manual checking of both the NL proof as well as the Lean proof, which is delicate and highly time consuming. Moreover, the fact that we display only two examples does not mean that these are the only cases of mistranslations."
The proof is about one of a multitude of possible theorems you could prove about the Navier-Stokes equation. Nobody is claiming that the Navier-Stokes equation itself is misformalized. Rather, they are claiming that what the theorem they proved says about Navier-Stokes is misformalized, in the sense that it's a different theorem than the one informally proven in the natural-language proof.
But nobody is claiming that it's a theorem about a misformalization of the Navier-Stokes equation rather than about the Navier-Stokes equation itself, and nobody is claiming that the theorem they proved in L∃∀N isn't proven. Except random ignorant commenters on Hacker News.
I don't know why this is so difficult. It seems like a lot of commenters here have the reasoning ability of GPT-3, possibly because they're extremely drunk or sleep-deprived, or are actually GPT-3.
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.)
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.
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?
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.
Yes, you are misunderstanding what the paper claims. Navier Stokes for example is not such an example, only the proof is different. For their other examples, none of them they claim that they concern actually the open ai solved theorems. You are welcome.
In case you are not aware, the actual theorem statement of N-S was never translated by an LLM, but was written independently by formal conjectures, as they say in the README [1].
A Lean proof has a much higher probability of being correct (in my opinion) than any published (either preprint or peer-reviewed) paper, yet no one before LLMs were walking around claiming every result published can't be trusted yet (without an actual reason).
We have seen one such instance of Lean bugs, which was found adversely against Lean (as in find bug then use this bug to prove Collatz, not just found when being asked to prove it).
It's also worth to note that the way N-S (and all the other proofs by OpenAI etc) have been found is first prove it in NL then translate to Lean. I.e. it would have to first believe it found a correct proof in NL, and then afterwards either accidentally or on purpose use a Lean kernel bug.
2. No exploit of a kernel soundness bug in Lean (and the independent kernel nanodo, which OpenAI also checks against).
In particular, if you trust this, then you don't need to care about anything else the Lean program does, no matter how many lines, lemmas etc. it makes along the way.
As I said above, the theorem statement have been written independently by formal conjectures, and you are free to read it yourself (or trust other people have done it).
So, assuming you don't disagree the theorem statement have been written correctly, you pretty much need to believe 2 is false, if you don't trust the proof [1]. And that's what I find has a rather low probability personally.
[1] As the book says, you also need to trust the hardware, compiler etc.
You may be overconfident here. The NL paper may be properly stating the Navier Stokes problem, and the Lean code may not be.
Here's from the paper--
3.1. When the NL paper declares stronger statements than what Lean proves
We commence with an example that complements those in §2. In the following example the AI autoformalisation results in a different Lean proof of a weaker statement.
None of the examples are of the NS lean statement. The validity of the latter is not under question ( in this paper ). Please note the distinction between “statement of NS” and “statement of lemmas used in the NL proof of NS”.
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.
Why do people program in Python instead of writing machine code?
Why are review papers published? Executive summaries? "Introduction to X" books?
People's time and computational resources are finite. Summarising information -- ideally in structured ways that preserve important properties, but even in informal, unstructured ways -- is critical for making any kind of progress in this world.
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.
Everyone. I don't think many people working in fluid dynamics were surprised you can find a blow-up in Navier-Stokes. What would advance human knowledge is understanding the situations in which a blow-up might occur. In that context, the lean proof is necessary, but the non-lean proof is more important.
The statement written in Lean, is not actually a correct description of the Navier-Stokes problem. It's some other easier statement. That's why the Lean code may not be a proof.
Here's a quote from the paper. "In the following example the AI autoformalisation results in a different Lean proof of a weaker statement."
So the question is, was the Navier-Stokes problem framed properly in the lean code, or is some easier problem represented in the Lean code?
The "statements" here are statements of lemmas, not the statement of the main theorem. The main theorem statement was written by humans (prior to the OpenAI work), so there shouldn't be any concern that an AI mistranslated it.
My point is that Astra did not write the statement of Navier-Stokes in Lean, there was already a human-written statement, so there should be no concern that it has errors.
This article shows that we can't conclude from the working Lean proof that the NL proof is also correct, because they are different in some places. On the other hand I think it's unlikely that it's "very" broken. OpenAI first spent a lot of computer time to find the NL proof, and then less time to translate it into Lean. So if there were errors in the NL proof it seems they were not fatal, the agent translating it into Lean was able to patch them up as it went along.
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?
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.
I don’t. But I do know how the scientific method works, and OpenAI’s display is anything but. Until what they have demonstrated is reproduced I take their claims to be nothing but marketing. A for profit company will lie in order to maximize their profits. Above I presented an alternative hypothesis, which is probably wrong, but until OpenAI’s results are replicated I will believe my alternative hypothesis just as much as I believes the claims of the for profit company making them.
It's the method they used to create the proof that's in question here. They claim their amazing product did it, and therefore you should buy their product because will do amazing things for you too!
In the absence of evidence, a guess is the best you got.
And, no until OpenAI’s results have been replicated, I don‘t believe companies own words about their own products, and therefor a marketing statement is not evidence.
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.
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.
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.
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)
e.g. one of the lemmas in the NL description is false, but a weaker version of the lemma (that does hold) is sufficient for the proof, so the (incorrect) lemma is never formalized.
Why do you assume this order? I would assume the AI starts with lean (that's what it was RL'd on at least) then tried to translate the proof for us humans, which is quite hard.
I'm not sure about it but it seems plausible given the potential error.
Edit: they explicite say that your order is correct in the post
Proof steps can become different in Lean but still work to prove the theorem. Incorrect proof steps in the NL paper could also be converted to correct ones in Lean. The paper shows some examples of this. So the NL paper can't be trusted even if Lean verification passes, but it doesn't immediately mean that the NL proof is wrong or that Lean is checking the wrong thing.
>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. That doesn't give us any new information about whether the generated Lean proof is or isn't valid.
This doesn't answer the question. The question was: what was the difference in A and B. Your answer looks like this:
A: The English language description doesn't do the same thing as the code the AI wrote.
B: The English language description doesn't do the same thing as the code the AI wrote.
A and B are the same; there is no difference. Is this what you meant? Or did you mean the opposite of this? If you meant the opposite of this, what exactly is the difference?
They published both a natural language proof and a lean proof. This paper says the NL proof does not match does not match the lean proof, using different arguments and some stronger claims. It does not claim the lean formulation of NS or the rest of the lean proof is invalid.
"The Lean code merely tells us that the theorem is correct, yet the NL proof with intermediate arguments, lemmas and results may be incorrect or have incorrect arguments."
You didn't answer the question. Quoting from upthread:
A: "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."
B: "No, they're not claiming that [...] The authors are claiming that the Lean proof is not the same proof as the NL one"
The question was: what's the difference between A and B?
Your answer to that question was "This paper says the NL proof does not match does not match the lean proof".
It seems to me like A is the exact same thing as B, and you are here claiming that they're different things while merely repeating the same claim that was already claimed in both A and B.
Statement A is upthread quoting the paper, and is not the statement B is arguing against. B is arguing against the incorrect statement "So these authors seem to be claiming that OpenAI has not really proven Navier-Stokes at all."
3) The comments promise functionality the code does not implement.
The first post was "It doesn't meet the business requirements the comments indicated, so the software is broken." The replying post was "Actually, the business requirements were faithfully turned into tests, so the software is fine. The comments need to be rewritten"
> No one is disputing that the Lean formalization of Navier-Stokes is correct, so we should have high confidence that the generated Lean proof is valid.
Why? It is a correct proof. Is it a correct (dis-)proof of NS? These statements do not seem particularly related. People, including (especially?) mathematicians, find NL proofs far easier to read than Lean proofs. I would bet the ratio of people who read (part of) the NL proof vs the Lean proof is at least 100 to 1. It seems incredibly unlikely that anyone has read and reviewed the whole Lean proof (including the authors of the OP).
Is it particularly easy to see that the Lean proof does actually disprove NS, rather than proving something similar but not the same?
Well the theorum statement (what it proves) is short and easy to verify. I would not be surprised if hundreds of mathematicians have looked at it at this point.
Which is exactly why you want a Lean proof in the first place!
NL proofs rely on not-entirely-correct prior art, and contain countless holes both big and small. When formalizing human NL proofs it is probably very normal that the Lean proofs doesn't quite follow the NL proof.
My understanding is that the statements in the Lean proof might not actually correspond to the Navier-Stokes problem. And that requires mathematical insight to be able to verify, which could take quite a while.
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.
The formal statement that Astra proved was written by a human, submitted to a DeepMind repository and reviewed by humans in a pull request. It's completely independent of OpenAI's effort. No PDE expert or formal verification expert has disputed it as far as I'm aware.
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.
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.
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.
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.
- 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.)
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.
This is a bit delicious if I understand it correctly.
They managed to find an excuse not to bother checking. They're saying that they refuse to verify the English paper because the lean had to be slightly changed to compile so there isn't a perfect 1:1 between the English paper and the compiled code.
They're also saying that this ipso facto means that it is impossible for AI to ever prove anything that can be then verified by humans via any submitted English papers because they will reject all papers that are associated with a lean conclusion.
If they don't verify the solution, it isn't solved according to the math world. Their careers are defended and they can all stick their heads in the proverbial sand and act like the math isn't solved.
I was pointing out that your original comment (before you edited it to just say "ok") did not properly represent the claims of this paper.
I am not making any claims about mathematicians as a collective group, because mathematicians have many diverse views on AI and can't be lumped together into a single "they" (as your comment seems to imply that they can). In fact, some academic mathematicians even work for the AI companies. Your comment seems to imply that if a group of mathematicians publish some statement, then that statement must speak for all mathematicians, but that's simply not true.
The association for Human Mathematics (AHM) criticized OpenAI's release of 722 math manuscripts and urged mathematicians "to discontinue their work with OpenAI." And, Terence Tao reposted AHM's statement on his blog.
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.
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.
We talk about the AI proof while people are not focusing on the fact that AI had much more access to knowledge for three reasons.
The first is that it filtered out rubbish. Yes, there is so much rubbish papers out there while good ones are lost in noise.
The second is that it ingested data from countless journals. The average researcher does not have this level of access because of monetary obstacles.
The third is that AI can process large amounts of data because of hardware availability.
AI is not that clever as people try to make it appear. All the above show problems in our society that AI does not solve. It just takes advantage of them to pass as a mister-know-it-ll.
183 comments
[ 0.16 ms ] story [ 16.1 ms ] threadMore interesting, you can ask a vision model to color parts of speech in img2img and it works OK for frontier models.
Even more so if it worked with PDFs.
I already have way too many projects on the backburner right now... wink wink nudge nudge to anyone who wants to take this.
I don’t think that actually explains the idea of a momentum density transport equation well at all.
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 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.
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 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.
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've been criticized for doing this, but to me it emphasizes how much attention goes to the hot, wrong papers.
We should be very careful about relinquishing sorting through such details to AI.
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?
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.
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.
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.
The idea that an AI company is beyond peer review is harmful.
that's not the claim. the formal statement of the problem for the NS proof was written by humans not autoformalized.
Also, it doesn't seem that they are questioning the truthfulness of either proof, just that they are different?
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.
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.
That he jotted in a margin that he had just seen a simple proof, and would write it down later. And we spent a hundred years trying to reproduce.
Or some other joke about a mathematician will put "and here we see it simply follows" or some such.
I'm all for abstraction, I get the point.
But for natural language it seems like " I saw my ex boyfriend last night and, yada yada yada, I'm really exhausted this morning".
See, the yada-yada is a bit too much abstraction.
Guess I'm missing the point of the paper, I thought it was trying to show that natural language is flawed and formalized systems are better.
[Citation needed]
2 + 2 = 5 -> Error
Every time.
The environment does matter. I think in your original objection, you were executing the code in different environments.
https://cs.stackexchange.com/questions/38152/what-is-determi...
And to the point of the original article. Each human interpreting natural language is a new environment. Each brain is a new compiler with different outcomes. Thus the ambiguity. Natural language isn't concrete enough to always have the same result when processed by different humans, or AI.
> the answer with many multi-threaded programs is often "no."
Isn't the original point, that natural language isn't sufficient for proofs? Aren't you agreeing now?
If you understand the Lean, then you can create a NL proof. The LLM clearly doesn't understand the Lean code it produced.
Can someone tell me in simple terms why this doesn't conflict with the incompleteness theorems?
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.
(The algorithms described above are of course completely impractical, taking time exponential in the length of the proof (of theorem or counterexample).)
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.
"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 incorrectly, so 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.
Did you mean “not…correctly”?
"Remark 3.4 (Further potential mistranslations of the Navier-Stokes proof). The above examples require careful manual checking of both the NL proof as well as the Lean proof, which is delicate and highly time consuming. Moreover, the fact that we display only two examples does not mean that these are the only cases of mistranslations."
This has nothing to do with whether the lean proof certifies (the real) NS.
But nobody is claiming that it's a theorem about a misformalization of the Navier-Stokes equation rather than about the Navier-Stokes equation itself, and nobody is claiming that the theorem they proved in L∃∀N isn't proven. Except random ignorant commenters on Hacker News.
I don't know why this is so difficult. It seems like a lot of commenters here have the reasoning ability of GPT-3, possibly because they're extremely drunk or sleep-deprived, or are actually GPT-3.
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.
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?
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.
A Lean proof has a much higher probability of being correct (in my opinion) than any published (either preprint or peer-reviewed) paper, yet no one before LLMs were walking around claiming every result published can't be trusted yet (without an actual reason).
We have seen one such instance of Lean bugs, which was found adversely against Lean (as in find bug then use this bug to prove Collatz, not just found when being asked to prove it).
It's also worth to note that the way N-S (and all the other proofs by OpenAI etc) have been found is first prove it in NL then translate to Lean. I.e. it would have to first believe it found a correct proof in NL, and then afterwards either accidentally or on purpose use a Lean kernel bug.
[1]: https://github.com/openai/NavierStokesAndEuler/blob/main/Com...
Define “correct” in this context. That’s the real problem here.
Here is what putting trust into a Lean proof means https://ammkrn.github.io/type_checking_in_lean4/trust/trust....
In particular the main ones are:
1. The theorem has been written correctly.
2. No exploit of a kernel soundness bug in Lean (and the independent kernel nanodo, which OpenAI also checks against).
In particular, if you trust this, then you don't need to care about anything else the Lean program does, no matter how many lines, lemmas etc. it makes along the way.
As I said above, the theorem statement have been written independently by formal conjectures, and you are free to read it yourself (or trust other people have done it).
So, assuming you don't disagree the theorem statement have been written correctly, you pretty much need to believe 2 is false, if you don't trust the proof [1]. And that's what I find has a rather low probability personally.
[1] As the book says, you also need to trust the hardware, compiler etc.
Here's from the paper--
3.1. When the NL paper declares stronger statements than what Lean proves
We commence with an example that complements those in §2. In the following example the AI autoformalisation results in a different Lean proof of a weaker statement.
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 are review papers published? Executive summaries? "Introduction to X" books?
People's time and computational resources are finite. Summarising information -- ideally in structured ways that preserve important properties, but even in informal, unstructured ways -- is critical for making any kind of progress in this world.
In order to prove security, you must first simulate the universe.
Everyone. I don't think many people working in fluid dynamics were surprised you can find a blow-up in Navier-Stokes. What would advance human knowledge is understanding the situations in which a blow-up might occur. In that context, the lean proof is necessary, but the non-lean proof is more important.
Here's a quote from the paper. "In the following example the AI autoformalisation results in a different Lean proof of a weaker statement."
So the question is, was the Navier-Stokes problem framed properly in the lean code, or is some easier problem represented in the Lean code?
"In all cases the correctness of the formal proof does not say anything about the correctness of the NL proof."
This article shows that we can't conclude from the working Lean proof that the NL proof is also correct, because they are different in some places. On the other hand I think it's unlikely that it's "very" broken. OpenAI first spent a lot of computer time to find the NL proof, and then less time to translate it into Lean. So if there were errors in the NL proof it seems they were not fatal, the agent translating it into Lean was able to patch them up as it went along.
If you think it's probably wrong, why believe it?
And, no until OpenAI’s results have been replicated, I don‘t believe companies own words about their own products, and therefor a marketing statement is not evidence.
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).
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.
"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.
> 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.
e.g. one of the lemmas in the NL description is false, but a weaker version of the lemma (that does hold) is sufficient for the proof, so the (incorrect) lemma is never formalized.
I'm not sure about it but it seems plausible given the potential error.
Edit: they explicite say that your order is correct in the post
These authors don't seem to be disputing that this Lean formalization of Navier-Stokes is correct. That doesn't give us any new information about whether the generated Lean proof is or isn't valid.
A: The English language description doesn't do the same thing as the code the AI wrote.
B: The English language description doesn't do the same thing as the code the AI wrote.
A and B are the same; there is no difference. Is this what you meant? Or did you mean the opposite of this? If you meant the opposite of this, what exactly is the difference?
"The Lean code merely tells us that the theorem is correct, yet the NL proof with intermediate arguments, lemmas and results may be incorrect or have incorrect arguments."
A: "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."
B: "No, they're not claiming that [...] The authors are claiming that the Lean proof is not the same proof as the NL one"
The question was: what's the difference between A and B?
Your answer to that question was "This paper says the NL proof does not match does not match the lean proof".
It seems to me like A is the exact same thing as B, and you are here claiming that they're different things while merely repeating the same claim that was already claimed in both A and B.
1) The code and the comments disagree.
2) The code passes the tests.
3) The comments promise functionality the code does not implement.
The first post was "It doesn't meet the business requirements the comments indicated, so the software is broken." The replying post was "Actually, the business requirements were faithfully turned into tests, so the software is fine. The comments need to be rewritten"
Why? It is a correct proof. Is it a correct (dis-)proof of NS? These statements do not seem particularly related. People, including (especially?) mathematicians, find NL proofs far easier to read than Lean proofs. I would bet the ratio of people who read (part of) the NL proof vs the Lean proof is at least 100 to 1. It seems incredibly unlikely that anyone has read and reviewed the whole Lean proof (including the authors of the OP).
Is it particularly easy to see that the Lean proof does actually disprove NS, rather than proving something similar but not the same?
NL proofs rely on not-entirely-correct prior art, and contain countless holes both big and small. When formalizing human NL proofs it is probably very normal that the Lean proofs doesn't quite follow the NL proof.
Is that exactly the same as saying the Lean proof isn't correct? I'm confused by what you're trying to distinguish.
There are a number of posts here that consider the correctness of the Lean code with high confidence. This paper I think weakens that confidence.
Generally I think we can agree we don't know if the NL proof is correct, or if the initial statement in Lean is correct. I suppose that's obvious.
https://github.com/google-deepmind/formal-conjectures/blob/8...
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.
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.
_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.)
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.
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...
They managed to find an excuse not to bother checking. They're saying that they refuse to verify the English paper because the lean had to be slightly changed to compile so there isn't a perfect 1:1 between the English paper and the compiled code.
They're also saying that this ipso facto means that it is impossible for AI to ever prove anything that can be then verified by humans via any submitted English papers because they will reject all papers that are associated with a lean conclusion.
If they don't verify the solution, it isn't solved according to the math world. Their careers are defended and they can all stick their heads in the proverbial sand and act like the math isn't solved.
I am not making any claims about mathematicians as a collective group, because mathematicians have many diverse views on AI and can't be lumped together into a single "they" (as your comment seems to imply that they can). In fact, some academic mathematicians even work for the AI companies. Your comment seems to imply that if a group of mathematicians publish some statement, then that statement must speak for all mathematicians, but that's simply not true.
The association for Human Mathematics (AHM) criticized OpenAI's release of 722 math manuscripts and urged mathematicians "to discontinue their work with OpenAI." And, Terence Tao reposted AHM's statement on his blog.
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.
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 with irony.
"Disclaimer: We do not make claims about the correctness of OpenAI’s NL proof, we only make statements about mistranslations into Lean."
The first is that it filtered out rubbish. Yes, there is so much rubbish papers out there while good ones are lost in noise. The second is that it ingested data from countless journals. The average researcher does not have this level of access because of monetary obstacles. The third is that AI can process large amounts of data because of hardware availability.
AI is not that clever as people try to make it appear. All the above show problems in our society that AI does not solve. It just takes advantage of them to pass as a mister-know-it-ll.