How to Formalize All of Mathematics

A coalition of mathematicians argues that rushing to formalize all mathematics with AI risks wasting resources and damaging research unless done with care. They point to high-profile AI-generated formalizations that impressed technically but added little lasting value - Math, Inc.’s Viazovska attempt, Anthropic’s Fermat’s Last Theorem dump, and OpenAI’s controversial Navier-Stokes submission - and warn that correctness alone is insufficient. Formal artifacts must be usable: well-documented, interoperable, creditable, and designed so others can build on them. Poorly curated mass formalizations can undermine incentives, obscure provenance, and set back community practices.

They offer a constructive alternative: coordinated, high-quality formal libraries combining human expertise, formal tools (Lean), and AI assistance, with rigorous curation and review. Existing efforts illustrate workable models: Mathlib’s community-vetted library; the Annals Challenge to formalize theorem statements; Formal Conjectures to capture vetted open problems; Tau Ceti’s AI-authored, expert-roadmap-driven library with adversarial AI review; and Formal Frontier’s source-to-library pipeline and build infrastructure producing dozens of coherent libraries and many formalized theorems. A registry, Palomar, is proposed to index projects with metadata and standards. The core prescription is alignment of libraries with mathematicians’ goals: prioritize reusability, documentation, naming, and review so formalization accelerates discovery rather than merely proving correctness.