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

主要观点总结

文章介绍了菲尔兹奖得主陶哲轩发起的一项名为方程理论的项目，该项目结合了专业与业余数学家、自动定理证明器、AI工具以及证明辅助语言Lean，共同描述与4694条幺半群方程定理相关的蕴含图。项目进度已完成99.9963%，仍有部分蕴含关系需要解决。陶哲轩分享了项目的最新进展，包括可视化工具的使用、方程定理的表格展示以及机器在其中的辅助作用等。项目通过GitHub平台进行协调，遵循标准的GitHub实践。

关键观点总结

关键观点1: 陶哲轩发起方程理论项目，利用人工智能等解决蕴含关系问题。

陶哲轩结合了专业与业余数学家、自动定理证明器、AI工具以及证明辅助语言Lean来解决与幺半群方程定理相关的蕴含图问题。项目进度已经接近完成，大部分蕴含关系已经得到证明。

关键观点2: 项目进度更新和项目成果展示。

陶哲轩分享了项目的最新进展，包括项目进度已经完成的百分比、已经解决的蕴含关系数量以及正在研究的方程定理的表格等信息。他还提到了可视化工具的使用，使得检查蕴含图的各个部分变得更加方便。

关键观点3: 人工智能在项目中的辅助作用。

虽然人工智能在项目中以一种辅助、次要的方式被使用，例如通过GitHub Copilot等工具来加速编写Lean证明等，但在解决剩余的、更困难的蕴含关系时，现代AI可能会发挥更重要的作用。

文章预览

 Datawhale分享  最新：陶哲轩，编辑：新智元 AI，已成为菲尔兹奖得主最得心应手的工具。 大约三周前，陶哲轩提出了一个协作项目—— 结合专业和业余数学家、自动定理证明器、AI工具，以及证明辅助语言Lean，来描述与4694条幺半群（magmas）方程定理定理相关的蕴含图。 这些定理最多可以使用，四次幺半群运算来表达。 也就是说，需要确定4694条定理之间可能存在4694 * (4694 - 1) = 22028942蕴含的关系真伪。 地址：https://github.com/teorth/equational_theories/blob/main/data/equations.txt 这一项目在9月25日发布当天便启动了，如今，已经紧锣密鼓进行了19天。 刚刚，陶哲轩公布了项目的最新进展： 从已解决原始蕴含关系角度来看，截至目前，项目进度已完成99.9963%。 在需要解决的22028942个蕴含关系中，8178279个被证明为真，13854531个被证明为假，只有826个仍未解决。 而 ………………………………