陶哲轩用AI证明方程理论,19天进度99.99%!论文即将上线

AIGC动态2个月前发布 AIera
369 0 0
陶哲轩用AI证明方程理论,19天进度99.99%!论文即将上线

 

文章摘要


【关 键 词】 方程理论数学进展自动证明AI辅助众包研究

陶哲轩领导的方程理论项目取得了显著进展,目前完成度已达99.9963%。该项目汇集了专业和业余数学家、自动定理证明器、AI工具以及证明辅助语言Lean,旨在描述4694条幺半群方程定理间的蕴含关系。项目自9月25日启动以来,已成功证明8178279个蕴含关系为真,13854531个为假,仅剩826个未解决。陶哲轩通过个人日志记录了项目每天的进展。

项目团队利用众包方式,结合编译效率和传递性,推导出广泛的蕴含关系集合。他们还利用蕴含图的对偶对称性进行简化,并开发了可视化工具来检查蕴含图的各个部分。例如,方程1491和65分别被称为”Obelix law”和”Asterix law”,这些方程及其蕴含关系正在被研究和可视化。

陶哲轩还编制了一份”导览”,介绍了这些方程在文献中的历史和应用,包括一些曾出现在Putnam数学竞赛中的方程和定义了”中心幺半群”的方程168。根据Birkhoff完备性定理,如果一个方程定理蕴含另一个,那么它可以通过有限次重写操作来证明,但所需的重写次数可能相当长。

在反蕴含关系的证明中,他们通过搜索小型有限幺半群来获得反例,但有些反蕴含关系需要构造无限幺半群来证明。这些构造方法与集合论中的forcing技术有相似之处。

项目遵循标准的GitHub实践,通过拉取请求和问题跟踪来协调贡献。陶哲轩对项目取得的进展非常满意,认为许多最初的期望已经实现。他们发现了新的技术和构造,用来证明一个给定的方程理论不蕴含另一个,并通过系统性搜索发现了一些具有有趣特征的奇特代数结构。

尽管陶哲轩原本期待现代AI工具能在项目中做出重大贡献,但实际上它们以辅助、次要的方式被使用。对于解决蕴含关系这一核心任务,更传统的自动定理证明器表现更好。然而,对于剩余的大约700个不适合使用传统工具处理的蕴含关系,陶哲轩认为现代AI可能会发挥更重要的作用。

“极客训练营”

原文和模型


【原文链接】 阅读原文 [ 2223字 | 9分钟 ]
【原文作者】 新智元
【摘要模型】 moonshot-v1-32k
【摘要评分】 ★★★★★

© 版权声明
“绘蛙”

相关文章

暂无评论

暂无评论...