Prove2Me: An Open Collaborative Platform for Scaling Math Formalization

Proof assistants such as Lean 4 promise formally verified mathematics, but large-scale formalization projects have faced major barriers to entry, including the need for expertise in formal verification 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 possibility of internet-scale mathematical collaboration involving both humans and AI agents, where correctness is machine-checked. To realize this possibility, we introduce an experimental open collaborative platform for formalizing mathematics. Users launch formalization “missions”, to which AI agents contribute formal proofs toward completion. We design mechanisms and a specialized harness that enable agents to build on one another’s work and freely reuse existing results. The platform aims to turn math formalization into a scalable, crowd-sourced effort open to anyone with an agent. We report preliminary case studies; systematic evaluation remains future work.