Prove2Me: An Open Collaborative Platform for Scaling Math Formalization

Summary (Overview)

• Prove2Me is an open-source collaborative platform that enables large-scale mathematical formalization by treating AI agents as first-class participants, allowing anyone with an AI agent to contribute Lean 4 proofs without requiring expertise in formal verification or even the underlying mathematics.
• The platform introduces audited missions, where human auditing is confined to a small curated core of statements (goal theorems, definitions, and milestone lemmas), while AI agents freely generate intermediate theorems at scale—resolving the tension between human auditing (which doesn't scale) and agent-generated content (which does).
• A key mechanism, proof-sketches, enables decomposition of complex theorems into atomized, independently solvable sub-problems. Proofs can import other theorems (including open ones), allowing agents to build on one another's work and enabling clean partitioning of effort across decentralized agents.
• The platform's Formalpedia library grows organically: every theorem is an immutable, standalone, individually importable object, making results reusable across missions and creating a searchable corpus of formalized mathematics.
• Case studies show that project-scale formalizations (81K–151K lines of Lean) can be completed by just 3–9 agents on consumer subscriptions (costing $200–$600), compared to 30,000 agent runs on metered API inference costing $100,000 for comparable centralized swarms.

Introduction and Theoretical Foundation

Background and Motivation

The dream of a fully formalized mathematical corpus has long been limited by human effort. The authors cite two prominent examples:

• Liquid Tensor Experiment (Peter Scholze): required ~18 months of sustained community effort [Commelin et al., 2022]
• Fermat's Last Theorem formalization: funded for five years, with leader Kevin Buzzard acknowledging he "cannot formalize it alone" [Buzzard, 2024]

Formalization has traditionally been confined to specialists who are simultaneously expert in mathematics and proof-assistant engineering.

The Turning Point: AI-Driven Theorem Proving

Recent AI advances offer a turning point:

• DeepSeek-Prover series reaching 88.9% on miniF2F [Xin et al., 2024, 2025; Ren et al., 2025]
• AlphaProof's silver-medal IMO performance [Hubert et al., 2026]
• Multi-agent swarms formalizing a 500-page graduate combinatorics textbook in ~a week [Gloeckle et al., 2026]

Three Obstacles to Scale

1. Auditing: The proof kernel certifies that a proof inhabits a statement, but not that the statement faithfully captures the intended claim. A recent Lean-as-judge audit finds only ~43% of AI-generated statements are faithful [Bourigault et al., 2026].

2. Reusability: Existing formalizations are monolithic Git repositories of tightly interdependent theorems. Since Lean recompiles the entire downstream cone when a module changes, integration is serialized through a single merge queue—the empirical bottleneck of large swarms.

3. Scale: Current swarms rely on a single organization's internal compute (tens of thousands of agents, five-figure budgets). The collective token budget of the general public remains untapped.

Theoretical Foundation: Curry–Howard Correspondence

The platform relies on the Curry–Howard correspondence [Wadler, 2015] at the heart of Lean 4: a proof of a proposition is a term whose type is that proposition. This enables:

• Statement-proof separation (each theorem is standalone and immutable)
• Proof checking via type checking (a proof submission must declare theorem solution whose type matches the target exactly, with no sorry or new axioms)
• Importing a theorem = assuming a term of that type (enabling proof-sketches with open theorems)

Methodology

Platform Design: Statement-Proof Separation

Each theorem is a standalone, immutable object with a theorem card containing:

• DESCRIPTION: natural-language account of the mathematics
• PREAMBLE: imports (from Mathlib and other platform definition files)
• FORMAL STATEMENT: the Lean 4 target statement, terminating in := by sorry
• SOURCE: link to originating paper/textbook (optional)
• TAGS: subject classification

The running example is Lemma 3.1 from the Sensitivity Conjecture proof [Huang, 2019]:

Lemma 3.1. Suppose $H$ is an $m$-vertex undirected graph, and $A$ is a symmetric adjacency matrix whose entries are in $\{-1, 0, 1\}$. Then the matrix degree of $H$ satisfies

$$\Delta(H) \geq \lambda_1 := \lambda_1(A).$$

Formalized as max_degree_ge_lambda_max in Lean 4:

theorem max_degree_ge_lambda_max
{V : Type*} [Fintype V] [DecidableEq V]
{A : Matrix V V ℝ} (hA : A.IsHermitian)
(h_entries : ∀ u v : V, A u v = -1 ∨ A u v = 0 ∨ A u v = 1)
(adj : V → V → Prop) [DecidableRel adj]
(h_zero : ∀ u v : V, ¬ adj u v → A u v = 0)
[Nonempty V] :
∃ v : V, hA.eigenvalues₀ ⟨0, Fintype.card_pos⟩
≤ ((Finset.univ : Finset V).filter fun u => adj u v).card := by sorry

Proof Submission

A proof submission is a Lean file declaring theorem solution with exactly the target's type, containing no sorry or new axioms. The platform compiles in the same environment and checks type equality. Agents may also submit disproofs (type ¬(target statement)). Every proof requires a detailed natural-language explanation.

Audited Missions

Mission structure: A mission = headline goal + dependent definitions + milestone lemmas. Humans audit only this core before release.

Captain workflow:

1. Captain's agent drafts the mission proposal (goal, definitions, milestones)
2. Captain must click each statement individually to confirm (cannot be delegated)
3. Confirmed drafts compile and publish as immutable theorems
4. Platform moderator reviews before going live

Sub-agent read-back: To lower the barrier for human auditors who can't read Lean, an independent auditor agent translates Lean code back into LaTeX mathematics, unfolding non-standard definitions. The human compares two mathematical statements (source vs. read-back) rather than inspecting Lean directly.

Proof-Sketches: The Key Collaboration Mechanism

Why naive sorry-filling fails:

1. Computational cost: Changing a downstream lemma requires recompiling all upstream files; Mathlib compilation is notoriously slow
2. Hard to atomize: Concurrent edits to shared files interfere; work cannot be cleanly partitioned

The solution: Proofs can import other platform theorems, including open ones. A proof-sketch establishes the target conditional on imported statements, deferring their proofs to separate submissions.

For Huang's Sensitivity Conjecture (Theorem 4.1):

Theorem 4.1. For every integer $n \geq 1$, let $H$ be an arbitrary $(2^{n-1} + 1)$-vertex induced subgraph of the $n$-dimensional hypercube graph $Q^n$, with maximum degree $\Delta(H)$. Then $\Delta(H) \geq \sqrt{n}$.

The proof-sketch imports:

• Lemma 3.1 (max_degree_ge_lambda_max)
• Lemma 4.2 (Cauchy's Interlace Theorem): For symmetric $n \times n$ matrix $A$ with eigenvalues $\lambda_1 \geq \lambda_2 \geq \cdots \geq \lambda_n$ and $m \times m$ principal submatrix $B$ with eigenvalues $\mu_1 \geq \cdots \geq \mu_m$:

$$\lambda_i \geq \mu_i \geq \lambda_{i + n - m}, \quad 1 \leq i \leq m$$

• Lemma 4.3 (Spectrum of $A_n$): Defined iteratively:

$$A_1 = \begin{bmatrix} 0 & 1 \\ 1 & 0 \end{bmatrix}, \qquad A_n = \begin{bmatrix} A_{n-1} & I \\ I & -A_{n-1} \end{bmatrix}$$

$A_n$ is a $2^n \times 2^n$ matrix with eigenvalues $\sqrt{n}$ (multiplicity $2^{n-1}$) and $-\sqrt{n}$ (multiplicity $2^{n-1}$).

Property 1 (Formal guarantee): Theorem 4.1 is verified if all imported child lemmas are verified.

Immutability ensures local correctness composes into global correctness, enabling clean partitioning of effort across agents, recursively down to every leaf.

Formalpedia: Reusable Theorem Corpus

• Every statement is atomized, immutable, and individually importable
• Search API indexes standardized natural-language descriptions
• Agents are instructed to search before submitting (reuse > introduce)
• Citation incentive: contributors earn credit for theorems others import

Milestones: Curated Checkpoints

A milestone = authoritative natural-language statement (transcribed from source) + link to canonical formalization. Milestones are:

• Idempotent: independent attempts converge on one canonical statement
• Authoritative: downstream proofs build without re-auditing
• Ordered: later milestones depend on earlier ones

Multi-Agent Continual Learning

• Discussion channel for agents to share progress and lessons
• Observed agents correcting each other: one agent's gotsman_linial theorem was disproved by a second agent; the first revised it to gotsman_linial_with_zero with the missing boundary condition, closing the branch

Empirical Validation / Results

Completed Missions (mid-June to end of July 2026)

† metered API inference (estimated in Gloeckle et al. [2026]); ‡ flat-rate consumer subscriptions (Claude and ChatGPT Max at ~$200/month × human contributors)

Key Observations

• The largest Prove2Me mission (151K LOC) is comparable to the centralized swarm (130K LOC) but was closed by 6 agents on 2 consumer subscriptions vs. 30,000 agent runs on metered API inference
• The Sensitivity Conjecture mission was closed with all four milestones reached
• The smallest mission: one subscription with four subagents produced 17K lines in a week
• Two explanations are confounded: stronger model generation and the harness design; separating them requires holding the model fixed and varying only the harness (left to future work)

Theoretical and Practical Implications

Auditing at Scale

Prove2Me resolves the fundamental tension between human auditing (which doesn't scale) and agent-generated content (which does) by fixing the audit surface in advance. The trusted object is not the agent's chosen decomposition but the Lean kernel's acceptance of proofs of audited statements. Intermediate lemmas matter only insofar as they help close audited goals.

Decentralized Collaboration

The platform demonstrates that formalization can tap the collective token budget of the general public rather than requiring centralized compute budgets. The cost differential is striking: three orders of magnitude ($600 vs.$100,000) for comparable output.

Reusability and the Formalpedia Vision

By making every theorem individually importable and immutable, Prove2Me positions itself as an application-layer complement to curated foundational libraries (Mathlib, CSLib, PhysLib), with the hope that accumulated results will eventually be contributed back.

The Human Role

The authors emphasize: "Prove2Me's vision is not to replace mathematicians." Choosing what to formalize, decomposing into milestones, and judging faithfulness remain human judgments. Agents supply mechanical labor and must write detailed natural-language accounts to keep content legible to humans.

Conclusion

Prove2Me demonstrates a viable path to internet-scale mathematical collaboration involving both humans and AI agents, with correctness machine-checked by the Lean kernel. Key takeaways:

1. Low barrier to entry: Anyone with an AI agent can contribute, regardless of Lean or mathematical expertise
2. Bounded auditing: Human review confined to curated mission cores
3. Atomized collaboration: Proof-sketches enable clean partitioning of effort
4. Organic library growth: Completed proofs become citable building blocks; unsolved sub-problems surface as new challenges

Future Research Directions

• Search in a large evolving corpus: How agents should locate existing theorems in Formalpedia
• Decentralized continual learning: How asynchronous agents exchange harnesses, lessons, and context
• Adversarial robustness: Rejecting low-quality or malicious submissions (e.g., via reputation systems)
• Human-legible insight extraction: Deriving mathematical understanding from machine-generated proofs

Invitation

Prove2Me is early-stage and iterating quickly. The authors invite contributions—whether formalizing one's own project with community support or contributing agents' idle tokens—via the community Slack channel or shuze.chen@columbia.edu.