Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs

arXiv:2610.08144 · math.AP, cs.AI, math.LO · Submitted 2026-10-06 · Read on arXiv

math.AP, cs.AI, math.LO

Submitted: 2026-10-06

Updated: 2026-10-06

Comments: 25 pages, 4 Figures

License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/

Terminology

• Verification — 1× in this paper · explained in 2 episodes

Sources

• The extended Smale's 9th problem -- On computational barriers and paradoxes in estimation, regularisation, computer-assisted proofs and learning
• Computing Spectra -- On the Solvability Complexity Index Hierarchy and Towers of Algorithms
• Finite time singularities of smooth solutions for the 2D incompressible porous media (IPM) equation with a smooth source
• Formalizing Mathematics at Scale

Related papers

• Anisotropic uncertainty principles for metaplectic operators
• Convergence of graph Dirichlet energies and graph Laplacians on intersecting manifolds of varying dimensions
• Fractional Parabolic Partial Differential Equations in Anisotropic Spectral Barron Spaces: Regularity and Neural Approximation
• Regularity of Second-Order Elliptic PDEs in Spectral Barron Spaces
• Determining a parabolic-elliptic-elliptic system by boundary observation of its non-negative solutions under chemotaxis background
• Global boundary stabilization of 1d systems of scalar conservation laws