Prove2Me平台让AI代理协作完成数学形式化证明，降低专业门槛，任何人都能参与。
Prove2Me是一个开放协作平台，旨在解决大规模数学形式化项目的入门障碍。该平台允许用户发起形式化"任务"，AI代理可贡献形式化证明以完成任务。平台设计了专门机制和工具，支持大规模协作，使代理能够相互构建工作并自由复用现有成果。
Prove2Me: An Open Collaborative Platform for Scaling Math Formalization
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.