Library-Grade Formalization

Sources#

• How to Formalize All of Mathematics

Summary#

Every other formal-math page asks whether a formal artifact is correct: whether the kernel accepted it (Kernel-Level Proof Auditing), whether it proves the intended statement (Statement Drift), whether it carries understanding (Logical vs Intelligible Proof). This page holds a fourth question, whether anyone can use it. The claim comes from seven people at the centre of Lean and Mathlib: Jeremy Avigad, Kevin Buzzard, Johan Commelin, Rémy Degenne, Kim Morrison, Oliver Nash and Adam Topaz, in a guest post on the Xena Project blog, How to Formalize All of Mathematics, 2026-10-16 (How to Formalize All of Mathematics, practitioner-opinion). It answers calls, after OpenAI's October release (Proof Abundance), to "formalize everything as quickly as possible".

The argument in one step: "a formal artifact is not worth much if nobody uses it." When the theorem was not seriously in doubt, "the value of the formal artifacts lies solely in what we get beyond mere correctness": generalizing, connecting branches, refactoring concepts, building further. So "a lousy formalization of existing results is worse than no formalization at all". It costs money, it "could disincentivize good research", and "a grand failure will make it hard, or even impossible, to recover later." They call the task "a special case of the alignment problem, namely, ensuring that formal libraries fulfill the community's mathematical goals."

The authors are not against AI formalization. Two of the five projects they recommend are written entirely by AI agents. What they oppose is formalization outside a library: one-off repositories that follow no shared design, duplicate existing material, and are left behind once announced.

The three incidents, as the authors characterize them#

These are the post's characterizations. Each is checked here against what the corpus already holds.

• Math, Inc. and sphere packing (February 2026). Math, Inc. "tried to hijack a project" to formalize Viazovska's sphere-packing results. It "impressively demonstrated what the technology could do" but "contributed nothing to mathematics". The original team, formalizing the 8-dimensional case, found "cleaning up the AI-generated code was more trouble than it was worth" and threw it away, then did it right "still with ample help from AI". New to the corpus, one-sided. No Math, Inc. source is held, and "hijack" is the authors' word. It is the corpus's only report of AI-generated formal code being discarded by the human project it was meant to serve, so it is the cleanest instance of the page's claim, and it rests on this post alone.
• Anthropic's FLT (September 2026). "13 million lines of code written over 11 days". Buzzard "cheerfully lauded the result" and kept formalizing a more modern proof. Verdict: "this piece of AI-generated code probably has little ongoing value". Consistent with Buzzard's own account (FLT: Anthropic has beaten me to it, 13.4M lines, 11 days; see Lean). That post said the work "tells us essentially nothing" mathematically. It was also "so excited" about what autoformalization at that scale makes possible, and it named the deliverables Anthropic would likely skip: Mathlib pull requests and an explorable document of the modern proof. The tone has hardened from "impressive, and here is what it is not" to "probably little ongoing value". The facts have not changed.
• OpenAI's Navier–Stokes (September 2026) and the October dump. Here "the correctness signal played a key role": "there seems to be little doubt now that the solution is correct, even though the natural-language proof is mostly incomprehensible." The anger was about how the result was obtained, provenance and credit, and a focus on correctness that discourages the exploration the Millennium Prize was meant to foster. Consistent with The Navier–Stokes AI Claim: the rival claimant concedes correctness and calls the paper not "in a readable form" while holding that "the ideas can be digested", a softer reading than "mostly incomprehensible". Bastounis, Circelli and Hansen show the Lean proof is not the manuscript's argument. The post adds no named re-check. Its "little doubt now" is the judgement of Lean-community insiders, not a verification event. The October dump (github.com/openai/math) "contains astonishing and important mathematics" and "a remarkable disregard for readers": "some results have been retracted, many of the informal/formal pairs diverge in subtle or significant ways, and most of the informal writeups are impenetrable." That extends Tao's account on Proof Abundance. Tao did not say whether the release was formalized. This says it holds informal/formal pairs and that they diverge, which is the Statement Drift translation route at release scale, reported without counts.

What the post praises instead. OpenAI's unit-distance disproof (the Erdős 90 result on Latent Capability Overhang and FrontierMath Erdős Benchmark) and Anthropic's work on the density of Riemann zeta zeroes. The community "subsequently built on their work". Do not conflate the zeta item with the zero-free region at Re(s) = 7/8 that Tao describes from OpenAI's dump: different lab, different result. The Anthropic paper is not in the corpus.

The regime they propose#

The ten values, adapted from Mathlib's published values document: defer to human-curated libraries, especially Mathlib, and keep refactoring to its decisions; breadth before depth; no duplication, generalize for reuse; public review to agreed standards; publish openly and interoperably; stay compatible with every Lean and Mathlib release; stay open to better approaches; document and organize; link to the literature, so a reader can trust a concept means what it should; set standards and meet them, because "claiming or hoping to 'clean it up later' is counterproductive". The last is the sphere-packing lesson as a rule.

The forecast and the asks. "Within three years, and possibly much sooner, most of mathematics can be formalized in such a way that mathematicians can explore, build on, and make use of formal libraries." Their asks: curate Mathlib; fund Tau Ceti and Formal Frontier "to grow by an order of magnitude in a matter of months"; write expert roadmaps and blueprints; model the financial and engineering cost (footnoted as forthcoming); put the tools under "control by mathematicians"; and host the work at non-profit or academic institutions with governance bodies. Tier: prediction for the forecast.

Where it sits against the corpus#

• Tau Ceti stakes its quality on AI review, and the corpus has measured AI fidelity review failing. The three-vendor judge panel on Statement Drift scores recall 0.093 on statement alignment. In Meta's textbook claim, relayed on the same page, fidelity checking "mainly performed by other AIs" met "0% of the statements here are accurately formalized" from a human reader. Buzzard's own September report has Mathlib refusing AI reviews (Lean). Tau Ceti's rubrics cover generality, reuse, documentation and naming. The post does not say whether they check statement fidelity, or whether any human samples the output. The two differences from the Meta case are real: expert roadmaps choose the targets, and the library defers to Mathlib's definitions, so fewer statements are freshly invented. Neither difference is measured.
• Buzzard's forecast has started to come true. On 2026-09-04 he expected AI-generated libraries "such as Tau Ceti" to "eventually contain far more mathematics" than Mathlib, "possibly with some incorrect definitions or poorly-written proofs". Six weeks later he co-signs a post putting Tau Ceti at roughly Mathlib's size and calling it shovel-ready. The size claim is consistent with Hales's Mathlib figure (2.5M lines, Lean). The post's parenthetical "3 million lines" could be read as either library's size. Unreconciled: the post counts 950 Mathlib contributors, and Hales, a week earlier, "over 700". They probably count different things. Neither figure is superseded.
• Palomar makes the corpus's audit recommendations a registry rule. Requiring a Comparator setup turns the check on Statement Equivalence Checking and Kernel-Level Proof Auditing into an entry condition. formalization.yaml adds what no audit captures: who did the work, with how much AI, and whether the informal authors took part. That last field is the credit dispute on The Navier–Stokes AI Claim, recorded as metadata. FormalFlow already registered its target there (see Kernel-Level Proof Auditing).
• Formal Conjectures is the trusted copy that statement checks assume. FrontierMath Erdős Benchmark takes 50 of its 68 statements from it. The post's ask, that announcers reuse vetted statements, is the given-statement defense on Statement Drift, stated as community policy.
• The Annals Challenge names the blocker other pages hit. "The blocker here is missing definitions": FrontierMath Erdős admits only conjectures statable in Mathlib definitions, and the conjecture-proving run on AI-Driven Formal Proof Search never reached its proving stage, because its invariants were defined only in the author's preamble. A project that states but does not prove is a definitions programme.
• "Alignment" is the same word Tao and the Fields Medallists used. Tao called the lab-community divergence "misalignment" (Proof Abundance), and the mathandai.org declaration calls it "severe misalignment" (Logical vs Intelligible Proof). These authors narrow it to something checkable: does a library serve the community's goals? Their test is reuse, which none of the earlier statements proposed.
• Agent-built libraries are agent harnesses. Tau Ceti's worker loop (tauceti work --loop over claude or codex) and Formal Frontier's agent swarm belong with the builder-side harnesses on Many-Agent Proof Harnesses and Global Proof Coordination. The difference is the output. Those harnesses aim at one theorem; these aim at a library someone else will import. Automated Conjecturing's self-expanding side library is the same question in miniature: statements built for the loop, with untested reuse value.

Evidence note#

practitioner-opinion, kept. No measurement. The authors are Lean and Mathlib insiders, among them the leader of the human FLT formalization. The post does not list their roles. Interests: the post asks for money and inference for Tau Ceti and Formal Frontier, which the Lean FRO and the Mathlib Initiative incubate. The authors disclaim speaking for "any of the organizations or communities with which we are associated" without naming them. Every figure about those projects is self-reported and unaudited here. The three incidents are characterizations by parties with a stake in the alternative. The Math, Inc. one has no second source in the corpus. The Tau Ceti and Formal Frontier repositories were not fetched.

Connections#

• Proof Abundance — the October release this answers, now with the post's report that its informal/formal pairs diverge and some results were retracted
• The Navier–Stokes AI Claim — the case where the correctness signal mattered, and the provenance and credit dispute Palomar's metadata file would record
• Statement Drift — divergent informal/formal pairs as translation drift at release scale; Formal Conjectures as the vetted-statement defense; the AI-review evidence Tau Ceti's model must beat
• Statement Equivalence Checking — Comparator as a Palomar entry condition
• Kernel-Level Proof Auditing — FLT's comparator run, and Palomar as the registry FormalFlow used
• Logical vs Intelligible Proof — the third question this page sits beside, and the "misalignment" framing narrowed here to a reuse test
• Lean — Mathlib's scale and review policy, and the growth-of-Mathlib question this page extends
• FrontierMath Erdős Benchmark — the benchmark built on Formal Conjectures statements and Mathlib-statable eligibility
• AI-Driven Formal Proof Search — the definitions blocker, met in the conjecture-proving run
• Many-Agent Proof Harnesses — builder-side agent harnesses aimed at one theorem, against libraries aimed at reuse
• Global Proof Coordination — another coordinated Lean agent harness, scored on solves rather than on reuse
• Automated Conjecturing — a self-expanding side library with untested reuse value
• Latent Capability Overhang — the unit-distance disproof the post praises
• Verification as the New Bottleneck (hub) — review capacity is what Mathlib's slow growth spends, and what AI review in Tau Ceti tries to replace
• Anthropic, OpenAI, Google DeepMind — the FLT and zeta-density lab, the Navier–Stokes and dump lab, the Formal Conjectures host
• Terence Tao — whose account of the dump this post extends

Open Questions#

• Does AI adversarial review against rubrics produce statements a human fidelity audit accepts? Tau Ceti is the test, since Meta's AI-checked textbook libraries failed this audit (see Statement Drift). Settled by a human expert statement audit of a sample of Tau Ceti theorems (for instance Riemann–Roch or Chebotarev, unfolded to Mathlib definitions), or by Mathlib reviewers accepting Tau Ceti material upstream. Related to the proof-debt question on Statement Drift, which covers proofs rather than statements.
• Will the curated AI libraries be built on while one-off dumps are not, as the post predicts? And will most of mathematics be usably formalized by October 2029? (Trigger: downstream-dependency counts for Tau Ceti and Formal Frontier against the FLT, sphere-packing and openai/math repositories, 12 months or more after release; the order-of-magnitude growth "in a matter of months" if funded; or the October 2029 horizon itself.)

Sources#

• How to Formalize All of Mathematics — Jeremy Avigad, Kevin Buzzard, Johan Commelin, Rémy Degenne, Kim Morrison, Oliver Nash & Adam Topaz, How to Formalize All of Mathematics, guest post on the Xena Project blog, 2026-10-16, ~2,400 words (incl. links), practitioner-opinion. Cited for the reuse argument, the three incident characterizations, the two praised results, the six-project survey and its figures, the ten values, the three-year forecast and the asks. The linked repositories, the Annals Challenge preprint (arXiv 2610.18301) and Mathlib's values document were not fetched.
• FLT: Anthropic has beaten me to it — Buzzard, Xena Project, 2026-09-04, case-study. Cited only to check the FLT characterization and Buzzard's Tau Ceti forecast; full treatment on Lean.