⌘ K
… 读取采集状态 同步中...
雷
原文
新智元· 新智元·· 14 天前精选AI 评分88

北大团队完成庞加莱猜想Lean 4形式化并发布双检验版本

北大团队官宣:庞加莱猜想被完整形式化!首个双检验版本来了

AI 导读

北京大学AI for Math团队宣布在Lean 4中完成庞加莱猜想的完整形式化,这是首个同时通过Lean build与Comparator检验的版本。团队在半月内生成约320万行代码,总成本低于3万美元,其中最大的里程碑M76包含约65万行代码,旨在连接拓扑流形与光滑流形。北大项目还通过双重检验机制验证了证明的正确性,并修复了Morgan和田刚专著中关于颈拓扑的一处印刷错误。

推荐理由

北大团队以约3万美元和半月时间完成庞加莱猜想的Lean 4形式化,展示了AI智能体在基础数学验证中的成本优势与工程化路径。

本文当前提供导读和图片预览,完整图文请查看原文。

来源:新智元 · mp.weixin.qq.com