让任何人用AI协作完成数学证明的形式化，实现可验证的开源数学工程。
Prove2Me: An Open Collaborative Platform for Scaling Math Formalization
- 构建开放平台，支持人类与AI协同进行数学形式化。
- 通过可复用证明和任务机制，实现大规模协作式证明生成。
- 适合数学研究者、形式化爱好者及AI编程实验者参与。
Lean 4等证明助手承诺实现数学的正式验证范式，但大规模形式化项目面临高门槛：既需形式化验证与数学专业知识，又耗费大量时间撰写形式化证明。人工智能编码代理显著降低了这些门槛，用户可用自然语言指令让代理生成复杂的Lean证明。这开启了互联网规模的数学协作可能——人类与AI共同参与，且结果可机器检查。为此，我们提出Prove2Me（https://prove2.me），一个开放的数学形式化协作平台。用户发起形式化“任务”，AI代理协作完成形式化证明。我们设计了机制与专用工具链，使代理能基于彼此工作成果继续推进，并自由复用已有定理。目标是将数学形式化转化为可扩展的众包工程，对任何拥有代理的用户开放。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。