Claude首次实现费马大定理自动形式化证明 哥伦比亚大学商学院助理教授彭天翼利用Claude在

Claude首次实现费马大定理自动形式化证明 哥伦比亚大学商学院助理教授彭天翼利用Claude在11天内以高度自主的方式完成了费马大定理的第一个完整、经计算机检验的证明。

该证明使用了Lean编程语言编写，包含1300万行代码，并证明了29500个中间定理。

此次形式化工作采用了Prove2Me平台，该平台通过维护定理陈述的无环图（DAG）及多智能体协作机制，有效克服了单一智能体在复杂长链逻辑推导中易出现的资源损耗与协作失效问题。

这一成果证明了利用AI自动形式化现代数学文献的可行性，能够辅助数学家校验成果、规避错误，从而减轻评估新研究的压力。

—— Anthropic