新智元报道
：桃子 好困
【新智元导读】 AI已完全融入数学家的工作流中。陶哲轩刚刚宣布，最新方程理论项目已完成99.9963%，众包之力外加AI辅助取得了重大成绩。他认为，剩余大约700个让人类头疼的难题，AI或许更有潜力。
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.99%
在集合中，有249个蕴含关系推测为假，并且很快就证明了是假的。
出于编译效率的考量，他们并没有在Lean中记录每一个证明，只在其中证明了一个较小的592790个蕴含关系集合，然后通过传递性推导出更广泛的蕴含关系集合。
例如，利用如果方程X蕴含方程Y，方程Y蕴含方程Z，那么方程X蕴含方程Z的事实。
他们还很快利用蕴含图对偶对称性，对其进一步简化。
经过项目志愿者的不懈努力，陶哲轩称现在有了很多出色的可视化工具（尚未完成的），来检查蕴含图的各个部分。
比如，如下这张图描述了方程1491：x = (y ◇ x) ◇ (y ◇ (y ◇ x ))的所有结果。
陶哲轩将其称之为「Obelix law」。它还有一个伙伴Asterix law，即方程65：x = y ◇ (x ◇ (y ◇ x ))。
如下是，他们正在研究的所有方程定理的表格，以及它们蕴含/被蕴含定理数量。
地址：https://teorth.github.io/equational_theories/implications/
这些界面也在某种程度上与Lean集成。
比如，我们可以点击查看Obelix law蕴含方程359，陶哲轩将其作为题目，让大家进行挑战。他暗示，在Lean中仅用4行就可以完成证明。
在过去的几周里，他还了解到这些定理中，有许多之前已经出现在文献中。
由此，这里编制了这些方程的「导览」。
地址：https://github.com/teorth/equational_theories/wiki/Tour-of-selected-equations
例如，除了众所周知的交换律（方程43）、结合律（方程4512）之外，一些方程（方程14、方程29、方程381、方程3722、方程3744）曾出现在一些Putnam数学竞赛中；
而方程1571则对指数为二的阿贝尔群（abelian groups）进行了分类。
根据Birkhoff完备性定理，如果一个方程定理蕴含另一个，那么它可以通过有限次重写操作来证明。
不过，所需的重写次数可能相当长。
上面提到的1491蕴含359的证明已经相当具有挑战性，需要四到五次重写。
另外，方程1689蕴含方程2的证明，更是极其冗长。尽管如此，标准的自动定理证明器，如Vampire，完全有能力证明绝大多数这些蕴含关系。
更微妙的是反蕴含关系，在这种情况下必须证明定理X不蕴含定理Y。原则上，只需要展示一个遵循X但不遵循Y的幺半群即可。
在很大一部分情况下，他们可以简单地搜索小型有限幺半群——比如两个、三个或四个元素的幺半群——来获得这种反蕴含关系。
但这些并不足够，事实上，他们只知道有些反蕴含关系，只能通过构造无限幺半群来证明。
比如，现在已知的Asterix law不蕴含Obelix law，但所有反例必然是无限的。
有趣的是，已知的构造方法与集合论中著名的forcing技术有一些相似之处，即不断向（部分）幺半群添加「通用」元素，以forcing存在具有某些特定属性的反例。
不过，这里的构造肯定比集合论构造简单得多。
他们还从「线性」幺半群x ◇ y = ax + by构造中取得了有益的进展。这些构造存在于交换环和非交换环中。
与「汇聚」（confluent）方程定理相关的自由幺半群，以及更普遍的具有完整重写系统的定理。
因此，未解决的蕴含关系数量继续稳步减少。
遵循标准GitHub实践，论文很快上线
经过相当繁忙的后端设置和「灭火」（putting out fires）工作后，项目现在运行得相当顺利。
项目在Lean Zulip频道上协调，所有贡献都通过GitHub上的拉取请求（pull request）过程进行，并通过基于问题的GitHub项目进行跟踪。
另外两位维护者Pietro Monticone、Shreyas Srinivas为其提供了宝贵的监督。
与之前的PFR形式化项目相比，这次项目的工作流程遵循了标准的GitHub实践，大致如下：
如果在Zulip讨论过程中，明确需要完成某些特定任务以推进项目（比如，在Lean中形式化讨论线程中已经推导出的蕴含关系证明），就会创建一个「问题」（通常由陶哲轩自己或其他维护者创建），其他贡献者可以「认领」这个问题，单独工作（使用主GitHub仓库的本地副本）。
然后提交「拉取请求」将他们的贡献合并回主仓库。这个请求随后可以由维护者和其他贡献者审查，如果获得批准，就会关闭相关问题。
更广泛地说，他们正努力记录这个设置中的所有过程和经验教训。
这将成为即将发表的关于这个项目的论文的一部分，现正处于初步规划阶段，可能会包括数十位。
陶哲轩表示，自己对项目取得的进展非常满意，而且许多最初的期望已经实现。
在科学方面，他们发现了一些新的技术和构造，用来证明一个给定的方程理论不蕴含另一个；他们还发现了一些具有有趣特征的奇特代数结构，如Asterix和Obelix对，是通过系统性搜索方式被发现的。
参与者方面，非常多样化，从各个职业阶段的数学家、计算机科学家，到感兴趣的学生和业余爱好者。
此外，Lean平台在整合人工生成和机器生成的贡献方面表现良好。
在讨论线程中，他们还进行了许多非正式的数学论证，但这些论证往往会迅速在Lean中形式化，消除了关于正确性的争议就。
进而，研究人员可以转而专注于如何最好地部署各种经过验证的技术，来解决剩余的蕴含关系。
AI并未做出重大贡献
原本，陶哲轩期待看到现代AI工具，能够在项目中做出重大贡献。
但实际上，它们以一种辅助、次要的方式被使用。
比如，通过GitHub Copilot等工具来加速编写Lean证明、LaTeX文档框架、其他软件代码。
此外，他们的几个可视化工具，也主要是使用Claude等大模型共同编写的。
然而，对于解决蕴含关系这一核心任务，更「传统」的自动定理证明器表现更好。
不过，目前剩余的大约700个蕴含关系，大多数不适合使用传统工具来处理。
有几个蕴含关系（特别是涉及Asterix和Obelix那些），已经让人类专家困惑多日。
陶哲轩认为，在解决剩余的、更困难的蕴含关系时，现代AI可能会发挥更重要的作用。
参考资料：
https://terrytao.wordpress.com/2024/10/12/the-equational-theories-project-a-brief-tour/
陶哲轩论文漏洞竟被AI发现，26年预言要成真！看定理名猜出研究方向，大神直呼AI能力惊人
数学界的传奇人物陶哲轩最近在使用AI工具时，竟然被Lean4和Copilot揭示出自己论文中的一项错误，这似乎预示着他26年前的预言——AI将成为数学论文合著者，正在逐步变为现实。 借助AI的力量，陶哲轩在论文的验证过程中发现了不易察觉的bug，尽管这只是个小问题，但显示出AI在辅助数学研究中的惊人能力。 陶哲轩发现，AI不仅能在形式化证明过程中捕捉到细微错误，还能预测研究方向。 比如在撰写关于麦克劳林不等式论文时，Copilot不仅能协助编写代码，还能根据定理名称推测研究路径。 这一系列事件让数学爱好者惊叹，AI在辅助证明和研究选择上展现出前所未有的效率。 陶哲轩已经开始在论文中大量使用AI工具，如GPT-4和Copilot，虽然 Lean4在处理复杂表达式上尚有局限，但其自动重写策略显著提高了效率。 随着LLM技术的发展，陶哲轩期待能通过自然语言指令让AI执行更复杂的数学转换，进一步提升研究的便利性。 数学界的大师对AI工具的依赖日益加深，这引发了网友们的讨论，有人认为LLM对所有层次的用户都有积极影响，但也有人担忧这可能加剧技能差距。 然而，随着像陶哲轩这样的专家在LLM的帮助下加速工作，未来的数学研究无疑将更加依赖于AI的力量。
陶哲轩又来安利AI工具了：新论文排版用上VSCode Copilot+插件
知名数学家陶哲轩在社交平台上分享了他的最新论文排版工具推荐——VSCode Copilot+插件。 这是他继推广GPT-4的代码功能后，再次为AI工具打call。 陶哲轩表示，他每5-10年会更换一次工具，以适应技术发展。 他曾经用过Word，主要是因其VB脚本功能，但因Word对LaTeX兼容性差，他很快就放弃了。 现在的选择是VSCode，得益于其自定义代码片段功能和AI辅助工具Copilot。 VSCode的效率远超Word，比如通过定义指令“cor”，只需按Tab键，即可进入预设的“推论”环境。 Copilot则能根据用户输入提供代码建议，进一步提升编写效率。 网友们也分享了各自使用的排版工具，工具选择因人而异。 对于想要提升论文排版效率的朋友，陶哲轩推荐的组合包括TeX Live和LaTeX Workshop，LaTeX Workshop在VSCode应用商店就能找到。 安装过程中，虽然配置有一定难度，但有大神分享的脚本代码可以简化。 配置完成后，VSCode将具备LaTeX支持，配合vim使用，对于包含公式和代码的文档尤其高效。 至于陶哲轩即将发布的新论文内容，虽然他没有透露具体细节，但从截图中可以猜测其部分科学和技术性质。 对于对论文排版有困扰的读者，尝试一下这些工具或许能带来惊喜。 如果你对陶哲轩的分享感兴趣，可以关注他的动态，一起探索科技带来的学术新体验。
加州理工华人用AI颠覆数学证明！提速5倍震惊陶哲轩，80%数学步骤全自动化
加州理工学院的华人团队通过AI工具Lean Copilot实现了数学证明的重大突破，将证明步骤的自动化率提升到惊人的80%，这一进步相当于加速了陶哲轩等数学家的研究速度，使其能够原地加速5倍。 这一工具的核心在于解决了一个在Lean中运行LLM推理的bug，使得机器学习模型能够与Lean无缝协作，实现自动化的定理证明过程。 团队在开源许可下发布了这一成果，贡献者宋沛洋，UCSB荣誉CS本科生和加州理工CMS系的SURF研究员，他的工作使得Copilot不仅能够提出证明策略，还能完成中间证明目标和选择相关前提，显著提升了数学证明的效率。 例如，Lean Copilot的suggest_tropics工具能够生成策略建议，通过结合基于规则的证明搜索工具aesop，进行更深入的证明搜索，寻找最优路径。 研究人员通过实验验证，证明搜索工具能够自动化81.2%的证明步骤，比策略建议和基于规则的aesop工具表现出更高的效率。 这一工具的本地LLM推理能力，以及对快速反馈和低计算需求的满足，使得它在各种硬件环境中都能高效运行，为数学家们提供了强大的助手。 华人宋沛洋在项目中发挥了关键作用，他不仅参与了LeanDojo平台的开发，还在加州理工学院的CMS系进行研究，探索机器学习与数学证明的结合。 团队的其他成员如Anima Anandkumar教授和Kaiyu Yang博士，也在神经符号人工智能领域做出了重要贡献。
