OpenAI’s Navier-Stokes release included a Lean 4 formal proof
OpenAI’s claimed solution of a Navier–Stokes Millennium Prize problem using large language model “agent swarms” and a Lean 4 formal proof is prompting both awe and skepticism. Commenters weigh the technical feat and the promise of automated proof formalization against massive compute costs, questions about whether AI plagiarized or overly relied on human researchers’ work, and the risk that math becomes something machines do without improving human understanding. Many also probe how much trust to place in formal verification tools like Lean, what bugs or mis-specifications could still invalidate results, and whether such negative existence proofs have real-world physical applications.
Cost and Efficiency of AI vs Human Formalization
- Thread disputes the “four orders of magnitude” savings claim: back-of-envelope estimates suggest ~$40M compute vs ~$130M human labor, still huge but smaller gap.
- Some argue the classic “40 hours per page” for formalization is outdated due to better automation and libraries; others defend it for complex research-level material.
- Coordinating ~1M hours of human effort is seen as practically impossible compared to a large agent swarm.
Lean, Autoformalization, and Performance
- Many note that modern Lean + mathlib dramatically reduce effort for undergraduate-level material, but deep research proofs still require enormous work.
- Lean is considered slow at this scale (e.g., multi-day, 230 GB verification), though several point out that agent generation ran massively parallel while verification was likely mostly single-machine.
- Discussion of optimizing Lean’s kernel and proving optimized versions equivalent to the simple one; projects that reimplement Lean in Lean are mentioned as a path.
Verification, Trust, and Possible Bugs
- Consensus: if axioms and theorem statements are correct, a checked Lean proof is highly trustworthy; the main risk is misformalizing the statement, not the internal proof steps.
- Some note Lean has had kernel bugs in the past; an AI could in principle exploit such a bug instead of truly proving the theorem.
- Concern about “adversarial” formalizations that subtly change definitions; checking the theorem statement and assumptions remains a human responsibility.
Ethics, Plagiarism, and Data Use
- Large subthread on whether the AI’s key ideas were “plagiarized” from researchers who used earlier models, especially via training on private chats.
- One side: timeline and problem variants suggest the AI solved harder cases and that recent private work could not have been in the training run.
- Other side: anonymization and mixing of user data make it “impossible to know” what influenced the model; distrust of lab ethics amplifies suspicion.
Significance, Understanding, and Value
- Some are amazed that a general model can both solve and formally verify such a problem; others worry the result is “one bit of information” with little accompanying human understanding.
- Critique that big AI labs chase headlines, not deep mathematical exposition, and that they don’t answer follow-up questions or integrate with the broader mathematical community.
Practical Impact of the Navier–Stokes Result
- Debate over real-world relevance: some think this negative result mainly shows Navier–Stokes is an imperfect physical model; others see limited immediate applications.
- Comparison to paradoxical or highly contrived examples in pure math; skepticism that such singularities matter for engineering or turbulence modeling.
Broader Reflections on AI and Mathematics
- Mixed emotions: excitement about autoformalization and future work on problems like the abc conjecture, but also anxiety that human mathematical creativity is being “mechanized.”
- Worries about future AI-generated proofs that humans cannot feasibly check without immense compute, and about potential attacks on formal verification toolchains.