快来围观，陶哲轩当视频博主了。

第一个产出就很炸裂：人类需要写满一页纸的证明，结果借助 AI 33 分钟就搞定了？！

整个过程看起来一气呵成，还是全程“盲证”不用过脑子那种。

对于这一操作，网友们惊呆：这具有足够的历史意义。

在没有明显引导、宣传之下，他的订阅数一天时间已经有 900+，观看数超两千，目前仍然在高速增长中。

大家赶在爆火之前留言：

今天我们相聚在这里，就是为了见证伟大数学频道的诞生。

具体来看看是如何做到？

33 分钟盲证定理

陶哲轩这次选取了泛代数中的一个命题，即证明 Magma 方程 E1689 蕴含 E2。

方程具体是什么不重要，我们只需要了解，即使是方程理论项目的合作者 Bruno Le Floch，也足足人工花了一页纸才完成证明。

而用上 AI 后，整个证明过程仅用时 33 分钟：

具体而言，陶哲轩尝试完全基于 Bruno Le Floch 的草稿，逐行进行形式化。

他将草稿拆分为微小逻辑单元，交由 GitHub Copilot 生成代码骨架，再以 Lean 的 canonical 策略匹配填补细节，过程中也涉及部分手动补全。

最终，整个形式化证明能够在 Lean 中通过验证。

不仅时间大大缩短了，更重要的是满足了“人类可读性”。

要知道 Bruno Le Floch 最初挑战该问题时，曾在论文中宣称 E1689-E2 的所有已知证明都依赖计算机辅助。

直到后来他使用 prover9 ATP（自动定理证明器）给出了一个更具可读性的人类版本，所以才对之前的想法产生动摇：

它是否仍然可以被认为是计算机辅助的，我不确定。

针对这一疑惑，陶哲轩提议今后可以在论文中明确说明，虽然最初的证明是由计算机生成的，但在项目进行过程中，研究者们成功地将其转化为一个人类可读的证明。

并且为了实际验证 AI 能在多大程度上开启自动化形式证明，陶哲轩就此开启了本次 YouTube 首秀。

通过几次亲自尝试，陶哲轩得出了如下结论：

这种半自动化的方法适用于那些技术性强、概念性弱的论证，即那些主要关注细节准确性而非整体概念理解的证明。

并且他再一次强调，AI 辅助证明能够把数学家从一些相对不重要的繁琐事务中解放出来，“让 AI 去做一些它擅长的事”。

在他看来，尽管最终的结果“并不优雅”，但它体现了 AI 辅助证明的巨大潜力。

最后需要说明一下，陶哲轩并非一次就成功了。

据他在视频中透露，前两次的证明过程都出现了一些“bug”——

第一次拿到的代码才到第 5 行他就有点看不懂了，所以选择了重开；第二次虽然完成了所有证明（用时 48 分钟），但由于是新人博主不太熟悉录屏设备，导致屏幕分享失败，因此又只能重来。

数学证明助手迎来 2.0 版本

此外，还有他开发的数学证明助手迎来 2.0 版本升级。

根据介绍，这是一个用 Python 开发的轻量级证明助手，其功能远逊于 Lean、Isabelle 或 Rocq 等完整证明助手，但（希望）它能够轻松用于证明一些简短而繁琐的任务。

一个具体的目标是，为渐近分析提供支持。

两周前，在大模型的帮助之下，他花了四个小时编程得到了这么一个概念验证工具。

结果不到两周，这个工具就迎来了全面改进 ——

首先，将其改造成一个基本的证明助手，使其能够处理一些命题逻辑；其次，根据反馈，这个证明助手变得更为灵活（在几个关键方面刻意模仿精简证明助手）。

目前这个助手有两种模式：假设模式和策略模式。其中策略模式作为默认模式，有点类似于 Lean、Isabelle 或 Rocq 里面那样式儿的策略模式。

目前策略列表主要分为四类：

• 命题策略（主要围绕通过布尔运算操纵命题）

• 线性算术策略（依赖于线性规划及其变体）

• 替代策略 —— 用一个假设或目标替代另一个假设或目标的各种技术

• 简化策略 —— 利用其他可用假设来“简化”假设或目标的方法

当然这些还不是全部，这个助手支持扩展，大家可以在里面进行添加。

举个例子。

如果 x，y，z 是正实数，且 x<2y 和 y<3z+1，证明 x<7z+2。

将它形式化就会变成：

>>> from main import *
>>> p = linarith_exercise()
Starting proof.  Current proof state:
x: pos_real
y: pos_real
z: pos_real
h1: x < 2*y
h2: y < 3z + 1
|- x < 7*z + 2

证明助手接收到指令后，指导助手使用各种“策略”来简化问题，直到问题得到解决。

那么这个问题可以通过线性算术 Linarith () 求解。

>>> p.use(Linarith())
Goal solved by linear arithmetic!
Proof complete!

如果想要有详细解释，也是 OK 的：

>>> from main import *
>>> p = linarith_exercise()
Starting proof.  Current proof state:
x: pos_real
y: pos_real
z: pos_real
h1: x < 2*y
h2: y < 3*z + 1|- x < 7*z + 2
>>> p.use(Linarith(verbose=true))
Checking feasibility of the following inequalities:
1*z > 0
1*x + -7*z >= 2
1*y + -3*z < 1
1*y >0
1*x > 0
1*x + -2*y < 0
Infeasible by summing the following:
1*z > 0 multiplied by 1/4
1*x + -7*z >= 2 multiplied by 1/4
1*y + -3*z < 1 multiplied by -1/2
1*x + -2*y < 0 multiplied by -1/4
Goal solved by linear arithmetic!
Proof complete!

可以看到，首先，它通过反证法进行论证，即采用否定 x≥7z+2 目标 x<7z+2 并将其添加到假设中。

然后，它将假设中所有不等式转化为“线性规划”形式，变量在左边，常数在右边。

最后，它使用精确线性规划来寻找这些不等式的线性组合，从而导致荒谬的不等式，在这种情况下 0<1。

解决完问题之后，还可以使用 proof（）进行检查。

有时候，遇到证明过程会涉及案例拆分的情况，那么证明助手最终会呈现树状结构。

对于这个证明助手，陶哲轩表示：非常满意，并且愿意接受进一步的建议或贡献新的功能。比如引入新的数据类型、公例和策略，或者贡献一些有难度的例子。

此外还计划开发用于估算符号函数的函数空间规范的工具。例如创建部署霍尔德不等式和索博列夫嵌入不等式等定理的策略。看起来 sympy 框架足够灵活，可以为这类对象创建更多的对象类。

感兴趣的旁友，可以前往去体验下哦。

参考链接：

• [1]https://mathstodon.xyz/@tao/114486537464033675

• [2]https://www.youtube.com/watch?v=cyyR7j2ChCI

• [3]https://github.com/teorth/estimate_tools/blob/master/EstimateTools/test/equational.lean

本文来自微信公众号：量子位（ID：QbitAI），作者：白交一水