2026年3月,Math公司开发的AI Agent Gauss在一周内独立完成了菲尔兹奖级数学成果的形式化验证,涉及Maryna Viazovska在8维和24维最优球体堆积问题上的研究。这一成果原需6个月完成,现生成20万行Lean代码,成为历史上最大规模的单一目的形式化项目。Gauss还检测并修正了原论文中的细节错误,展示了AI加速数学研究的能力。团队认为,自动形式化将彻底变革数学知识体系。目前代码已公开发布。
原文链接
本文链接:https://kx.umi6.com/article/33380.html
转载请注明文章出处
相关推荐
换一换
王的猜想,刚刚扩展到四维
2026-10-11 15:44:39
陶哲轩12年前的预言,现在AI帮他兑现了
2026-06-20 20:21:47
新晋菲尔兹奖得主,当天宣布加入OpenAI
2026-07-24 10:29:19
字节Seed发布最强数学模型:一招“打草稿”,IMO银牌变金牌
2025-12-25 14:40:05
数学专业,危!菲尔兹奖得主亲测ChatGPT 5.5 Pro,17分钟出论文级成果
2026-05-11 14:09:39
数学家24小时驳回OpenAI攻破的猜想!“AI证对了每句话,但已跟原猜想无关”
2026-08-04 18:08:29
形式化证明与大模型:共创可验证的AI数学未来|量子位直播
2025-05-27 12:29:36
姚班校友主导,Claude攻克费马大定理首个完整形式化证明
2026-09-05 10:04:54
陶哲轩、邓煜均在列!25位菲尔兹奖得主联合警告AI正毁掉数学
2026-09-12 13:08:57
菲尔兹奖得主都看懵了:OpenAI非数学模型首次自主突破80年未解数学难题
2026-05-21 17:54:30
啥?陶哲轩18个月没搞定的数学挑战,被这个“AI高斯”三周完成了
2025-09-14 13:38:51
菲尔兹奖得主都未能破解的数学难题 被两名高中生用AI攻破了
2026-09-14 08:33:03
7天几百元开一家店!用千问办公电商版,立省启动资金5万元
2026-10-15 10:33:35
787 文章
1049485 浏览
24小时热文
更多
-
2026-10-20 14:16:11 -
2026-10-20 13:15:46 -
2026-10-20 13:12:18