# Prove2Me: An Open Collaborative Platform for Scaling Math Formalization

arXiv: https://arxiv.org/abs/2608.28433 · HTML: https://mlsanity.com/paper/2608.28433/

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Builds on 21 of its 33 references that are in the map.
- First posted on arXiv 28 Aug 2026.

## Builds on (most cited first, 21 of 21)

- [CAMEL: Communicative Agents for "Mind" Exploration of Large Language Model Society](https://mlsanity.com/paper/2303.17760/) (2023)
- [ChatDev: Communicative Agents for Software Development](https://mlsanity.com/paper/2307.07924/) (2023)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean](https://mlsanity.com/paper/2404.12534/) (2024)
- [Aristotle: IMO-level Automated Theorem Proving](https://mlsanity.com/paper/2510.01346/) (2025)
- [130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone?](https://mlsanity.com/paper/2601.03298/) (2026)
- [M2F: Automated Formalization of Mathematical Literature at Scale](https://mlsanity.com/paper/2602.17016/) (2026)
- [MerLean: An Agentic Framework for Autoformalization in Quantum Computation](https://mlsanity.com/paper/2602.16554/) (2026)
- [Formalizing Mathematics at Scale](https://mlsanity.com/paper/2605.29955/) (2026)
- [Decentralized Multi-Agent Systems with Shared Context](https://mlsanity.com/paper/2606.10662/) (2026)
- [Automatic Textbook Formalization](https://mlsanity.com/paper/2604.03071/) (2026)
- [EconCSLib: AI-Assisted Lean Formalization for Economics & Computation research](https://mlsanity.com/paper/2606.13306/) (2026)
- [CSLib: The Lean Computer Science Library](https://mlsanity.com/paper/2602.04846/) (2026)
- [FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean](https://mlsanity.com/paper/2604.23002/) (2026)
- [Risk-Controlled Lean-as-Judge for Natural-Language Mathematical Reasoning](https://mlsanity.com/paper/2605.28365/) (2026)
- [EconCSLib: A Lean Library for Computational Economics and AI-Assisted Research](https://mlsanity.com/paper/2606.16144/) (2026)

## Built on by (most cited first, 5 of 5)

- [Choir: An Open Protocol for Distributed Multi-Agent Autoformalization](https://mlsanity.com/paper/2609.31903/) (2026)
- [AIProver: Agentic Auto-Formalization of Mathematical Research via Certificate-Driven Evolving Harness](https://mlsanity.com/paper/2610.05367/) (2026)
- [An AI-Assisted Formalization of the Poincar'e Conjecture](https://mlsanity.com/paper/2610.08329/) (2026)
- [The Future of AI-assisted Physics: Discovering, Verifying and Organizing Results via Formalization](https://mlsanity.com/paper/2610.14059/) (2026)
- [PANINI-DR: Controlled Deep Research through Generative Semantic Workspaces](https://mlsanity.com/paper/2610.15208/) (2026)

## Abstract (arXiv)

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.