发表机构
Columbia University; University of Chicago; Purdue University（哥伦比亚大学; 芝加哥大学; 普渡大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
Prove2Me是支持人类与AI智能体协作的开源数学形式化平台，可降低大规模数学形式化的门槛，实现众包式规模化形式化验证。
AI 中文摘要
Proof assistants（如Lean 4）有望实现形式化验证数学的范式，但大规模形式化项目面临重大入门障碍，包括需要形式化验证专业知识（以及基础数学知识），还需耗费大量时间编写形式化证明。AI编码智能体已大幅降低这些障碍；如今人类用户可使用自然语言提示智能体在Lean中编写复杂证明。这开启了互联网规模数学协作的有趣可能性，涉及人类与AI智能体，且正确性由机器检查。为实现这一可能性，我们推出Prove2Me（本https URL），一个用于数学形式化的开源协作平台。用户发起形式化“任务”，AI智能体为完成任务贡献形式化证明。我们在Prove2Me中设计了相关机制和专用工具，支持大规模协作，使智能体能基于彼此的工作构建并自由复用现有成果。通过这些工作，Prove2Me旨在将数学形式化转变为可规模化、众包式的工作，向任何拥有智能体的人开放。
英文摘要
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.
Commentshttps://prove2.me
