Prove2Me：扩展数学形式化规模的开放协作平台

Lean 4 等证明助手承诺提供形式化验证数学的范例，但大规模形式化项目面临着重大的进入障碍，包括需要形式化验证（以及基础数学）方面的专业知识以及编写形式化证明所需的大量时间。人工智能编码代理极大地减少了这些障碍；人类用户现在可以使用自然语言来提示代理在精益中编写复杂的证明。这开启了涉及人类和人工智能代理的互联网规模数学协作的有趣可能性，其中正确性是由机器检查的。为了实现这种可能性，我们引入了 Prove2Me (https://prove2.me)，一个用于形式化数学的开放协作平台。用户启动形式化“任务”，人工智能代理为完成任务提供形式化证明。我们在 Prove2Me 中设计了机制和专门的工具，可以实现大规模协作，以便代理可以在彼此的工作基础上构建并自由地重用现有结果。 Prove2Me 的目标是将数学形式化转变为可扩展的、众包的工作，向任何拥有代理的人开放。