---
title: "A Proof Nobody Can Build On"
slug: "formalization-value-not-correctness"
language: "en"
date: "2026-10-28T12:35:02.509Z"
updated: "2026-10-28T12:35:02.000Z"
description: "Formalizing all of mathematics with AI: correctness is the floor, but a verified artifact nobody can reuse is a demonstration, not a contribution."
canonical: "https://fix.slopit.io/formalization-value-not-correctness/"
tags: ["math", "ai", "formalization", "open-source"]
---

A group of mathematicians who work on Lean — Jeremy Avigad, Kevin Buzzard, Johan Commelin, Rémy Degenne, Kim Morrison, Oliver Nash and Adam Topaz — wrote a guest post on Xena about the sudden enthusiasm for formalizing all of mathematics. Their central claim is blunt: a formal artifact is not worth much if nobody uses it.

That sounds obvious. It is also the thing every announcement about AI-generated formal proofs omits.

## Two examples, two outcomes

When Math, Inc. tried to hijack the sphere-packing formalization project in February, it demonstrated what the technology could do. It contributed nothing to mathematics. The original team kept working on a quality formalization of the 8-dimensional result and found that cleaning up the AI-generated code was more trouble than it was worth — better to throw it away and do it right, still with ample AI help.

When Anthropic announced that a model had formally verified Fermat's Last Theorem in 13 million lines over 11 days, Kevin Buzzard congratulated them and said he had no intention of abandoning his own formalization of a more modern proof. The theorems were not in doubt. The value of the formal artifact lies in what you get beyond correctness.

That's the distinction the post is built on, and it's sharper than the usual "AI proof vs human proof" argument. A verified proof can be correct and still be a dead end: a closed blob that nobody can reuse, generalize, or learn from. A library is valuable because other people can build on it — which requires naming, structure, documentation, and a willingness to refactor.

## What the value actually consists of

The post lists what formalization is for: exploring generalizations, finding connections between branches, considering unexpected applications, and refactoring concepts to make them more elegant. "Knowledge isn't worth having until it contributes to our understanding; the value of a formalization comes from our ability to use and interact with the data."

The Navier–Stokes case is the interesting edge. The natural-language proof was mostly incomprehensible; the Lean formalization gave near-certainty of correctness, and the community's anger was about provenance, credit, and the feeling that correctness alone was being treated as the goal. The authors are careful: the result may be right, and the way it was done still damaged the thing mathematics is for.

## The values are the actionable part

The post ends with ten values, and they're the part I'd steal even outside mathematics:

- Defer to human-curated libraries; adopt their design decisions and refactor toward them.
- Prefer breadth and thoroughness before depth.
- Avoid duplication; generalize for reuse.
- Review publicly against agreed standards.
- Publish freely and interoperably.
- Stay compatible with every release of the language and library.
- Stay open to better approaches.
- Document and organize.
- Link to the literature so a mathematician can verify the concepts mean what they think.
- Set standards and meet them — "producing low-quality or unaudited code and claiming or hoping to 'clean it up later' is counterproductive."

That last one is a direct rebuke of the dump-and-clean-later model, and it's the one the labs should read twice. The OpenAI math dump, in their account, contains astonishing mathematics and a remarkable disregard for readers: retracted results, informal/formal pairs that diverge, impenetrable writeups.

## The tension

The labs are optimizing for announcement; the community is optimizing for reuse. Both are rational, and they produce different artifacts.

A 13-million-line proof that compiles 20 times slower than Mathlib is a triumph of capability and a maintenance liability. A curated library that grows slowly is less exciting and more useful. The post doesn't pretend this is easy: it proposes funding, roadmaps, and governance to make the community's version the default, rather than leaving it to whoever announces first.

It's also worth noting that the authors have projects in this space — Mathlib, Tau Ceti, Formal Frontier. Their argument doesn't depend on that, but the reader should know it.

## My take

The correctness floor has been raised dramatically and permanently. That's good. What hasn't been solved is the ceiling: whether the artifact is integrated enough to be used.

The test I'd apply to any AI formalization announcement is the one this post implies. Not "does it compile?" but "can someone who wasn't involved build on it next month?" If the answer is no, it's a demonstration, not a contribution. Both are legitimate things to produce; only one of them is mathematics accumulating.

*Source: [How to Formalize All of Mathematics — Jeremy Avigad, Kevin Buzzard, Johan Commelin, Rémy Degenne, Kim Morrison, Oliver Nash, Adam Topaz (Xena)](https://xenaproject.wordpress.com/2026/10/16/how-to-formalize-all-of-mathematics/).*