Prove2Me

Prove2Me is an open collaborative platform for formalizing mathematics in Lean 4, built by a group led by Tianyi Peng at Columbia University. A user who proposes a project, called its captain, turns a paper, a textbook, or an open problem into a "mission": a set of audited Lean statements that anyone's AI coding agent can try to prove, with every submission checked by the Lean kernel on the platform's servers. Statements are stored separately from their proofs as immutable objects, a proof may import other statements (including ones nobody has proved yet) to decompose a hard theorem into smaller problems, and every proved result joins a searchable public library the project calls Formalpedia.^[1][4] The platform is described in an arXiv paper by Shuze Chen, Kunal Marwaha, Xiaoyang Lu, Henry Yuen and Tianyi Peng, first posted on August 28, 2026.^[1] It drew wide attention on September 4, 2026, when Anthropic said its Claude agents completed the first end-to-end computer-checked proof of Fermat's Last Theorem after the company "switched to using Prove2Me" for the attempt.^[14] As of September 5, 2026 the site listed 128 missions, 101 of them completed, and a Formalpedia of about 56,800 theorems, roughly 45,000 of them machine checked (the counts moved during the day).^[3][11]

Background and motivation

Formal verification means writing a proof in a language precise enough that a computer checks every step, and Lean 4 with its Mathlib library is the system most large formalization projects now use.^[4] The paper opens with the human cost of that work (Peter Scholze's Liquid Tensor Experiment took roughly eighteen months of community effort; Kevin Buzzard's Fermat's Last Theorem project is funded for five years) and argues that AI coding agents have lowered the barrier, since a person can now prompt an agent in natural language to write Lean. That opens the possibility of "internet-scale mathematical collaboration involving both humans and AI agents, where correctness is machine-checked".^[1][2]

The paper names three obstacles that existing agent-driven formalization efforts still face. The first is auditing: the Lean kernel certifies that a proof inhabits a statement, not that the statement says what the source intended, and the authors cite a Lean-as-judge audit (Bourigault et al., 2026) that found only about 43% of proved statements faithful. The second is reusability: prior Lean formalizations tend to live on GitHub as tightly interdependent theorems that are hard to extract individually, and Lean recompiles the whole downstream cone whenever a module changes, so integration is serialized through a single merge queue. The third is scale: the agent swarms that have formalized whole textbooks ran on a single organization's compute, with "tens of thousands of agents and five-figure budgets per project", leaving the public's collective token budget untapped.^[2]

Prove2Me's stated answer is fourfold: a low barrier to entry (anyone with an agent can contribute Lean proofs "without expertise in Lean or even in the underlying mathematics"), a mission design that confines human auditing to a small curated core, a collaboration mechanism that decomposes proofs into atomized tasks, and a reusable library that grows as missions complete.^[2] The FAQ puts the relationship to the Lean ecosystem plainly: foundational libraries such as Mathlib, CSLib, PhysLib and Tau Ceti provide general-purpose foundations, registries such as Palomar record finished formalizations, and Prove2Me "covers the stretch in between", turning a user's own goal into a mission other people's agents can help complete.^[4]

How it works

Theorems as immutable cards

The basic design decision is to separate a theorem's statement from its proofs. Each theorem is a standalone, immutable object that is stated once and may collect many independent proofs, possibly from different agents.^[2] A theorem card carries a natural-language description of the mathematics, a preamble of imports (from Mathlib or from definition files hosted on the platform), and the formal Lean 4 statement, which must end in a := by sorry placeholder. A submission can also carry a source link to the originating paper or textbook and subject tags.^[2] Everything about a theorem except its Lean statement can be edited by its submitter afterwards; the statement itself, like every proof, can never be edited, only deprecated and re-uploaded.^[4]

Each theorem belongs to exactly one verification environment, pinned to a specific Lean toolchain and Mathlib revision, and environments are fully isolated: a proof can only import results that live in the same environment.^[4][8] As of September 5, 2026 the agent documentation listed three environments.^[8]

Scroll sideways for more →

Proofs, disproofs and verdicts

A proof submission is a Lean file declaring a theorem named solution whose type matches the target theorem's type exactly and which contains no sorry and no new axioms. The platform compiles it in the target's environment and checks that the two types match as Lean terms, relying on the Curry-Howard correspondence at the heart of Lean: a proof of a proposition is a term whose type is that proposition.^[2] A disproof is the same mechanism applied to the negation of the target statement.^[2][4] Every proof's axioms are checked against a whitelist, and agents must upload a natural-language explanation of the proof idea alongside the Lean file.^[2][5] Because every submission goes through the kernel, the site says a wrong proof "cannot enter the library, no matter how confident the agent was".^[4]

The agent-facing API returns one of a fixed set of verdicts.^[8]

Scroll sideways for more →

Proof-sketches and the decomposition graph

The mechanism that lets agents build on one another is the proof-sketch. A proof on Prove2Me may import other platform theorems, including open theorems that have not been proved yet; a sketch establishes the target conditional on its imports and defers their proofs to separate submissions. Because statements and sketches are immutable, an accepted sorry-free sketch gives a permanent guarantee: the parent theorem is verified once all imported children are verified. Each child immediately becomes a new, self-contained open problem that any agent can attack without downloading or compiling the parent, and when the last child closes, the parent resolves automatically.^[2] The paper's running example is Hao Huang's 2019 proof of the Sensitivity Conjecture, which reduces to Cauchy's interlace theorem, a spectral bound on the maximum degree, and a lemma about the eigenvalues of a recursively defined matrix; each became a node in the decomposition graph and the mission closed with all four milestones reached.^[2]

The paper contrasts this with the obvious alternative, asking agents to fill sorry placeholders in a shared set of files. That approach fails, the authors say, because any change forces recompilation of every dependent file and because interdependent edits to the same files cannot be cleanly partitioned across agents; Git-based workflows used by other large Lean projects mitigate this at the cost of a central merge queue.^[2] Anthropic later credited the same separation of statements and proofs into different files with "speeding up Lean compilation and minimizing resource consumption" during its Fermat run.^[14]

Missions, captains and audited cores

Because anyone with an agent can post a statement, statements may be false, ill-defined or hallucinated. Prove2Me's answer is the mission: a headline goal (the main theorem of a paper, a book chapter, or an open problem), the definitions it rests on, and the milestone lemmas that structure its proof. Humans audit this core before the mission goes live and audit nothing beyond it; agents then introduce intermediate lemmas freely, because "a wrong lemma simply can't help prove a correctly-stated goal".^[2][5]

A mission is created by a captain, the human who proposes it. Captains do not need to write Lean: their agent drafts a mission proposal, a private, editable bundle of the goal, definitions and milestones. What the captain cannot delegate is the audit: the person must confirm each statement individually before the drafts are compiled and published as immutable theorems, and a platform moderator reviews a public mission before it goes live.^[2][9] To make that audit possible for people who do not read Lean, an independent auditor agent is given each Lean declaration and its definitions, but not the source, and translates it back into ordinary mathematical notation, making every binder and hypothesis explicit. The human then compares the source statement with the read-back, "math to math, not code".^[2][5]

Scroll sideways for more →

Private missions let a researcher verify an unpublished paper while still importing public Formalpedia theorems; releasing one to the public catalog is permanent.^[4][9]

Milestones

Decomposition alone does not make decentralized work compose. The paper describes two ways consensus can fail: several agents formalize the same lemma in incompatible ways, so their work cannot be combined, or one formalization silently drifts from the source and contaminates every sketch built on it. Milestones address both. A milestone pairs an authoritative natural-language statement, usually transcribed verbatim from the source, with a link to the platform theorem the captain has attested as its canonical formalization. They are ordered, since later milestones typically depend on earlier ones, and they are the entry point to a mission rather than the raw graph: an agent formalizes against the milestone's statement instead of inventing a restatement, and reuses a milestone whose theorem is already proved. When every milestone is proved and connected by sketches, the goal auto-resolves and the mission is complete.^[2] Linking a theorem to a milestone is an attestation, and solvers are told to use linked declarations as-is without re-checking them.^[9]

Formalpedia, search and credit

Because every statement is atomized and immutable and carries all the context it needs to compile, any proved theorem can be imported by any later sketch in any mission. The resulting cross-mission library is Formalpedia, which the authors present as building on Mathlib, CSLib and PhysLib rather than competing with them, focused on "the application layer, where results are one-off and mutually independent".^[2] The harness requires every agent to submit a standardized natural-language description with each Lean statement, and a search API indexes those descriptions; agents are instructed to search before they submit and to introduce a new statement only when none exists.^[2] Anthropic listed this natural-language description among the things that helped its Fermat run, "resulting in a simpler proof path".^[14]

Credit is permanent and attached to the contributor whose agent proved a theorem first. A contributor also earns credit when a statement they proposed is later imported by other proofs, which the paper calls the platform's form of citation, and both feed a trust score that ranks users.^[2][4][7] The users page listed roughly 190 to 200 accounts during September 5, 2026, with ranks such as Grandmaster and Master; the earliest accounts, including those of Chen and Peng and a "Community (Bot)" account that captains open-problem missions, date from March 2026.^[12]

Connecting an agent

Any coding agent with shell or network access can take part; the paper and FAQ name Claude Code, Codex, Cursor, OpenClaw, opencode, GitHub Copilot and Antigravity, and note that web chatbots cannot be used directly because they cannot run code to call the API.^[2][4] Setup is a single instruction: point the agent at prove2.me/start.md. That file tells the agent to clone the open-source prove2me_workspace repository (public on GitHub since July 3, 2026) if it has git and shell access,^[13] or to fetch the same documentation over HTTP if it does not, and then to read SKILL.md, which documents the REST API under https://prove2.me/api/v1 (registration, environments, theorem search, proof submission and polling, decomposition graphs, open leaves, mission proposals, milestones, votes and tags).^[6][7] The workspace mirrors the server's layout with three folders, Definitions/, Theorems/ and Solutions/, so local and server-side verification agree; a local Lean installation is optional because the server verifies every submission.^[2][7] After setup the human drives everything in plain language, for example "Work on the next open milestone of <mission_name>" or "Draft a mission proposal for and hand it to me to review".^[2][5] The agent authenticates with a 30-day API key exchanged for one-hour access tokens, and all submission endpoints are asynchronous, so agents can run unattended for days.^[4][7] The FAQ says the platform itself is free and that proving runs on the user's own agent subscription.^[4]

Missions and results

Case studies reported by the authors

The paper reports that contributors completed several missions between mid-June and the end of July 2026 and tabulates four of them alongside the centralized swarm of Gloeckle et al. (2026), which formalized an algebraic combinatorics textbook in about 130,000 lines of Lean with 30,000 agents on an estimated $100,000 of metered API inference. The project's August 27 blog post extends the table.^[2][10] Costs in the Prove2Me rows are the authors' convention of roughly $200 per month of a Claude or ChatGPT Max plan times the number of human contributors, not API billing, and the "agents" column counts subagents launched by one person; the paper stresses these are case studies rather than a controlled experiment and that a stronger model generation and the harness are confounded in every row.^[2][10]

Scroll sideways for more →

The blog post flags that the matrix multiplication mission reused results already proved on the platform in an earlier mission on Schönhage's bound, so its two days are "not on the same footing as the other rows", and describes Markov Chains and Mixing Times as a graduate textbook split into 13 chapter missions and completed by one user with a $200 Claude Code subscription over a weekend.^[10] The site's FAQ shows a shorter version of the same table with slightly different figures (four agents rather than six for Bandit Algorithms, and costs given as weeks of a subscription).^[4]

Public missions as of September 2026

On September 5, 2026 the missions page counted 27 open and 101 completed missions, 128 in all, each tagged by field and typed as a research paper, a textbook, or an open problem.^[3] Open missions listed that day included the following.

Scroll sideways for more →

The open-problem missions are stated as Lean goals whose partial progress is banked in Formalpedia; the FAQ notes that "a disproof is a result too".^[4] Formalpedia itself reported about 56,800 theorems, roughly 45,000 of them machine checked, on the same day.^[11]

Role in Anthropic's Fermat's Last Theorem formalization

Prove2Me's most visible use is the formalization of Fermat's Last Theorem that Anthropic announced on September 4, 2026. According to Anthropic, Tianyi Peng, described as an Anthropic researcher whose group at Columbia builds tools for AI formalization, set out to test whether Claude could make progress on FLT. Several initial attempts failed: agents had early success but "quickly lost track of the project's state and stopped collaborating effectively", though their work contributed about 7% of the non-boilerplate lines of the final proof. "The effort succeeded when we switched to using Prove2Me," the company wrote, listing three things the platform did: it maintained a directed acyclic graph of theorem statements that agents used to decide what to attempt next, which mitigated memory degradation and allowed parallel work; it sped up Lean compilation by separating statements and proofs into different files with the links maintained independently; and it enabled search and reuse through the natural-language description of each statement.^[14]

Anthropic's accompanying timeline document describes the run as using "a new harness based on Prove2Me, a platform developed by Anthropic researcher Tianyi Peng's group at Columbia University", and defines a "card" as Prove2Me's unit of work: one theorem statement posted as a node in the shared dependency graph, together with its proof once one is accepted. Day 1 was August 7, 2026; about 2,100 theorems were proved on the platform by Day 2, more than 10,000 by Day 6, and the root card fermat_last_theorem read "Proved" at 02:00:57 UTC on August 18 (10:00:57 pm Eastern on August 17). The platform's running total at the close was about 30,300 statements, of which 29,511 sit in the final theorem's dependency tree.^[15] The document is explicit that a "Proved" mark on the platform is not an end-to-end check, because Prove2Me compiles each card's proof separately against only the statements of its children; Anthropic recompiled all 29,511 cards from source outside the platform the next morning, built the whole tree as one Lean project, and ran the Lean FRO's comparator and the independent nanoda kernel over the result.^[15] One agent said as much to the project's readers minutes after the close, writing that until the off-site recheck read clean "the honest sentence is 'proved on prove2me, pending the independent re-check' rather than 'FLT is formalized'".^[15]

The run used dozens of Claude agents in a Claude Code-based multi-agent harness and about six billion output tokens from an internal research model Anthropic called "roughly comparable to Claude Fable 5.1".^[14] Human mathematical input was limited to occasional high-level instructions from Peng.^[14] In a post-run assessment that Anthropic quotes but says it has not independently verified, Claude listed a cost of the card-by-card approach: "Each card was proved in isolation", roughly two in five theorem statements in the proof files repeat a statement made elsewhere word for word, and one basic lemma is re-declared in over 300 files.^[15] Anthropic's own footnote says the proof "is likely much longer than it needs to be".^[14]

Anthropic also reported a smaller experiment in which its researchers used three personal Claude Max plans to formalize applications of the Hardy-Littlewood circle method. Collaborating entirely through Prove2Me, the agents completed a formalization of Vinogradov's three-primes theorem in three days, which the company offered as evidence that "collaborative formalization of major results with consumer AI subscriptions is achievable" given the right scaffold.^[14]

People

The paper's authors are Shuze Chen (Graduate School of Business, Columbia University, corresponding author), Kunal Marwaha (Department of Computer Science, University of Chicago), Xiaoyang Lu (Department of Computer Science, Purdue University), Henry Yuen (Department of Computer Science, Columbia University) and Tianyi Peng (Graduate School of Business, Columbia University, corresponding author).^[2] Chen writes the project's blog, and on September 5, 2026 his profile listed 90 missions, 63 of them captained; Peng's listed 17 missions and 8 captained, and Marwaha's 4 missions and 5 captained.^[10][12]

Anthropic introduces Peng as an Anthropic researcher whose Columbia group builds tools for AI formalization, and its post carries a footnote on why he cares about verification: as an undergraduate, his research advisor wanted to include results from Peng's thesis in a Nature article and asked whether he was sure the proof was correct. Peng answered that he was "99% sure, but it's hard to be 100% certain about a proof this long", and the work was not published in Nature.^[14]

Reception

Kevin Buzzard, who leads the Imperial College London FLT project and reviewed Anthropic's proof, wrote on September 4, 2026 that one of Anthropic's internal models, "using the prove2.me platform", had formalized a complete proof of FLT in Lean, the last item on Freek Wiedijk's list of 100 formalization challenges.^[16] The Anthropic post reached the front page of Hacker News the same day; by the morning of September 5 UTC it had about 580 points and about 360 comments, and several commenters focused on the platform, one noting that the success "required tooling crafted by humans" and another that Prove2Me "uses a graph like previous automated theorem provers".^[17]

The authors describe Prove2Me as "at an early stage and iterating quickly" and list open questions: how agents should search a large, evolving corpus of formal statements; how decentralized, asynchronous agents can exchange harnesses, lessons and context; how the platform can reject adversarial or low-quality submissions, for instance through a reputation system; and how to extract human-legible insight from machine-generated proofs. They stress that choosing what to formalize, decomposing it into milestones and judging faithfulness remain matters of human judgment: "Humans are the platform's first principle".^[2]

See also

• Formalization of Fermat's Last Theorem
• Lean and Mathlib
• Automated theorem proving
• AlphaProof and DeepSeek-Prover
• Coding agents

References

1. ^Prove2Me: An Open Collaborative Platform for Scaling Math Formalization (abstract) - arXiv (Shuze Chen, Kunal Marwaha, Xiaoyang Lu, Henry Yuen, Tianyi Peng), submitted August 28, 2026, v2 August 31, 2026.
2. ^Prove2Me: An Open Collaborative Platform for Scaling Math Formalization (full text, v2) - arXiv HTML (Chen, Marwaha, Lu, Yuen, Peng), August 31, 2026.
3. ^Prove2Me: Missions - Prove2Me, accessed September 5, 2026.
4. ^FAQ - Prove2Me, accessed September 5, 2026.
5. ^About Prove2Me: How Prove2Me works - Prove2Me, accessed September 5, 2026.
6. ^Prove2me: Agent Onboarding (start.md) - Prove2Me, accessed September 5, 2026.
7. ^SKILL.md: Prove2me, an open-source platform for math formalization at scale (version 0.9.6) - Prove2Me, accessed September 5, 2026.
8. ^references/prove.md: Lean environments, submitting proofs, verdicts and reductions - Prove2Me, accessed September 5, 2026.
9. ^references/mission_captain.md: Mission captain playbook - Prove2Me, accessed September 5, 2026.
10. ^Intro to Prove2Me I: Formalizing a textbook in a week - Prove2Me blog (Shuze Chen), August 27, 2026.
11. ^Formalpedia - Prove2Me, accessed September 5, 2026.
12. ^Users - Prove2Me, accessed September 5, 2026.
13. ^prove2me/prove2me_workspace - GitHub (repository created July 3, 2026; metadata fetched September 5, 2026).
14. ^Formalizing Fermat's Last Theorem - Anthropic, September 4, 2026.
15. ^Formalizing Fermat's Last Theorem in Lean: A timeline and selected excerpts from Claude's reasoning - Anthropic (PDF accompanying the September 4, 2026 post).
16. ^FLT: Anthropic has beaten me to it - Xena Project (Kevin Buzzard), September 4, 2026.
17. ^Formalizing Fermat's Last Theorem (discussion) - Hacker News, September 4, 2026 (snapshot of points, comment count and quoted comments taken September 5, 2026 via the Algolia HN API).