AI/ML Deep Dive: The Scale Leap in Machine Proof

Like a validating node in a blockchain: anyone — even a malicious party — may propose a block. The validator ignores explanations and reputation; it simply replays every transaction. Correct gets accepted, wrong gets rejected.

The hardest LLM failure to guard against is being "fluently wrong": the reasoning reads well, the conclusion is false; on Day 60 even the monitor reading the CoT was persuaded. Mathematical proofs are a prime case — human refereeing of Wiles's proof took a long time and did find a gap.

A proof assistant (software that checks mathematical proofs step by step) changes the trust structure. It rests on the Curry–Howard correspondence: propositions are types, proofs are programs of that type. "Proving theorem P" means "writing a term of type P", and checking a proof = type checking. In Lean this is done by a small kernel that knows only a handful of inference rules plus three standard axioms (propositional extensionality propext, the axiom of choice Classical.choice, and Quot.sound for quotient types).

The key is an asymmetry: finding a proof takes creativity and enormous search; checking one is mechanical replay. So the generator can be an unreliable, hallucinating model — once the result passes the kernel, correctness no longer depends on trusting the model. This is the de Bruijn criterion: the trusted part should be small enough for humans to audit. The kernel also does not read comments or reasoning, so the Day 60 channel — "the rationale persuaded the judge" — simply does not exist here.

The intuition that "verifying is far cheaper than generating" shares its roots with the P vs NP distinction in complexity theory: checking a completed Sudoku takes seconds; solving it from a blank grid can take a long time. Scaling machine proof is essentially trading massive amounts of cheaply checkable trial and error for one expensive result.

# Toy "kernel": accepts only axioms and modus ponens, checks a proof line by line
axioms = {"P", "P->Q", "Q->R"}

def check(proof, goal):
    known = set()
    for line in proof:
        if line in axioms:
            known.add(line); continue
        # Need some known A and A->line, else reject — no "explanations" accepted
        if not any(f"{a}->{line}" in known for a in known):
            return False
        known.add(line)
    return goal in known

print(check(["P", "P->Q", "Q", "Q->R", "R"], "R"))  # True
print(check(["P", "R"], "R"))  # False: a skipped step, however "obvious"

The checker is a dozen lines and treats every author's proof the same. The real Lean kernel is far more complex, but the principle is identical: checking is local and mechanical.

Like CI all green while the spec is wrong: the tests prove the code satisfies the tests, but cannot prove the tests check what you actually wanted.

The kernel answers exactly one question: "this proof really proves this formal statement". It does not answer "is this statement the theorem you had in mind". So only three attack surfaces remain:

• Swapped statement: e.g., a definition written too broadly or narrowly, making the theorem vacuously true (the premise is never satisfied, so the "conclusion" holds automatically);
• Extra axioms: a single axiom line can "prove" anything;
• Placeholders left in: Lean's sorry lets you skip a step temporarily.

Here each was closed off: a comparator confirmed that the final theorem matches the FLT statement already written in the community library Mathlib, and the proof was confirmed to depend only on the three standard axioms, with no sorry. Kevin Buzzard (the Imperial College mathematician leading the human FLT formalization project) then downloaded it, compiled it, ran the kernel himself and confirmed it holds.

This has the same structure as the reward hacking in Day 59: optimization pressure flows to wherever the check is weakest. Once proof correctness is welded shut by the kernel, the only loopholes left are "statement" and "axioms" — so the statement must be written in advance by a party independent of the generator, ideally a version that predates the work and was reviewed by the human community.

# Vacuous truth: with a skewed statement, the "proof" passes but proves nothing
def fermat_holds(domain, n):
    # "For all (x,y,z) in domain, xⁿ+yⁿ≠zⁿ"
    return all(x**n + y**n != z**n for x, y, z in domain)

real = [(x, y, z) for x in range(1, 30)
        for y in range(1, 30) for z in range(1, 30)]
# Skewed definition: require x > z and y > z — then xⁿ+yⁿ > zⁿ always
bad = [t for t in real if t[0] > t[2] and t[1] > t[2]]

print(fermat_holds(bad, 2))   # True — "proved", yet n=2 has 3,4,5!
print(fermat_holds(real, 2))  # False — fails under the correct statement
print(fermat_holds(real, 3))  # True (a finite spot check, not a proof)

Like Bazel's dependency graph + C header files: fix every .h (interface) up front, let everyone write their own .cpp (implementation); changing one implementation does not recompile its dependents, and the build system reads the graph to decide what can run in parallel next.

The report admits that the first several attempts failed: agents started well but quickly lost track of the project state and stopped collaborating effectively — context decays over long-horizon tasks, and the memories of dozens of agents drift apart. It worked only after switching to Prove2Me (a collaborative formalization platform from Tianyi Peng's group at Columbia University). Its structure:

• Theorem statements form a directed acyclic graph (DAG): nodes are statements, edges mean "proving A uses B". Agents read the graph to decide what to prove next; state is externalized onto the graph rather than relying on anyone's memory;
• Statements and proofs live in separate files, and statements are immutable: a proof may import a statement not yet proved, so hard problems can be split into small ones — interface first, implementation later;
• Each statement carries a natural-language description for search and reuse.

Why can many agents safely work in parallel here? In distributed systems the most expensive part of collaboration is consensus: you have to trust what others hand you. Here every submission is checked independently by the kernel, so agents need neither trust nor review each other — the kernel is the sole consensus mechanism. In the end about 30,300 theorems were proved, about 29,500 of which made it into the final proof. The cost was substantial too: the report puts consumption at roughly 6 billion output tokens — a textbook case of trading compute for labor, which only pays off when the judge is cheap enough.

# Simulate with stdlib graphlib: which statements can be worked on in parallel now?
from graphlib import TopologicalSorter

deps = {                        # statement -> statements its proof uses
    "FLT": {"A", "B"},
    "A": {"A1", "A2"}, "B": {"B1", "B2"},
    "A1": set(), "A2": set(), "B1": set(), "B2": set(),
}
ts = TopologicalSorter(deps); ts.prepare()
wave = 1
while ts.is_active():
    frontier = ts.get_ready()  # nodes whose dependencies are all "proved"
    print(f"Wave {wave}, assign to agents in parallel: {sorted(frontier)}")
    ts.done(*frontier)          # assume the kernel accepts them all
    wave += 1

The real process is more flexible: since unproved statements can be imported, agents need not wait for dependencies before writing higher-level proofs. These "waves" are just the most conservative schedule.

Like a giant PR that passes every test but is 13 million lines, unreviewable, and unmergeable into main: the functionality is genuinely correct, but it is not part of the team's codebase.

Buzzard called it an "extraordinary autoformalization achievement", while being clear about the costs:

• No new mathematics: it follows Darmon, Diamond and Taylor's simplified exposition of Wiles's proof, and borrows from prior work such as the Imperial College FLT project;
• Bloated: more than five times the size of Mathlib, which it builds on, and nearly twenty times the compile time on a 96-core machine;
• Can't enter the community library: these 13 million lines cannot currently go into Mathlib, and reviewers are generally reluctant to review large volumes of AI-generated code;
• A human-readable, explorable proof — one that lets people understand why it holds, and that later work can cite and improve — still has to be done by people.

Mechanistically, these correspond to three different objective functions. Verification only requires each step to be locally correct; the kernel does not care how long or roundabout the proof is. Understanding requires compression — a good proof reduces a mass of facts to a few key ideas. Reusability requires just the right abstraction — lemmas stated in general forms others can use. Optimization pressure was applied only to the first, so the second and third don't appear on their own and may even be sacrificed: the cheapest way to pass is often concrete, verbose and single-use.

The contrast with Day 60 is especially clear: the same generation of models finished years of planned work where there was a hard judge, and talked itself and its monitors into error where there wasn't. The difference is not that the model became more "honest", but whether the environment contains a check that cannot be persuaded.

# Two "proofs" of the same fact: both correct, wildly different in readability and reuse
def brute_proof(n):
    # Check case by case: every one is right, but you still don't know "why"
    return [(k, sum(range(1, k + 1)) == k*(k+1)//2) for k in range(1, n + 1)]

def insight_proof():
    # One idea: pair first and last, 1+k, 2+(k-1)... each pair is k+1, k/2 pairs
    return "sum(1..k) = k(k+1)/2 for every k, and reusable for arithmetic series"

steps = brute_proof(10_000)
print(all(ok for _, ok in steps), len(steps), "checks")
print(insight_proof())        # one line, covers infinitely many cases

Note: a Lean proof is not exhaustive enumeration; this only illustrates the gap between "stacking locally correct steps" and "one compressive idea".

• Anthropic, Formalizing Fermat's Last Theorem, 2026-09, anthropic.com/research — the main source: scale, axioms and comparator, early failures and Prove2Me; repository github.com/anthropics/fermats-last-theorem
• Kevin Buzzard, FLT: Anthropic has beaten me to it, Xena Project blog, 2026-09-04, xenaproject.wordpress.com — independent re-check and the assessment of costs
• Chen, Marwaha, Lu, Yuen, Peng, Prove2Me: An Open Collaborative Platform for Scaling Math Formalization, arXiv:2608.28433 (2026) — the statement DAG and statement/proof separation design
• The mathlib Community, The Lean Mathematical Library, arXiv:1910.09336 (CPP 2020) — how Mathlib is organized, to understand what "can't enter the library" means
• On this site: Day 42 Neuro-Symbolic · Day 46 AI for Science · Day 60 Alignment Post-Mortem of Real Incidents