Did the computer prove the thing we actually meant?
- What it is
- A paper separates a computer-checked proof from a faithful translation of the original mathematics, gives precise complexity results, and reports mismatches in a Navier–Stokes formalization.
- Who did it
- Alexander Bastounis, Fabian Circelli, and Anders C. Hansen.
- What it could mean
- A proof checker can give the right answer to the wrong question. This work puts that translation risk under the microscope; it does not declare the Navier–Stokes result false.
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Read the original work
Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs ↗See the proposed checks
Review A.4's quantified predicate and reduction, then inspect each cited manuscript statement against its exact Lean declaration and downstream uses.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
Explore existing proof dockets →
The translation must preserve the original claim
The altered shape illustrates a change of meaning between an informal argument and its formal version. It is not one of the paper's specific Navier–Stokes estimates and does not depict a disproof.
Read the source · Introduction and Section 3 · statement and argument correspondence ↗- What it claims
- For l≥2 and k≥9, Theorem A.4 claims Σl⁰-completeness for deciding existence of a natural-number witness to the explicitly constructed polynomial predicate. Sections 2–3 distinguish theorem checking from faithful translation of an argument and report specific Navier–Stokes correspondence mismatches.
- Why this could matter
- Did the computer prove the thing we actually meant? A machine can verify every step after an assumption quietly changes. The paper examines that gap between ordinary mathematics and formal code. Its authors explicitly stop short of deciding whether the original Navier–Stokes proof is correct.
- If it holds up
- Proof reports would need a clearer bridge between the human claim, formal assumptions, and actual machine-checked conclusion.
- If it does not
- The particular theorem or mismatch examples would need revision; checking what a formal statement means would still matter.
- Impact horizon
- Methods · Formal verification · Proof translation · AI-assisted mathematics
- Version
- arXiv v1; 2026-10-06.
- Why we tracked it
- source-reviewed mathematical intake, not a completed peer review or homepage feature.
- Highest-risk dependency
- Analyst judgment: avoid turning a worst-case computability result into a claim about every finite translation; independently assess what each reported mismatch implies for the final theorem. The authors expressly do not decide the correctness of OpenAI's natural-language proof. A proof of a correctly specified endpoint can remain valid despite a different derivation; correspondence and theorem validity are separate questions.
- Available artifacts
- arXiv v1 supplies the manuscript and precise comparisons against OpenAI/NavierStokesAndEuler f9e8bc5b38b6e212696e8a30e3e91517af887bbd. The cited examples and Appendix A theorem have not been independently adjudicated here.
- Current boundary
- Intake record only; examination not started.