Choosing and auditing a research formalization

Choose an ecosystem by the mathematical work it lets your group sustain. Then define what its formal artifact is supposed to certify: the final theorem, a particular argument, reusable infrastructure, or some combination. Recent Lean developments show why both decisions matter. A checked endpoint and an auditable mathematical explanation are separately valuable deliverables.

What the current Lean results demonstrate

Lean’s project record establishes serious research-scale formalization. Current work uses Lean 4 and mathlib; historical Lean 3 artifacts are not automatically source-compatible with that environment. It contains several kinds of accomplishment, whose scope should stay visible:

The PFR README’s opening still describes some refinements as ongoing, but its later registration section and structured metadata report their completion. The table follows the latter, more specific status record; the discrepancy is retained in the evidence. These are formalizations of established results, rather than evidence that their underlying mathematical theorems were newly discovered by the formalizers.¹²³⁴⁵

Formalization can also change the mathematics. Tooby-Smith’s two-Higgs-doublet study reports a counterexample to a published sufficiency condition and a corrected reduction. The Erdős problem 728 account presents a new solution while carefully acknowledging uncertainty about prior literature. Novelty and priority are historical claims assessed through sources; a kernel does not certify them.⁶⁷

Anthropic describes its FLT repository as an unmaintained research artifact that does not accept contributions. A successful theorem certificate and a library welcoming future work are different resources.⁸

The dimension-eight sphere-packing project provides a further practical lesson. Its authors report a February 2026 verification milestone, but describe readable, reusable code as continuing work. Missing analytic infrastructure also influenced the proof route. Verification, mathematical generality and maintainability therefore need separate acceptance criteria.⁹

Why Lean appears so often in the headlines

Three documented developments help explain the concentration. Mathlib provides shared mathematical infrastructure and contributor conventions. Lean FRO maintains the prover, while the Mathlib Initiative supports library review, coordination and documentation. AI researchers also adopted Lean: DeepMind’s AlphaProof trained proof search against its checker, and the later projects discussed here used it for research-scale formalization.^10111213

My inference is that reusable mathematics, organized maintenance and investment in proof search reinforce one another. They lower some costs for the next Lean project and make its result more visible. This explains a plausible concentration of effort; it does not measure the causes or establish that Lean’s logic is uniquely suitable for frontier mathematics.

The Navier–Stokes case: identify the target first

OpenAI’s 8 September announcement claims finite-time breakdown for three-dimensional incompressible Navier–Stokes with smooth forcing and initially zero velocity, targeting Clay alternatives C and D. Its separate Euler claim is unforced. Clay’s published formulation permits forced breakdown in C/D; a correct result satisfying those alternatives would meet an official route to the problem. It would not establish unforced Navier–Stokes blow-up.¹⁴¹⁵

The formal endpoint should be assessed independently of its manuscript. The published Comparator development gives an existential breakdown statement for each positive viscosity, and its adapter constructs the witness from the development’s main theorem. The desired witness is not simply supplied as an additional top-level hypothesis. The project reports only propext, Classical.choice and Quot.sound in the main results’ axiom dependencies, with no sorry. Those are author-provided records, rather than this survey’s checking receipts.¹⁶¹⁷¹⁸

Bastounis, Circelli and Hansen’s 6 October preprint challenges correspondence between intermediate manuscript claims and formal declarations. It explicitly declines to judge the correctness of the manuscript itself.¹⁹

One comparison concerns the inverse of a directional derivative on a two-dimensional torus. For smooth, zero-mean $𝐹$, let $𝑁=𝑣\cdot {\nabla }_{𝑦}$, where $𝑣=\left(\sqrt{2}-1,1\right)$. Here ${𝑁}^{-1}𝐹$ denotes the unique smooth zero-mean solution of $𝑁𝜑=𝐹$; this particular direction matters. Here ${𝐶}_{𝑦}^{𝑟}$ measures the size of torus derivatives through order $𝑟$; the bound’s constant may depend on $𝑚$, but not on $𝐹$. The manuscript’s Lemma 8.6 states an estimate of the form

The cited formal theorem instead requires input-derivative bounds of order $𝑚+5$ to control output derivatives of order $𝑚$. Its code is pinned at commit f9e8bc5b38b6e212696e8a30e3e91517af887bbd.²⁰²¹

The extra derivative matters for this comparison. Using a higher derivative norm on the right does not, merely by being checked, establish the displayed sharper bound. Smoothness of the functions does not make the quantitative estimates identical. Whether the formal estimate suffices downstream is a different question, answered by the formal dependencies and their mathematical interpretation.

A second comparison concerns a pressure-flux estimate. The manuscript’s displayed bound uses a localized velocity quantity; the formal declaration also uses a localized gradient quantity and different powers of the cutoff radius. That is an observable change in the intermediate assertion, not evidence by itself of a false final theorem.²²²³

The critique’s general impossibility discussion concerns a universal guaranteed translator, including arbitrary hidden existence presuppositions. It does not establish that this finite manuscript cannot be explained or audited. Public commentary by Matt Baker and Kevin Buzzard likewise distinguishes the final formal theorem from verification of its accompanying prose. This survey found no specific first-party OpenAI reply to the critique.²⁴²⁵

Separate the five verification questions

1. Statement fidelity: do the formal domains, quantifiers, definitions and hypotheses express the intended theorem?
2. Argument fidelity: do the intermediate lemmas and inferences correspond to the particular manuscript, or has another route been substituted?
3. Foundational adequacy: are the axioms and optional features appropriate to the mathematical claim?
4. Checking integrity: which exact implementation accepted which artifact, and can independent checking reproduce that result?
5. Explanation and reuse: can mathematicians inspect the decisive constructions and use the result without reconstructing an opaque development?

A project can succeed on one question and remain unresolved on another. This framework is the author’s synthesis of the preceding distinctions. It applies to every ecosystem here; no checker compares its judgment with unprovided English intentions.

Which ecosystem deserves the first pilot?

For a new collaborative project in conventional classical mathematics, Lean with mathlib is my default candidate when nearby definitions and theorems exist. Its demonstrated projects and common infrastructure justify that recommendation. They do not justify rewriting an established development or assuming every field has adequate coverage. Mathlib’s own policy places limits on scope and review capacity, and generated contributions must be understood and disclosed.²⁶

Choose Rocq first when dependent representations, certified computation or a strong existing MathComp development dominate the work. Its four-color and odd-order histories show the value of engineering a coherent mathematical infrastructure. For univalent work, choose the actual library and its assumptions, rather than “Rocq” generically.²⁷²⁸

Choose Isabelle/HOL first when the group already uses its theories, needs locales and structured Isar exposition, or benefits from reconstructed external automation. AFP includes substantial analytic mathematics. Its seL4 use is important evidence of verification practice, with model and platform assumptions explicitly stated.²⁹³⁰³¹

Choose Mizar first when a set-theoretic article and MML’s existing representation are the desired products, particularly with experienced collaborators. Its structured proofs and library-review tradition support that fit. Its checking architecture and distribution policy deserve direct inspection if a project requires independently auditable small-kernel assurance.³²³³

Choose Agda for constructive dependent mathematics whose algorithms and proof terms are central. Choose Cubical Agda when computational univalence or higher inductive constructions materially help the mathematics. Its cohomology and schemes work demonstrates research beyond studying the prover itself. TypeTopology provides another substantial mathematical tradition with different assumptions and style.³⁴³⁵³⁶

Choose Arend when its HoTT-I language, library and specialist collaborators fit the construction. Complete spaces and the August 2026 library additions supply concrete evidence. Its computational limitations and the unmeasured size of its support community favor a bounded pilot before a large dependency commitment.³⁷³⁸

HOL Light, HOL4 and Metamath remain justified choices when their existing infrastructure or checking model fits. Flyspeck used HOL Light and Isabelle together; HOL4 supports substantial analysis and probability; Metamath separates explicit proof verification from proof discovery. These are established mathematical communities with infrastructure that can justify choosing them for a new project.³⁹⁴⁰⁴¹

Would another language settle the translation problem?

No language in this survey provides automatic one-to-one correspondence with an arbitrary natural-language proof. Mizar and Isar make explicit intermediate claims comparatively easy to expose. Typed programs can expose constructions. Metamath makes low-level inferences explicit. These features aid inspection, but a definition or hypothesis can still differ from the intended one.

Nor is literal one-to-one correspondence always the right contract. Formal proofs routinely insert omitted details, split lemmas and reorganize arguments to suit a library. For an endpoint-certification project, an alternative valid proof may be wholly acceptable. For a manuscript-verification project, changed lemmas and routes should be declared, checked for their precise relationship, and reflected in the explanation. The acceptance criteria must specify which product is wanted.

A bounded research pilot

Before committing months of work, formalize a representative lemma and one difficult interface. Record:

• the informal statement beside its full formal statement, including transitive definitions;
• the exact hypotheses and axiom dependencies, plus admissions or trusted extensions;
• the nearest existing library results, missing infrastructure and incompatible representations;
• the correspondence of the decisive manuscript steps, including intentional substitutions;
• pinned toolchain and dependency identities, replay results, and a human-readable account of the construction;
• who will review, maintain and teach the artifact after its first successful check.

For an existential PDE theorem, the existence of the constructed witness must be discharged, rather than hidden in an interface assumption. For an analytic estimate, compare constants, regularity, quantifier order and uniformity. For an algorithmic result, separate mathematical existence from effective computation. These checks test the advertised result directly.

Independent checking can strengthen the receipt, but should use appropriate versions. Lean’s September 2026 hardening notes document deliberately constructed soundness failures, including one accepted by nanoda. The Anthropic FLT artifact pins an earlier version and describes particular independent-checker patches. This is a reason to inspect exact receipts, not a finding that either FLT or Navier–Stokes exploits a bug.⁴²⁴³

Problem space

• Survey terminus: the comparative source-based assessment is complete.

• Next useful mathematical decision: choose a representative theorem and a community able to review its statement and proof interfaces.

  • Keystone: write the certification contract before running proof search.
  • If manuscript fidelity is required: map changed intermediate statements and revise the prose to match the checked route.