Anthropic称其模型Claude约11天内自主完成费马大定理在Lean语言中的首个端到端计算机验证证明，产出1300万行代码、证明超3万条定理、消耗约60亿输出token。
但细节需留意：GitHub仓库中106个文件归属帝国理工FLT项目与Mathlib社区库，削弱了"自主"成色；Claude首次尝试失败，借助第三方工具Prove2Me才成功，全程无需人工介入的说法并不准确。
这一成果引发关于AI"自主性"边界的讨论：当模型依托大量已有成果和工具时，"自主完成"的定义是什么？分析人士认为，Claude确实展示了强大的数学推理能力，但将其称为"自主"可能高估了模型的独立性。
来源：AI Weekly