Source-linked AI summary
Prove2Me: An Open Collaborative Platform for Scaling Math Formalization
Shuze Chen, Kunal Marwaha, Xiaoyang Lu, Henry Yuen, Tianyi Peng
TL;DR
Large-scale formalization is limited by the time and expertise required to produce and audit machine-checked mathematics. Prove2Me introduces an open platform where AI agents collaborate through missions, reusable theorem objects, and proof-sketches. The paper reports project-scale Lean developments, while noting that its case studies cannot separate model-generation effects from harness effects and that open platform governance remains unresolved.
Problem
Large formalization projects require substantial time and specialized mathematical and proof-assistant expertise, while auditing, reuse, and scalable collaboration remain difficult.
Method
Prove2Me separates immutable theorem statements from proofs and organizes agent collaboration through audited missions, proof-sketches, and reusable results.
Results
Prove2Me supports project-scale Lean developments, including a largest mission comparable to a centralized swarm in size and a smallest mission producing 17K lines in a week.
Takeaways & Limitations
The platform provides an open collaborative framework in which agents can partition proof work, reuse results, and contribute beneath human choices about statements and milestones.
Takeaways & Limitations
The case studies cannot distinguish stronger model generations from the multi-agent harness, and open submission raises unresolved quality, trust, and human-legibility challenges.
Abstract
from arXiv · showhide
Proof assistants such as Lean 4 promise the paradigm of formally verified mathematics, but large-scale formalization projects have faced major barriers to entry, including the need for expertise in formal verification (as well as the underlying mathematics) and the significant time required for writing formal proofs. AI coding agents have dramatically reduced these barriers; human users can now use natural language to prompt agents to write complex proofs in Lean. This opens up the intriguing possibility of internet-scale mathematical collaboration involving both humans and AI agents, where correctness is machine-checked. To realize this possibility, we introduce Prove2Me (https://prove2.me), an open collaborative platform for formalizing mathematics. Users launch formalization "missions", to which AI agents contribute formal proofs toward completion. We designed mechanisms and a specialized harness in Prove2Me that enable large-scale collaboration so that agents can build on one another's work and freely reuse existing results. In doing so, Prove2Me aims to turn math formalization into a scalable, crowd-sourced effort open to anyone with an agent.
1 Introduction
Large-scale mathematical formalization has been constrained by the time and specialized expertise required for machine-checked proofs. Prove2Me responds by combining AI-agent participation with audited, decomposed, reusable collaboration.
- Motivation: Formalizing major mathematical corpora has required sustained community effort and simultaneous expertise in mathematics and proof-assistant engineering.The Liquid Tensor Experiment took roughly eighteen months, while Fermat’s Last Theorem formalization is funded for five years.
- Motivation: AI theorem proving and agent-based formalization are advancing across research papers, textbooks, and foundational mathematics.These developments suggest that multiple agents may reduce tasks previously requiring months or years, although the supplied passage is truncated before stating the full claim.
- Challenges: Existing efforts face scalable auditing, reusability, and collaboration obstacles as AI-generated theorem collections grow.Human expertise is still needed to assess semantic faithfulness, tightly interdependent repositories hinder isolated reuse, and large swarms create coordination challenges.
- Prove2Me: Prove2Me lowers entry barriers, limits human auditing to curated mission cores, decomposes proofs into atomized tasks, and grows a reusable library.Completed proofs become citable building blocks while unsolved sub-problems surface as new challenges.
- Prove2Me: The platform’s vision is crowd-sourced formalization in which AI agents contribute to large mathematical projects and build on one another’s work.The paper presents missions, type-based verification, proof-sketches, and completed community missions as the main components of this vision.
2 Related work
Recent AI systems increasingly generate Lean proofs and formalize substantial corpora, but monolithic workflows leave auditing, reuse, integration, and compute-scaling bottlenecks. Prove2Me is motivated by these limitations.
- AI for theorem proving: AI theorem provers have progressed from machine-generated library proofs to systems reporting strong miniF2F and IMO-level performance.The related work cites retrieval-augmented provers, the DeepSeek-Prover series, AlphaProof, Aristotle, and workflow-integrated tactic suggestion.
- AI-assisted formalization: AI agents now formalize textbooks, foundational theory, and research papers, including large single-agent and multi-agent developments.Examples span point-set topology, economics, computation, quantum computation, and physics.
- Motivating limitations: These efforts remain limited by auditing, reusability, integration cost, and dependence on centralized compute.The paper identifies these limitations as motivations for Prove2Me.
- Auditing: Lean’s kernel verifies that a proof inhabits a statement, but not that an AI-generated statement faithfully expresses the intended mathematics.Statements may be vacuous, omit hypotheses, or drift semantically; one cited audit found only about 43% of proved statements faithful.
- Reusability and cost: Monolithic repositories make individual results difficult to reuse and serialize integration through merge queues when downstream recompilation is required.The related work also notes that prior swarms rely on one organization’s internal compute.
3 Basic design of Prove2Me
Prove2Me separates immutable theorem statements from independently submitted proofs, verifies submissions in pinned environments, and uses missions to bound human auditing. Its workflow also supports natural-language read-back for statement review.
- Basic design: Each theorem is a standalone immutable object stated once, while multiple agents may submit independent proofs for it.This separation is the foundation for efficient, scalable verification on the platform.
- Submitting a theorem: The running example formalizes a Sensitivity Conjecture lemma about the matrix degree of an undirected graph.The graph has m vertices and a symmetric adjacency matrix with entries in {−1, 0, 1}.
- Submitting a theorem: Theorem cards combine a natural-language DESCRIPTION, imported PREAMBLE, and Lean 4 FORMAL STATEMENT, with optional source and subject TAGS.Statements must terminate in a := by sorry placeholder before proof submission, and accepted results compile in a selected pinned environment.
- Submitting a proof: A proof submission declares solution with exactly the target theorem’s type and contains no sorry or new axioms.The platform compiles it in the target environment and checks type equality, making the proof interchangeable with the target statement as a Lean term.
- Audited missions: Prove2Me accepts theorem statements from anyone but uses audited missions to keep the headline goal and milestone core faithful to the intended mathematics.Human auditing remains necessary because kernel checking does not establish semantic faithfulness; mission proposals are reviewed before publication.
- Audited missions: Independent auditor agents perform read-back by translating Lean declarations and dependent definitions into ordinary mathematics for human review.This step is intended to reduce the expertise required for auditing formalized statements.
- Audited missions: Missions can contain hundreds or thousands of supporting theorems while keeping the audited core bounded.This design lets agents generate supporting content at scale without expanding the human audit surface proportionally.
4 Multi-agent collaboration
Prove2Me scales decentralized formalization by decomposing theorems into immutable, independently solvable sub-problems and aligning them through curated milestones. Its import mechanism supports reusable cross-mission results, while agents can detect and correct one another’s formalizations.
- Motivation: Directly filling shared sorry placeholders fails to scale because recompilation is expensive and the work is difficult to atomize.Centralized Git workflows alleviate some problems but introduce human or orchestrator merge bottlenecks, while tightly interdependent theorems remain difficult to reuse.
- Proof decomposition: Proof-sketches import open or proved theorems, making a target conditional on child statements whose proofs can be submitted separately.This turns a hard theorem into atomized sub-problems and allows agents to work without compiling the parent theorem.
- Proof decomposition: Immutable, self-contained child lemmas compose local proofs into global correctness, allowing parent theorems to auto-resolve as dependencies close.The Sensitivity Conjecture example illustrates recursive decomposition through child lemmas and an assisting matrix lemma.
- Formalpedia: Formalpedia accumulates proved atomized theorems that any later proof-sketch can import across missions, creating a shared library of formalized mathematics.It complements foundational libraries by focusing on application-layer results that are one-off and mutually independent.
- Milestones: Milestones provide authoritative canonical targets that prevent conflicting restatements, supply intermediate footholds, and complete missions when all are proved and connected.The milestone mechanism aligns agent work with source statements and enables the goal theorem to resolve automatically.
- Multi-agent continual learning: Agents can correct one another: a disproof exposed a missing boundary condition in gotsman_linial, and the revised theorem closed the entire branch.This example demonstrates continual correction within decentralized collaboration rather than merely parallel proof generation.
- Multi-agent continual learning: Coordinating decentralized, asynchronous agents remains an open question because most existing multi-agent collaboration studies use centralized orchestrators.The platform’s collaboration dynamics motivate a broader research agenda beyond the mechanisms demonstrated here.
5 Case study
Prove2Me reports completed formalization missions as case studies, illustrating project-scale Lean development across different corpora and working patterns. The evidence is not a controlled comparison, and model generation is confounded with the multi-agent harness.
- Completed missions: Several missions were completed between mid-June and the end of July 2026, including research results and textbooks, while the Sensitivity Conjecture mission reached all four milestones.These are platform case studies spanning the exact matrix completion result, Sipser–Gács–Lautemann, and two textbooks.
- Project scale: 151K vs. 130K lines: the largest Prove2Me mission was comparable in size to the centralized swarm’s development.The Prove2Me mission was closed by 6 agents on two consumer subscriptions, versus 30,000 agent runs on metered API inference for the centralized swarm.
- Project scale: 17K lines in a week: one subscription with four subagents produced the smallest reported mission, formalizing Bertsimas and Tsitsiklis [1997].
- Interpretation: The table reports case studies rather than a controlled experiment, with differing corpora, difficulty, working patterns, model generations, and incomparable cost conventions.
- Limitations: Stronger model generation and the multi-agent harness are confounded in every row, so their separate effects remain unresolved.The paper states that separating them requires holding the model fixed and varying only the harness, which is left for future work.
6 Prove2Me done right
Prove2Me is driven through natural-language instructions to agents, which handle setup, API interaction, and Lean verification workflows. Agents need code-execution access for direct use, while local Lean checking remains optional because the server verifies submissions.
- Access boundary: Webpage chatbots cannot be used directly because they lack the ability to run code for Prove2Me API calls.
- Setup: Agents begin setup by following prove2.me/start.md, selecting an onboarding path based on available shell, git, or HTTP capabilities.
- Setup: The workspace installs the pinned Lean and Mathlib revisions and mirrors the server’s module layout so local and server-side verification agree.
- Usage: Natural-language prompts drive usage, with Table 2 collecting common instructions and agents following SKILL.md to use Prove2Me APIs.
- Usage: Agents can browse missions through API calls such as curl "https://prove2.me/api/v1/missions?limit=20&offset=0".
7 Conclusion and outlook
The paper presents Prove2Me as an open platform where AI agents contribute to audited, decomposed, reusable formalization work while humans retain responsibility for mathematical judgment. It also identifies open problems in theorem search, decentralized coordination, submission quality, and human-readable insight.
- Platform contribution: Prove2Me combines low entry barriers, audited missions, proof-sketch decomposition, and an immutable library of reusable results.
- Human–agent roles: Humans choose what to formalize, decompose projects into milestones, and judge whether formal statements capture intended claims; agents provide mechanical labor and detailed natural-language accounts.
- Open questions: As Formalpedia grows, agents must search a large, evolving corpus to locate suitable theorems for import.
- Open questions: Open submission raises questions about rejecting adversarial content and building community trust beyond mission auditing, potentially through reputation systems.
- Open questions: Extracting human-legible insight from machine-generated proofs remains an open problem because the platform ultimately aims to create value for people.
A Images for multi-agent continual learning
The figures depict collaborative and corrective interactions among agents: agents share progress on one mission, and a disproved theorem prompts a corrected formalization.
- Two agents share their latest progress in a discussion under the exact matrix completion mission.
- An agent learns from a disproved theorem and proposes a corrected formalization of the Gotsman–Linial reduction.