AI时代，证明只需一页纸，人类何需苦战？
天才数学家陶哲轩，以他的卓越才华和敏锐洞察力，再次引领了数学界的潮流。这次，他将人工智能（AI）引入了数学证明领域，将人类对数学的探索推向了一个新的高度。
陶哲轩的这次视频博主之旅，可谓是一鸣惊人。他选取了一个泛代数的命题，即证明Magma方程E1689蕴含E2。即使是方程理论项目的合作者Bruno Le Floch，也足足人工花了一页纸才完成证明。然而，借助AI，整个证明过程仅用时33分钟。
AI在此过程中的角色，可谓神奇。陶哲轩将草稿拆分为微小逻辑单元，交由GitHub Copilot生成代码骨架，再以Lean的canonical策略匹配填补细节。过程中也涉及部分手动补全，最终，整个形式化证明能够在Lean中通过验证。
这样的操作不仅大大缩短了时间，更重要的是满足了“人类可读性”。Bruno Le Floch最初挑战该问题时，曾在论文中宣称E1689-E2的所有已知证明都依赖计算机辅助。然而，经过AI的助力，研究者成功地将证明转化为一个人类可读的证明。这无疑为AI在数学领域的角色提供了新的解读。
陶哲轩此次尝试并非一次成功即止。据他在视频中透露，前两次的证明过程都出现了一些“bug”。第一次拿到的代码才到第5行他就有点看不懂了，所以选择了重开；第二次虽然完成了所有证明（用时48分钟），但由于是新人博主不太熟悉录屏设备，导致屏幕分享失败，因此又只能重来。但他并未因此气馁，而是以积极的态度面对挑战，继续探索AI在数学证明中的应用。
与此同时，陶哲轩开发的数学证明助手也迎来了2.0版本升级。这个轻量级证明助手的功能远逊于Lean、Isabelle或Rocq等完整证明助手，但希望它能够轻松用于证明一些简短而繁琐的任务。这个工具的两个具体目标是：为渐近分析提供支持，以及根据反馈进行灵活的扩展。目前这个助手有两种模式：假设模式和策略模式。其中策略模式作为默认模式，有点类似于Lean、Isabelle或Rocq里面那样式儿的策略模式。
陶哲轩对这个证明助手的改进感到非常满意，并愿意接受进一步的建议或贡献新的功能。他表示这个工具足够灵活，可以为解决一些看似棘手的问题提供帮助。他还计划引入新的数据类型、公例和策略，或者贡献一些有难度的例子。此外，他还计划开发用于估算符号函数的函数空间规范的工具。
天才数学家陶哲轩的这次尝试，让我们看到了AI在数学领域的无限可能。他以自己的实际行动证明了AI在数学证明中的强大作用，将人类对数学的探索推向了一个新的高度。在这个AI时代，我们看到了证明只需一页纸的可能，也看到了人类在数学领域探索的新方向。
总的来说，陶哲轩的这次尝试给我们提供了一个全新的视角来看待AI与数学的关系。我们期待在未来的日子里，会有更多的数学家和科学家投身于此，共同探索AI在数学领域的无限可能。在这个过程中，我们也将更深入地理解数学的本质，以及它在人类文明中的重要地位。
