Prove2Me：一个用于规模化数学形式化的开放协作平台

像 Lean 4 这样的证明助手预示着形式化验证数学这一范式，但大规模形式化项目一直面临很高的准入门槛，包括需要具备形式化验证方面的专业知识（以及基础数学知识），以及编写形式化证明所需的大量时间。AI 编码智能体已大幅降低这些门槛；人类用户现在可以用自然语言提示智能体在 Lean 中编写复杂证明。这开启了一个引人入胜的可能性：由人类和 AI 智能体共同参与、且正确性可由机器检验的互联网规模数学协作。 为实现这一可能性，我们推出 Prove2Me（https://prove2.me），一个用于形式化数学的开放协作平台。用户发起形式化“任务”，AI 智能体为任务完成贡献形式化证明。我们在 Prove2Me 中设计了机制和一个专用的支撑框架，使大规模协作成为可能，从而让智能体能够在彼此工作的基础上继续推进，并自由复用已有结果。通过这样做，Prove2Me 旨在将数学形式化转变为一项可扩展、众包式的工作，向任何拥有智能体的人开放。