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.
omnicognate 16 minutes ago [-]
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.
kzrdude 11 minutes ago [-]
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.
mkarrmann 10 minutes ago [-]
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.
fasterik 2 minutes ago [-]
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.
nicf 14 minutes ago [-]
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.)
pohl 19 minutes ago [-]
> has not formalized the original "natural language" idea of Navier-Stokes incorrectly
Did you mean “not…correctly”?
OhNoNotAgain_99 18 minutes ago [-]
[dead]
j2kun 49 minutes ago [-]
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.
fasterik 31 minutes ago [-]
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".
abstrakraft 19 minutes ago [-]
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".
fasterik 13 minutes ago [-]
That's not the claim made in TFA. See the sibling comments, in particular about the DeepMind Formal Conjectures encoding.
28 minutes ago [-]
Arodex 24 minutes ago [-]
>we provide several examples of AI mistranslations of NL statements and proofs into Lean in practice, resulting in mismatches between NL proofs and their Lean `verifications'. These include OpenAI's announced Navier-Stokes proof. 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.
Maybe read the original article before replying, at a minimum.
fasterik 19 minutes ago [-]
Does that contradict what I said? Right there in your quote, it says that the NL proof does not correspond to the Lean proof. However, the statement of the theorem in Lean is not derived from the NL proof. It comes from DeepMind's formalization of the Navier-Stokes Millennium problem, which as far as I'm aware nobody disputes.
j2kun 21 minutes ago [-]
Both proofs may be correct, and the problem may indeed be solved. My point is that it should not be assumed.
kurtis_reed 17 minutes ago [-]
> Maybe read the original article before replying, at a minimum.
Maybe read the comment before replying, at a minimum.
john_strinlai 44 minutes ago [-]
>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?
abdullahkhalids 31 minutes ago [-]
OpenAI has expressed this sentiment by not submitting to or saying they will submit their results to peer reviewed journals.
fasterik 25 minutes ago [-]
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.
abdullahkhalids 59 seconds ago [-]
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.
1234-1298 4 minutes ago [-]
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.
j2kun 19 minutes ago [-]
I would say it's released in the spirit of machine learning's competitive landscape (which is the culture this emerged from).
13 minutes ago [-]
john_strinlai 27 minutes ago [-]
not submitting to whatever journal is quite different than saying they are "beyond peer review"
are people not reviewing openai claims right now?
yieldcrv 26 minutes ago [-]
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
setgree 27 minutes ago [-]
"not interested in" != "beyond"
swiftcoder 30 minutes ago [-]
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
fatcatsbestcats 23 minutes ago [-]
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.
john_strinlai 8 minutes ago [-]
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.
j2kun 24 minutes ago [-]
Exactly. Coverage here is "OpenAI has solved problem X", not "OpenAI has claimed to solve problem X."
This is so lovely. I desperately wish I could color code all math!!
stared 33 minutes ago [-]
You can. Not only the code is there, but also an interactive editor.
buzzy_hacker 55 minutes ago [-]
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?
caughtinthought 52 minutes ago [-]
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."
hyperpape 46 minutes ago [-]
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?
ammar2 46 minutes ago [-]
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.
empath75 46 minutes ago [-]
> 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.
latent-person 22 minutes ago [-]
> 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.
Yeah, I was surprised some people think LLMs are reasoning in Lean directly... all their training data is in NL.
ammar2 7 minutes ago [-]
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.
caughtinthought 38 minutes ago [-]
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.
OrderlyTiamat 48 minutes ago [-]
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?
ndriscoll 30 minutes ago [-]
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.
nyeah 21 seconds ago [-]
[delayed]
25 minutes ago [-]
jansport123 38 minutes ago [-]
syntax vs semantics
jrflo 38 minutes ago [-]
It doesn't look like they've found an error in the NL proof either, just that they are different?
kccqzy 27 minutes ago [-]
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.
16 minutes ago [-]
kurtis_reed 16 minutes ago [-]
How do you know the natural language proof is incorrect?
zmgsabst 44 minutes ago [-]
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.
kurtis_reed 13 minutes ago [-]
Yes however, whether a natural language proof and a formal proof "correspond" is subjective.
empath75 48 minutes ago [-]
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.
Sniffnoy 13 minutes ago [-]
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.
notrealyme123 23 minutes ago [-]
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?
skywalqer 16 minutes ago [-]
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.
jcranmer 16 minutes ago [-]
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).
ezwoodland 20 minutes ago [-]
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.
hypersoar 19 minutes ago [-]
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.
arbirk 34 minutes ago [-]
It was a piston in a non-compressible fluid so to speak (ie. storm in a glass of water)
129983-asf 17 minutes ago [-]
Two leading experts on Navier Stokes still do not know whether their methods were used:
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.
jrflo 44 minutes ago [-]
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?
ted_dunning 32 minutes ago [-]
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.
empath75 56 minutes ago [-]
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.
hgoel 7 minutes ago [-]
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.
ted_dunning 39 minutes ago [-]
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.
ndriscoll 14 minutes ago [-]
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.
dekhn 38 minutes ago [-]
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.
FrustratedMonky 41 minutes ago [-]
Not a mathematician. Why not just always use LEAN? Why use natural language at all?
ted_dunning 35 minutes ago [-]
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.
matusp 34 minutes ago [-]
Why not always write machine code? Why use programming languages at all?
caughtinthought 24 minutes ago [-]
The example in Figure 1 should help understand why... the NL version is much more approachable for humans.
jansport123 37 minutes ago [-]
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...
Jaxan 32 minutes ago [-]
Not only that, we also have code comments and standalone documentation.
binlog 36 minutes ago [-]
Because people need to understand what is being proven.
Jtarii 33 minutes ago [-]
Lean is a write only programming language.
35 minutes ago [-]
le-mark 57 minutes ago [-]
> 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
ted_dunning 37 minutes ago [-]
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.
hyperpape 50 minutes ago [-]
> the downvotes will show many disagree
> gotcha bitch!
You may have misdiagnosed the problem.
52 minutes ago [-]
ballmerpoint 50 minutes ago [-]
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.
sebzim4500 33 minutes ago [-]
No one is disputing the correctness of the lean proof, the problem is that they did a bad job converting it to natural language.
ForHackernews 43 minutes ago [-]
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.
Rendered at 17:20:28 GMT+0000 (Coordinated Universal Time) with Vercel.
"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.
Did you mean “not…correctly”?
The idea that an AI company is beyond peer review is harmful.
Maybe read the original article before replying, at a minimum.
Maybe read the comment before replying, at a minimum.
i havent seen this sentiment expressed anywhere, have you?
isn't this comment chain on a submission about openai's claims being reviewed?
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.
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.
are people not reviewing openai claims right now?
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
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.
From the paper: "A third possibility is that the NL proof provides stronger statements than what the formal proof actually establishes, with (of course) different proofs. The latter happens in OpenAI’s announced proof of blow-up of Navier Stokes equations."
What the examples seem to show is that the proof method is different between the natural language proof and the lean proof. Which, if the lean proof actually proves blowup, would suggest that the natural language proof is subtly wrong, but the strategy was close enough to be used to create a real lean proof.
A little worrying, but part of the purpose of formalizing things in Lean, it forces you to be more accurate than natural language does. It's surprisingly common for major theorems to have slight inaccuracies early on that can be repaired. Famously, the initial proof of Fermat's Last Theorem had a flaw that took a year to repair (though I think that's unusually difficult).
So the most fundamental question is: does the Lean theorem faithfully state the right theorem?
For what it's worth the initial lean specifications for the top-level theorems generally come from human written formalizations such as in https://github.com/leanprover-community/mathlib4/blob/021ce6... so we can be reasonably confident about their correctness.
No, the other way around. The natural language proof was derived from the lean code, badly. This is my experience with using claude and lean to prove things. Its natural language explanations drift a lot from the lean, both before and after. But the lean code is the lean code.
Was it? Are you claiming a LLM does reasoning in lean or what? Since this (and all the other proofs by OpenAI etc) have been in the reverse order [1]:
> The agents arrived at their resolution on Saturday, September 5, about 88 hours after the first agents were launched. Lean formalization and verification took an additional 17 hours via GPT‑6 Astra.
[1]: https://openai.com/index/navier-stokes-solution/
That is definitely interesting because how do you know the 88 hours of work are correct before you throw another 17 hours of lean formalization work on it? You could end up just finding out there was some hallucination in the original work.
If your code compiles, are you sure it's bug free?
Humans have made similar mistakes too. A human writes a specification for how things should work, the human translates that into code, the code does not work, and finally the human fixes the code and forgets to fix the original spec.
So the Lean proves something and the question is whether that something is actually what we care about — or something similar, but ultimately not the question.
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.
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.
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.
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.
We should be very careful about relinquishing sorting through such details to AI.
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.
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
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.
> gotcha bitch!
You may have misdiagnosed the problem.
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.