Prove2Me: An Open Collaborative Platform for Scaling Math Formalization (Chen et al., 2026)

A preprint by Shuze Chen, Kunal Marwaha, Xiaoyang Lu, Henry Yuen and Tianyi Peng, submitted to arXiv on August 28, 2026 and revised August 31, 2026 (arXiv:2608.28433 [cs.AI], cross-listed cs.LO and cs.MA; DOI 10.48550/arXiv.2608.28433). Affiliations as listed on the paper are Columbia University's Graduate School of Business (Chen, Peng), the University of Chicago Department of Computer Science (Marwaha), Purdue University Department of Computer Science (Lu), and Columbia University Department of Computer Science (Yuen). No author is listed with an industry affiliation. The platform is at prove2.me.

Prove2Me is the platform on which Anthropic's computer-checked proof of Fermat's Last Theorem was produced (Formalizing Fermat's Last Theorem (Anthropic, September 2026)); that post describes Peng as an Anthropic researcher whose group at Columbia builds tools for AI formalization.

The argument

The paper's premise is that proof assistants such as Lean 4 "promise the paradigm of formally verified mathematics," but that large-scale formalization has been limited by the need for expertise in both formal verification and the underlying mathematics, and by the time required to write formal proofs. Two examples anchor the scale of the problem: Peter Scholze's Liquid Tensor Experiment required roughly eighteen months of sustained community effort, and the community formalization of Fermat's Last Theorem is funded for five years, with Kevin Buzzard acknowledging that he "cannot formalize it alone."

The paper's position is that AI coding agents have reduced those barriers enough that "human users can now use natural language to prompt agents to write complex proofs in Lean," which opens "the intriguing possibility of internet-scale mathematical collaboration involving both humans and AI agents, where correctness is machine-checked."

Three obstacles are identified in existing agent-driven formalization work:

• Auditing. The proof kernel certifies that a proof inhabits a statement, not that the statement captures the intended claim; an AI-generated statement "can be vacuous, miss a hypothesis, or drift semantically, yet still be 'proved'." The paper cites a Lean-as-judge audit finding only about 43 percent of proved statements faithful (Bourigault et al., 2026).
• Reusability. Formalizations are released as monolithic Git repositories of interdependent theorems; because Lean recompiles the downstream cone on any module change, integration serializes through a merge queue that becomes the bottleneck of large agent swarms, and individual results are hard to extract.
• Scale. Existing swarms "rely on a single organization's internal compute," with tens of thousands of agents and five-figure per-project budgets, "leaving the collective resources of the broader community untapped."

Design

The basic design decision is to separate the statement of a theorem from its proofs: each theorem is a standalone, immutable object stated once, which may carry multiple proofs by different agents. A theorem card holds a natural-language description, a preamble of imports (from Mathlib or from definition files hosted on the platform), and the formal Lean 4 statement, which must terminate in a := by sorry placeholder.

Audited missions are the mechanism keeping an agent-generated library trustworthy. Human review is confined in advance to a mission's curated core — its goal statement, the definitions it rests on, and the milestone lemmas structuring its proof — while agents introduce the remaining intermediate theorems freely. The paper presents this as pushing further a mitigation already common in the literature: shrinking the human audit surface to definitions and top-level statements rather than proofs.

Proof-sketches are the paper's central contribution to multi-agent collaboration. A proof may import other theorems already on the platform, including open theorems not yet proved; a proof that does so is a proof-sketch, establishing its target conditional on the imported statements. By the Curry–Howard correspondence, importing a theorem is equivalent to assuming a term of that type. Combined with the platform's immutability rule — every statement and proof-sketch is persistent and cannot be edited once submitted — this yields the paper's stated Property 1: a theorem is verified if all its imported child lemmas are verified. Each child lemma then becomes an atomized problem an agent can attack without downloading or compiling the parent, and the parent auto-resolves once the children close. The worked example is Huang's 2019 proof of the Sensitivity Conjecture, decomposed into Cauchy's interlace theorem, the spectrum of the iteratively defined matrix family, a max-degree spectral bound, and a small assisting lemma.

The paper explains why the obvious alternative fails: asking agents to fill sorry placeholders directly in shared files is computationally expensive, because a change to a downstream lemma forces recompilation of every dependent file, and the work resists atomization, because concurrent edits to the same file interfere. Git workflows mitigate this at the cost of centralizing review in human maintainers or an orchestrating agent — "a bottleneck that becomes prohibitively expensive for a decentralized platform."

Milestones are lemma-level sub-targets curated by a mission's captain, each pairing an authoritative natural-language statement, usually transcribed verbatim from the source paper or textbook, with a link to its canonical formalization once attested. The paper identifies two consensus failures they address: independent agents formalizing the same lemma in mutually incompatible ways, so that parallel effort is duplicated rather than accumulated, and a formalization that silently deviates from the source contaminating every proof-sketch that imports it.

Formalpedia is the library that results. Because every statement is atomized and immutable and carries the context needed to compile on its own, any proved theorem becomes a building block for any later proof-sketch in any mission. The paper positions Formalpedia at the application layer, building on curated foundational libraries such as Mathlib, CSLib and PhysLib rather than competing with them, and distinguishes it from Lean-verified registries such as Palomar and TheoremDB on two grounds: every statement is individually importable, and an accompanying harness opens formalization work itself to a broader community. It also distinguishes Prove2Me from the Tau Ceti Project, which targets a foundation-layer library downstream of Mathlib and "explicitly disavows frontier results such as recent research papers."

A discussion channel lets agents post progress and findings in real time. The paper reports observing agents correcting one another: in the Sensitivity Conjecture mission, one agent proposed a proof-sketch importing a theorem named gotsman_linial, which a second agent disproved; prompted by the disproof, the first agent proposed gotsman_linial_with_zero supplying the missing boundary condition, and the corrected theorem closed the branch.

Case study

Between mid-June and the end of July 2026, contributors completed several missions. The paper reports four in a table alongside, for context, the algebraic combinatorics textbook formalized by the centralized agent swarm of Gloeckle et al. (2026). The Sensitivity Conjecture mission used as the running example was also closed, with all four milestones reached.

† metered API inference, estimated in Gloeckle et al. (2026). ‡ flat-rate consumer subscriptions, priced by the authors as Claude and ChatGPT Max plans at roughly $200 per month times the number of human contributors. The paper states plainly that the two cost conventions are not comparable and that "Table 1 reports case studies, not a controlled experiment" — corpora, difficulty, working patterns and model generations differ across rows. What it takes the table to show is the resource footprint of a project-scale Lean development: the largest Prove2Me mission is comparable in size to the centralized swarm's (151K against 130K lines) and was closed by 6 agents on two consumer subscriptions, against 30,000 agent runs on metered API inference. The authors name the confound explicitly — a stronger model generation and a harness built for multi-agent proving are not separated by these data, and doing so "requires holding the model fixed and varying only the harness, which we leave to future work."

Using the platform

The paper includes a quick-start section. Any agent with shell or terminal access works — it names Claude Code, Codex, Cursor, OpenClaw, OpenCode, GitHub Copilot and Antigravity — while webpage chatbots cannot be used directly because they cannot run code to make the platform's API calls. Setup is a single instruction pointing the agent at prove2.me/start.md; the agent then chooses an onboarding path from its own capabilities, installs the pinned toolchain (elan with the exact Lean and Mathlib revisions the platform verifies against), and mirrors the server's module layout in three local folders of definitions, theorems and solutions. A local Lean installation is optional, since the server verifies every submission. Human users drive the work in natural language, and the paper tabulates the common instructions.

Stated limits and open questions

The conclusion states that "Prove2Me's vision is not to replace mathematicians": choosing what is worth formalizing, decomposing it into milestones, and judging whether a formal statement says what it is meant to say "all remain matters of human judgment; agents supply the mechanical labor beneath those decisions." Agents are required to write a detailed natural-language account of every statement and proof they submit so the output stays legible to people.

Four open problems are named: how agents should search a large, evolving corpus of formal statements as Formalpedia grows; how decentralized asynchronous agents can exchange harnesses, lessons and context to learn continually; how the platform can reject adversarial or low-quality submissions and build community trust, for instance through a reputation system; and how to extract human-legible insight from machine-generated proofs.

Relationships

• supports: Formalizing Fermat's Last Theorem (Anthropic, September 2026)
• supports: Autoformalization and Machine-Checked Proof
• supports: AI for Science
• related: Agentic AI
• related: Agent Architecture Patterns
• related: Verification Asymmetry
• related: Anthropic