Definition
AI autoformalization translates natural-language (NL) mathematics into proof assistants such as Lean so machines can check logical consistency. Faithfulness between NL and formal artifacts is a separate — and hard — problem from whether either proof is mathematically correct.
Key Points
- 2026-10-06/09: Cambridge team shows OpenAI’s Navier–Stokes Lean code does not match NL Lemma 8.6 (m+4 vs m+5 derivative bound) (2026-10-09-navier-stokes-lean-mismatch-arxiv)
- Theoretical barrier: semantically faithful NL disambiguation ranks arbitrarily high in the Solvability Complexity Index — harder than Halting (2026-10-09-navier-stokes-lean-mismatch-arxiv)
A compiling Lean proof verifies the formal statement given, not that it equals the human paper. Mismatch ≠ refutation of the underlying math claim.
Related
- lean-formalization
- automated-theorem-proving
- ai-for-mathematics
- navier-stokes-millennium-problem
- openai