Navier–Stokes Lost in Translation
A new paper claims AI autoformalization tools can subtly alter mathematical proofs when translating from natural language to formal systems like Lean. This "lost in translation" effect, which reportedly impacted OpenAI's much-hyped Navier-Stokes solution, highlights the profound ambiguities inherent in human mathematical language. The Hacker News community debates whether this undermines AI-generated proofs or merely emphasizes the need for careful human oversight and improved AI transparency.
The Lowdown
This paper investigates the semantic fidelity of AI autoformalization, the process by which AI systems translate natural language (NL) mathematical texts into formal languages, such as Lean, for mechanical verification. The authors argue that this translation process is fraught with difficulties, specifically claiming that resolving ambiguities in mathematical NL to achieve semantically faithful translation is computationally intractable, even harder than the Halting problem.
Key findings and arguments include:
- The fundamental challenge of translating ambiguous natural language mathematics into precise formal systems.
- Empirical evidence showing AI mistranslations of NL statements and proofs into Lean, leading to mismatches between the original NL arguments and their formal "verifications."
- A direct assertion that OpenAI's highly publicized Lean proof of the Navier-Stokes equations' blow-up does not, in fact, correspond to its companion natural language proof. The paper clarifies it's not questioning the correctness of OpenAI's NL proof but rather the mistranslations into Lean.
- The authors' work suggests that while an AI might produce a formally verifiable Lean proof, that proof may address a subtly different problem or follow a different logical path than its purported natural language origin, thereby failing to offer confidence in the original NL argument.
In essence, the paper serves as a significant cautionary tale, suggesting that the mechanical verification of AI-generated formal proofs does not automatically validate their natural language counterparts, calling into question the reliability of AI as a direct translator and validator of complex mathematical reasoning.
The Gossip
Proof's Perplexity & Precision
The central debate revolves around the paper's core claim: is the Lean proof wrong, or just different from the natural language (NL) proof? Many commenters clarify that the Lean proof itself is likely valid for the theorem it states, which is generally believed to be the Clay Institute problem statement. The issue is whether the path taken by the Lean proof truly reflects the NL proof's logic, or if the AI "tweaked" the proof during formalization. There's also discussion on whether OpenAI's AI first generated the NL proof and then formalized it, or vice versa, influencing the perceived "translation" direction.
Natural vs. Formal Nuances
This theme explores the inherent tension between the expressive power and inherent ambiguity of natural language in mathematics versus the strict, unambiguous rigor of formal proof systems like Lean. Commenters discuss why humans still rely on NL for mathematical discourse (readability, intuition, abstract thinking) despite its imprecision. Many share anecdotes of uncovering errors or ambiguities in human-written papers only when attempting formalization, suggesting that AI might be doing the same, perhaps without fully realizing or communicating the semantic shifts.
OpenAI's Overtures & Oversight
The discussion often veers into critique of OpenAI's method of announcing mathematical breakthroughs, particularly the perception that they sidestep traditional academic peer review processes. Commenters debate whether simply releasing Lean code on GitHub constitutes sufficient "peer review" or if it implies a dangerous "beyond peer review" mentality from AI companies. Some express cynicism about OpenAI's claims and marketing, suggesting alternative explanations for how the proofs might have been generated or that the focus is on speed over rigor and communication.
Gödel's General Grievances
A subset of the discussion touches upon Gödel's Incompleteness Theorems, with some commenters initially wondering if they pose a fundamental barrier to complete mechanical verification. However, others quickly clarify that Gödel's theorems apply to provability within a system, not the mechanical checking of a given proof's steps or the fidelity of a definition. The consensus is that while a system cannot prove its own consistency, it can still rigorously verify specific proofs against established axioms, and that the kernel of such systems can be made small enough to trust.