2026-09-05
Prove2Me has humans audit a small core while agents co-write Lean. Bandit Algorithms closed at 151K lines with 6 agents in 13 days for about $400.
Lean 4 can check mathematics by machine, but contributors have had to be fluent in both the math and the prover. The Liquid Tensor Experiment took the community about eighteen months. Buzzard's Fermat formalization is funded for five years, and he has said he cannot do it alone. AI provers now write serious Lean, yet current projects still stall in three places: humans cannot audit libraries that grow by hundreds of thousands of theorems; GitHub developments are tightly coupled, so a single result is hard to reuse; and large agent swarms sit on one lab's internal compute.
Prove2Me wants formalization to be crowd work for anyone with a terminal-capable agent. A circulating Chinese claim that Claude formalized Fermat in eleven days with 13 million lines of Lean is not a result in this paper. Fermat appears only as motivation. The missions actually closed are matrix completion, a complexity theorem, and textbooks.
Statements and proofs are split. Each theorem is an immutable object whose statement ends in sorry. A proof submission must match that type exactly, contain no sorry and no new axioms, and compile in the platform's chosen Lean kernel. A human captain launches a mission: a headline goal, its definitions, and milestone lemmas form the audited core; intermediate lemmas are left for agents. Faithfulness is checked by a second agent that sees only Lean, translates it back to natural language, and is compared with the source, so the captain need not read prover code.
Collaboration runs on proof-sketches: a sorry-free proof may import other platform theorems, including ones still open. Huang's Sensitivity Conjecture splits into a degree bound, Cauchy interlacing, a matrix spectrum, and helpers; when the children close, the parent resolves. The same import path turns proved results into Formalpedia, a searchable library of reusable blocks. Milestones are authoritative statements copied from the source so parallel agents do not formalize the same lemma incompatibly. Agents also correct each other in a discussion channel: a gotsmanlinial import was disproved, then repaired with a boundary condition that closed the branch.
Onboarding is one instruction: point the agent at prove2.me/start.md. Webpage chatbots are out, because the agent has to run code against the API.
Case studies from mid-June to late July 2026, not a controlled experiment. Cost bases differ: the comparison row is metered API; Prove2Me rows price consumer Max plans at about $200 per month times the number of humans.
| Mission | Type | Lean LOC | Cost | Agents | Days |
| Algebraic Combinatorics (Gloeckle et al.) | textbook | 130K | $100,000 API | 30,000 | 7 |
| Exact Matrix Completion | paper | 81K | $600 | 9 | 16 |
| Sipser–Gács–Lautemann | paper | 55K | $400 | 3 | 8 |
| Bandit Algorithms | textbook | 151K | $400 | 6 | 13 |
| Introduction to Linear Optimization | textbook | 17K | $200 | 4 | 7 |
The largest Prove2Me mission, 151K lines, is in the same size band as the 130K centralized swarm, with 6 agents and two subscriptions. The Sensitivity Conjecture running example also closed, all four milestones marked. The authors say a stronger model generation and a multi-agent harness are confounded in every row.
The unit of formalization becomes an importable theorem rather than a lab git repo. Humans audit whether the core says what the source meant; agents supply partitionable labor. Consumer subscriptions producing 100K-line Lean shifts the bottleneck from the compute bill to audit protocol and search.
Table 1 is explicitly a case study. Model generation and harness are mixed; there is no hold-the-model, vary-the-platform ablation. Humans still audit the core, so captains and moderators become the next bottleneck at scale. Kernel acceptance is not semantic fidelity; a cited Lean-as-judge audit passes only about 43% of proved statements. How to coordinate decentralized asynchronous agents is left open. How to search Formalpedia as it grows has no benchmark yet.