{"path":"research/formalized-fermat-and-the-oracle-boundary.md","content":"# Formalized Fermat and the Oracle Boundary — what an 11-day machine proof says to a \"Lean for reasoning\"\n\n**Date**: 2026-09-05 · **Type**: founder-shared source read against the corpus · **Source**: a Facebook\npost relaying Anthropic's research note *Formalizing Fermat's Last Theorem* (2026-09-04); the note\nitself was read directly and the facts below are quoted from it, not from the post.\n\n---\n\n## 1. What happened, as the primary source states it\n\nClaude *\"produced the first end-to-end, computer-checked proof of FLT\"* in **11 days**: about **13\nmillion lines of Lean** (*\"over 5x the size of Mathlib\"*), **30,300 theorems** of which **29,500** are\nused in the final proof, **no `sorry`**, and *\"just Lean's three standard axioms\"*. The proof\n*\"follows a simplified version of Wiles's proof from Darmon, Diamond and Taylor\"* and *\"adapts pieces\nfrom the Imperial College London FLT project\"* — Kevin Buzzard's five-year programme, which the corpus\nalready tracks ([lean-social-system-research.md](lean-social-system-research.md) § 6). A separate\ncomparator *\"confirmed that the theorem's statement matches Mathlib's own statement of FLT\"*. Human\nmathematical input *\"was limited to occasional high-level instructions\"* — the example given is\n*\"Jacobian as a scheme sounds high priority\"*. Cost: *\"about six billion output tokens\"*. Anthropic's\nown caveat: *\"our proof is likely much longer than it needs to be.\"*\n\n## 2. What it confirms for the Lean analogy\n\nThe corpus built the sorry model on Tao's PFR project — a 33-page proof formalized in three weeks by 25\nstrangers, each filling one `sorry` ([lean-deliberus-analogies.md](lean-deliberus-analogies.md) § 1).\nThis is the next order of magnitude in the same direction with the strangers removed: the articulation\ncost of turning a proof into machine-checkable form fell from a five-year programme to eleven days.\nThat is condition (b) of the success prior — the articulation cost falling by an order of magnitude —\nobserved in the adjacent domain at two orders rather than one\n([fractal-priors-for-success.md](fractal-priors-for-success.md)). The project's own bet is that LLM\nextraction did the same thing for ordinary reasoning; here is the same variable moving, hard, where a\nchecker exists to prove it moved.\n\nThe 29,500 intermediate theorems are also the reasoning layer made visible in the one domain that\nalready had an oracle: the *dark matter of knowledge* the SciencePedia line names — conclusions kept,\nreasoning chains omitted — is exactly what Wiles's published proof left implicit and what the\nformalization had to write down ([the-missing-layer.md](../the-missing-layer.md)).\n\n## 3. The human residue collapsed to direction, not verification\n\n*\"Occasional high-level instructions… 'Jacobian as a scheme sounds high priority'\"* is priority-setting.\nIn the corpus's vocabulary that is the second positional act — *here is what you should be asking* —\nwhich the canon line *an act's value is not its rung* names as one of the two highest-value human\ncontributions ([what-human-judgment-is-for.md](what-human-judgment-is-for.md)). In the one domain with\na perfect checker, the human's job did not become checking; it became choosing what to pursue. That\nis one team's report and a single instance, but it is a clean instance: with an oracle in place the\nhuman role goes to the act the corpus predicted, not to ratification.\n\n## 4. Five times Mathlib: reuse failed under cheap generation\n\nThe kernel accepts a redundant proof as happily as a minimal one. Mathlib's conciseness comes from\nhuman curation — Buzzard's own observation that definitions, not theorems, are the hard part, and that\na garbled definition *\"will still compile, it just won't mean what it is supposed to mean\"*. A\nsorry-free proof five times Mathlib is a graph with no merge pass: generation was cheap, identity and\nreuse were not exercised, and the result is correct and bloated. The corpus's reuse-flywheel condition\n— *identity is decidable because Lean has types* ([the-reuse-flywheel-prior.md](the-reuse-flywheel-prior.md))\n— held for **checking** and not for **reuse**: whether a lemma is *the same as* one already in Mathlib\nis decidable, but whether a proof *should* have used it is a judgment about elegance the kernel does\nnot make. Even in the domain where identity is free, the reuse layer is judged, not decided. Deliberus's\nown version of this is measured: two thirds of the graph is machine-minted scaffolding, and the\nanti-drowning programme is the merge programme ([drowning-in-claims.md](drowning-in-claims.md)).\n\n## 5. The comparator is our coverage check by another name\n\nThe one thing the kernel cannot check is that the theorem *proven* is the theorem *meant*. The team\nran a separate comparator against Mathlib's statement of FLT for exactly that reason. The corpus built\nthe same instrument for the same blind spot eight days earlier: `check_coverage` runs as a **separate\ncall** because a model must not grade its own omissions, and asks whether the decomposition still says\nwhat the parent said ([the-jhu-decomposition-line.md](the-jhu-decomposition-line.md)). Coverage fails\nsilently in both domains, and in both the remedy is a second reader of the statement rather than a\nharder look at the proof.\n\n## 6. The boundary: thirteen million lines nobody reads\n\nNobody will read 13 million lines, and nobody needs to, because the kernel ratified every one. That is\nthe endpoint of full delegation **with an oracle**. Deliberus has no oracle for evaluative claims — the\nterminus enum is a map of the oracle gradient, and only the empirical leg reaches ground\n([fragile-checkers-and-the-verification-bottleneck.md](fragile-checkers-and-the-verification-bottleneck.md))\n— so the same sentence here reads *N claims nobody examined*, which is the open founder question about\nthe standing of untouched machine structure with the kernel removed. The FLT result does not answer\nthat question; it draws its boundary sharply. Where a leg reaches ground, delegation can run to\ncompletion and the human goes to direction-setting (§ 3). Where it does not, what stands in for the\nkernel is the deterministic audits and the positional human checks the conservative design lays out\n([cheap-to-add-slow-to-matter.md](cheap-to-add-slow-to-matter.md)) — and that is the strongest reason\nyet for the fact-layer-first sequencing: it is the leg on which an FLT-shaped result is even possible.\n\nOne more contrast. Six billion output tokens is a large number that cost nothing in checking, because\nthe checker is free and mechanical. *Checking that keeps pace with persuasion* is the project's\npromise, and in mathematics the check now keeps pace at machine speed. In the evaluative layer the\nscarce check is a person from a position, which is why every human act there has to be made to\nmatter rather than made to scale.\n\n---\n\nCross-references: [lean-deliberus-analogies.md](lean-deliberus-analogies.md) ·\n[lean-social-system-research.md](lean-social-system-research.md) · [the-reuse-flywheel-prior.md](the-reuse-flywheel-prior.md)\n· [the-jhu-decomposition-line.md](the-jhu-decomposition-line.md) · [what-human-judgment-is-for.md](what-human-judgment-is-for.md)\n· [fragile-checkers-and-the-verification-bottleneck.md](fragile-checkers-and-the-verification-bottleneck.md)\n· [drowning-in-claims.md](drowning-in-claims.md) · [fractal-priors-for-success.md](fractal-priors-for-success.md).\n"}