Prove2Me: An Open Collaborative Platform for Scaling Math Formalization
Artificial IntelligenceLogic in Computer ScienceMultiagent Systems
Summary
The authors present Prove2Me, a new online platform that lets people and AI work together to create formal mathematical proofs using the Lean 4 proof assistant. Normally, writing formal proofs is hard and takes a lot of time, but AI coding agents can now help by turning natural language instructions into proofs. Prove2Me allows many users and AI agents to collaborate by sharing and building on each other's work, making formal math more accessible and faster to develop. Their system aims to make large-scale math formalization a team effort open to everyone.
Authors
Shuze Chen, Kunal Marwaha, Xiaoyang Lu, Henry Yuen, Tianyi Peng
Abstract
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.