Formal proof and verifiable outputs: when the verifier settles the question

One agent delivers an answer. Another reviews it. Both agree. Even so, the conclusion may be wrong because they share models, context, assumptions, or similar failures.

Anthropic's announcement about formalizing Fermat's Last Theorem offers a rare case: formal verifiers could reject or accept the AI-generated artifact without trusting the model's eloquence.

State: Evidence Brief approved for publication. This text analyzes a public artifact and proposes an architectural pattern. It does not claim that Trustyu Forge reproduced the experiment or that this design is implemented or operating across all its products.

The correct scope of the claim

On September 4, 2026, Anthropic reported that its Prove2Me multi-agent system formalized an existing proof of Fermat's Last Theorem in Lean. The Anthropic publication describes 11 days of work, dozens of agents, approximately 6 billion output tokens, more than 13 million lines of Lean produced throughout the process, and 29,511 declarations used in the final proof.

Precise wording matters: the agents did not discover the theorem or a new mathematical proof. They converted a simplified exposition of the Wiles and Taylor-Wiles proof into a verifiable formal chain. The public repository pins Lean 4.33.1 and Mathlib v4.33.0, provides build instructions, and exposes the artifacts under the Apache-2.0 license.

These figures do not disclose total financial cost, equivalent human productivity, or performance in other domains. They measure the process and artifact in this case.

Four layers of verification

1. The formal body

Lean turns each step into terms that must satisfy the type system. The final answer is not accepted because it looks correct: it must be reconstructed by the kernel.

2. The Lean kernel

The repository reports a build of 60,475 modules. The kernel checked the chain using three standard axioms. The trust surface is smaller than the entire stack that produced the code, but it is not zero: it includes the kernel, pinned versions, the build chain, and the environment.

3. The Comparator

O Comparator compares Lean theorems up to definitional equality. In this case, it was used to check whether the final statement matches the expected Mathlib theorem and whether the axiom list agrees. This prevents a common false positive in formal generation: proving a similar but weaker or different statement.

4. An independent kernel

According to Anthropic and the repository, Nanoda — a Rust verifier independent of the Lean kernel — checked 1,052,234 declarations without errors. Four small patches were required and described as not weakening the type system. This caveat must remain attached to the claim; “independent verifier” does not mean reproduction without adaptation.

Kevin Buzzard, a professor at Imperial College London and leader of a related formalization project, reports in the Xena Project having compiled the code and run the Comparator successfully. This is relevant external corroboration. There is also relationship context: Anthropic provided the academic project with access to a 500 GB machine.

Proof-carrying output for agents

In software security, proof-carrying code describes code accompanied by verifiable evidence of properties. The pattern can be carefully generalized to agents: a proof-carrying output includes the result, the conditions under which it was produced, and an artifact that an independent verifier can reconstruct.

A text response does not become proof merely by including a rationale. To be proof-carrying, evidence must have defined semantics, accept rejection, and reduce the amount of trust placed in the generator.

spec versionada
      ↓
gerador probabilístico ──→ artefato candidato
                               ↓
                    verificador independente
                         ↙           ↘
                    rejeita        aceita
                       ↓              ↓
              evidência de falha   receipt assinado
                       └──────→ decisão humana/runtime

A minimum verifiable-output contract

The contract must survive sessions, models, and teams. Isolated environments, explicit state, and durable evidence are properties of the harness around the agent, not magical qualities of the model. They help make failures observable but do not automatically prove that a product is safe or ready to operate. [HARNESS31-C2]

What Prove2Me teaches about orchestration

O Prove2Me paper describes a neurosymbolic system that organizes goals as a directed acyclic graph, parallelizes subtasks, searches for and reuses lemmas, and separates proposing statements from constructing proofs.

This design contains four transferable lessons:

1. Dependency is a system entity. Subtasks advance only when their prerequisites are met.
2. State is shared and versioned. Agents do not work only from conversational summaries.
3. The verifier creates objective feedback. Failures return to the cycle without requiring a subjective assessment by the generator itself.
4. Failed attempts are evidence. Anthropic reports earlier approaches that did not scale; the outcome depended on scaffolding and decomposition, not merely on greater model capability.

Where this pattern fits — and where it does not

Proof-carrying output is especially useful when the domain offers verifiable invariants:

• compilation, types, tests, and software properties;
• accounting reconciliation and conservation of totals;
• application of policies and access boundaries;
• data transformations with schema contracts;
• reproducible calculations and regulatory trails;
• configurations that can be evaluated through policy-as-code.

The pattern is more limited when the result depends on taste, negotiation, social context, human prognosis, or open legal categories. In those cases, structured evidence remains useful but does not eliminate judgment, interpretive disputes, or professional accountability.

Reproduction cost and operational boundary

O repository reports that the full build generated about 67 GB in the .lake, used approximately 220 GB for temporary C files, took 5 hours and 32 minutes with 96 parallel jobs, and reached peak memory of 153 GB. The Comparator took approximately 15 hours and reached 230 GB.

This shows that verifiability also consumes engineering and infrastructure. Anthropic did not publish the experiment's total cost. Six billion tokens should not be converted into a price without knowing models, discounts, caching, internal attempts, and infrastructure. For products, the goal is not to maximize proof; it is to choose evidence proportional to consequence and risk.

Technical gate before release

A team can use this gate for a critical workflow:

1. Is the requirement versioned, with explicit rejection conditions?
2. Is the material outcome — not just the text — verifiable?
3. Is the verifier independent of the generator in the relevant failure dimension?
4. Are input, output, versions, and evidence linked by digests?
5. Are failure, inconclusive, and timeout states distinct from success?
6. Is release authority separate from production and verification?
7. Were verification cost and latency measured at p95?
8. Is there a fallback, and does the error remain contained and reversible?

An approved gate is not evidence of observed production. It is bounded authorization for the evaluated version and scope.

Limitations, counterpoints, and conflicts

• Anthropic is the primary source and developer of the system; it has a commercial interest in the outcome.
• The open repository, kernels, and Buzzard's assessment strengthen the technical claim but do not constitute a financial audit or reproduction by multiple independent groups.
• Buzzard considers that the work adds little to known mathematics and much to autoformalization; his analysis also takes place in an ecosystem that received infrastructure from Anthropic.
• The mathematical domain allows formal verification. The same assurance does not transfer to open-ended decisions.
• Lines, tokens, and declaration counts measure volume, not value in isolation.
• Total cost, energy consumption, and the distribution of failed attempts were not disclosed.

Sources and editorial context

1. Anthropic — Formalizing Fermat's Last Theorem in Lean. Primary vendor source, published on 04/09/2026.
2. Anthropic — fermats-last-theorem repository. Code, versions, instructions, build metrics, and license.
3. Xena Project — FLT: Anthropic has beaten me to it. Corroboration and counterpoint from Kevin Buzzard.
4. Prove2Me. Description of the neurosymbolic system and orchestration.
5. Lean Comparator. Implementation of the comparator used in the check.

Editorial and responsibility note

This text combines facts attributed to sources with the author's analysis and technical proposal. Personal and professional views are not proven facts; data, denominators, boundaries, and conflicts are identified when available. The content is informational and does not replace specific technical, mathematical, legal, financial, or security assessment. Tech Human and Trustyu operate commercially in related areas. Research, structure, and writing were assisted by AI; factual review, author approval, and publication were confirmed by Fernando Parreiras on 05/09/2026, without additional independent human review.

Research cutoff: 05/09/2026. Editorial state: extraordinary special publication authorized for 05/09/2026 at 19:21 BRT.