Prove2Me: An Open Collaborative Platform for Scaling Math Formalization
Shuze Chen, Kunal Marwaha, Xiaoyang Lu, Henry Yuen, Tianyi Peng
cs.AI, cs.LO, cs.MA
2026-08-28
Prove2Me splits theorems from proofs and decomposes goals via proof-sketches. Bandit Algorithms yielded 151K Lean lines with 6 agents on ~$400 plans in 13 days.
Lean 4 can machine-check theorems. Large formalization projects still stall on people. Scholze's Liquid Tensor Experiment took about 18 months of community work. Kevin Buzzard's Fermat's Last Theorem effort is funded for five years; he has said he cannot finish it alone. AI agents now dump textbooks and papers into Lean at speed, but three bottlenecks remain. Faithfulness of a statement to the intended claim still needs a human. GitHub dumps of tightly coupled theorems are hard to reuse one lemma at a time. The impressive swarms run on one lab's internal compute.
Prove2Me tries to make formalization a crowd-sourced mission: humans audit a small core of statements, agents fill in proofs, and proofs can import one another.
The platform splits theorems and proofs into two immutable objects. A theorem card holds a natural-language description, a preamble, and a Lean statement ending in sorry. A proof must declare theorem solution with exactly that type and no sorry or new axioms. The backend checks the Curry-Howard match. Agents can also submit a negation as a disproof.
Human audit is confined to a mission's core: the goal theorem, its definitions, and milestone lemmas. The captain need not write Lean, but must click every core statement. An independent auditor agent does a read-back: it sees only the Lean declaration, not the source, and renders it as LaTeX so a human compares two math statements. Bourigault et al. report that a Lean-as-judge audit found only about 43% of proved statements faithful, which is why this human gate stays.
Collaboration runs through proof-sketches. A sorry-free proof may import other platform theorems, including still-open ones. Once a parent sketch is accepted, each child lemma becomes its own problem; when the children close, the parent auto-resolves. Immutability is what makes local correctness compose. Milestones pin canonical formalizations of key source lemmas so parallel agents do not fork incompatible restatements. Closed atomic theorems enter Formalpedia, searchable by the natural-language descriptions agents must file, and later sketches can import them. Credit accrues both for closing open theorems and for proposing statements that later proofs import.
Case studies from mid-June to late July 2026, which the paper flags as not a controlled experiment:
| Mission | Type | Lean LOC | Cost convention | Agents | Days |
| Gloeckle et al. algebraic combinatorics (external) | Textbook | 130K | $100k API | 30,000 runs | 7 |
| Exact Matrix Completion | Paper | 81K | $600 subscriptions | 9 | 16 |
| Sipser–Gács–Lautemann | Paper | 55K | $400 subscriptions | 3 | 8 |
| Bandit Algorithms | Textbook | 151K | $400 subscriptions | 6 | 13 |
| Introduction to Linear Optimization | Textbook | 17K | $200 subscriptions | 4 | 7 |
The largest Prove2Me mission matches the centralized swarm in size (151K vs 130K lines) with 6 agents on two consumer plans. The Sensitivity Conjecture mission closed all four milestones. API invoices and flat-rate subscriptions are not comparable.
The skill bar for contributing Lean drops from "knows the proof assistant" to "can steer an agent in natural language." For someone who wants a paper or textbook formalized, a mission keeps the audit surface on the core statements and lets agents invent intermediate lemmas. Formalpedia makes those lemmas independently importable, which a monolithic Git repo does not.
This is mechanism design, not a new prover. The platform does not claim to out-prove AlphaProof.
The case studies mix corpora, difficulty, working patterns, and model generations. They cannot separate a stronger model from the harness. Subscription cost is estimated as about $200 per month times the number of human contributors, which does not line up with Gloeckle et al.'s metered API bill.
Humans still audit the mission core. Statement faithfulness has no scalable automatic guarantee. Open submission invites junk and adversarial content; a reputation system is still a wish. How decentralized, asynchronous agents should share context is left open. Choosing what is worth formalizing, and how to cut milestones, remains human judgment.