黑海洋 黑海洋 WIKI

Claude首次实现费马大定理自动形式化证明

资讯 · 约 1 分钟 · 黑海洋 · 1.3万

哥伦比亚大学商学院助理教授彭天翼利用Claude在11天内以高度自主的方式完成了费马大定理的第一个完整、经计算机检验的证明。该证明使用了Lean编程语言编写,包含1300万行代码,并证明了29500个中间定理。此次形式化工作采用了Prove2Me平台,该平台通过维护定理陈述的无环图(DAG)及多智能体协作机制,有效克服了单一智能体在复杂长链逻辑推导中易出现的资源损耗与协作失效问题。这一成果证明了利用AI自动形式化现代数学文献的可行性,能够辅助数学家校验成果、规避错误,从而减轻评估新研究的压力。

—— Anthropic

相关文档

评论与补充0

有问题或想补充的,写在下面 · 选中正文文字再点「报告错误」会自动引用

还没有评论。有疑问、补充,或者发现错字,都可以写在下面。

就事论事,别发广告 · 正常评论