新智元报道

编辑：桃子 KingHZ

【新智元导读】菲尔兹奖得主陶哲轩再放大招，仅数天时间，开源的概念验证工具借助Copilot迭代至2.0版本。而在最新视频中，他甚至用AI在33分钟「盲做」形式化一页证明，效率惊人。

数学大神陶哲轩携手ChatGPT，打造了开源项目——数学概念验证工具，专攻任意正参数的不等式证明。

没想到，才几天的时间，这款工具迎来2.0版本惊艳升级！

它已从最初的自动化验证框架，摇身一变，成为如今灵活的证明助手。

2.0版不仅能全自动证明，还支持半自动交互式证明。

在设计过程中，他不仅融入了命题逻辑，还模仿Lean证明助手的精髓，结合Python神器sympy，让工具变得更强大、更通用。

这个工具的巨大优势在于，能够让人类数学家与AI助手无缝协作，攻克繁琐计算。

值得一提的是，GitHub Copilot在陶哲轩工具2.0版本中，发挥了重要的作用。

仅数天，2.0版来袭

数学证明助手2.0主要用于证明简短但繁琐的任务，比如验证不等式推导。

这次更新特意添加了对渐近估计的支持。

项目链接：https://github.com/teorth/estimates

这个证明助手有两种工作模式：假设模式（Assumption mode）与策略模式（Tactic mode）。

大多数练习开始后默认处于策略模式，其界面风格模仿了现代的形式化证明系统，如Lean、Isabelle或Rocq。

上手简单

新根据上手简单，使用方便，比如要证明下列不等式：

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

在Python中，定义一个函数就可以了。

deflinarith_exercise: p= ProofAssistant x, y, z = p.vars( "pos_real", "x", "y", "z") p.assume(x < 2*y, "h1") p.assume(y < 3*z+ 1, "h2") p.begin_proof(x < 7*z+ 2) returnp

在交互式 Python 环境中：

>>> 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

自定义证明任务

1. 初始化：

p= ProofAssistant

2. 添加变量：

x = p. var( "real", "x") y, z = p.vars( "pos_int", "y", "z")

3. 添加假设：

p.assume(x + y + z <= 3, "h") p.assume((x >= y) & (y >= z), "h2")

4. 开始目标：

p.begin_proof(E q(z,1)) # 开始证明 z = 1

此外，还支持引用预置引理。

因为设计目标是可扩展性强，新版本还鼓励用户自行提出或贡献新的策略。

策略是用于将当前证明状态转化为零个或多个后续证明状态的方法。

通常通过ProofAssistant的.use方法调用。

渐近分析

这个证明辅助工具最初的设计动机之一，是为了构建一个可以操控渐近估计的环境，例如如下几种常见形式：

• X≲Y也可写作 X=O(Y)），表示存在某个绝对常数C，使得∣X∣≤C；

• X≪Y（也可写作 X=o(Y)），表示对任意常数ε>0，只要渐近参数足够大，就有 ∣X∣≤εY；

• X≍Y（也可写作 X=Θ(Y)），表示X≲Y且Y≲X。

在sympy中，这种渐近行为是通过如下方式实现的：

首先，陶哲轩等定义了新的sympy表达式类型，称为OrderOfMagnitude，对应于所讨论的数量级空间O。

这种表达式虽然不是具体的数值，但支持多种代数操作，例如加法、乘法、实数次幂以及数量级比较。

然而需要注意的是，在该数量级系统中不存在「零」或「减法」的概念。

接下来，他们定义了一个名为Theta的操作。

它将正实数的sympy表达式映射为OrderOfMagnitude表达式，能够形式化表示上述渐近关系：

• X≲Y：形式化为 lesssim(X, Y)，语法糖为 Theta(Abs(X)) <= Theta(Y)；

• X≪Y：形式化为 ll(X, Y)，语法糖为 Theta(Abs(X)) < Theta(Y)；

• X≍Y：形式化为 asymp(X, Y)，语法糖为 Eq(Theta(X), Theta(Y))。

在sympy中，还内建了各种渐近运算的规则，例如：

• 对于任意数值常数 C，有Θ(C) 会简化为Θ(1)；

• 对于两个表达式X, Y，有 Θ(X+Y)会简化为 max⁡(Θ(X),Θ(Y))； 等等。

以下是一个使用证明辅助工具建立渐近估计的简单示例：

假设已知正整数N和两个正实数x和y，满足：x≤2N^2以及y<3N

任务是推导出：xy≲N^4

首先，定义对应函数：

def loglinarith_exercise: p = ProofAssistant N = p. var( "pos_int", "N") x, y = p. vars( "pos_real", "x", "y") p. assume(x <= 2*N** 2, "h1") p. assume(y < 3*N, "h2") p. begin_proof( lesssim(x*y, N** 4)) return p

然后，执行相关命令，自动完成相关证明：

>>> from main import * >>> p = loglinarith _exercise Starting proof. Current proof state: N: pos_int x: pos _real y: pos_real h1: x <= 2 *N**2 h2: y < 3*N |- Theta(x)*Theta(y) <= Theta(N)**4 >>> p.use(LogLinarith(verbose=True)) Checking feasibility of the following inequalities: Theta(N) **1 >= Theta(1) Theta(x)**1 * Theta(N) **-2 <= Theta(1) Theta(y)**1 * Theta(N) **-1 <= Theta(1) Theta(x)**1 * Theta(y) **1 * Theta(N)**-4 > Theta(1) Infeasible by multiplying the following: Theta(N) **1 >= Theta(1) raised to power 1 Theta(x)**1 * Theta(N) **-2 <= Theta(1) raised to power -1 Theta(y)**1 * Theta(N) **-1 <= Theta(1) raised to power -1 Theta(x)**1 * Theta(y) **1 * Theta(N)**-4 > Theta(1) raised to power 1 Proof complete!

33分钟「盲做」数学证明

就在刚刚，陶哲轩还发布了一则30多分钟的新视频。

视频中，他抛出了一个令人兴奋的新实验：

用自动化工具，如GitHub Copilot、Lean证明助手，半自动形式化一个仅一页纸的数学证明。

陶哲轩仅用33分钟便完成，且全程「盲目」操作，无需深究证明的高层逻辑。

在帖子介绍中，他提到这次实验是源于，自己在Equational Theories Project中，与作者Bruno Le Floch的交流。

他提供了一个关于命题E1689-E2「人类可读」证明草稿，挑战了此前「所有证明都依赖计算机」的说法。

陶哲轩突发奇想，决定用一种计算方式形式化这个证明，而且完全依赖工具，摒弃对证明整体结构的理解。

他坦言，「这与我通常的形式化工作方式，截然不同。我不试图把握『宏观思路』，而是借助GitHub Copilot的大模型和Lean的canonical匹配策略，专注于细节的准确性」。

在演示视频中，他将Bruno的草稿拆解成细小的逻辑单元，AI工具自动处理约一半细节，剩余部分由他手动补全。

最终，生成了一个能在Lean中通过验证的形式化证明。

用时仅33分钟。

这种「技术性、非概念性」的证明，正是AI工具的用武之地。

陶哲轩认为，这类证明的关键在于，确保每一步逻辑严密，而非依赖深刻的洞察。

AI接管了繁琐的推理，让数学家能专注于如何表达逻辑，而无需反复验证细节。

陶哲轩的这次实验，远不止一个证明的完成。它让我们看到，AI正在重塑研究范式。

参考资料：

GitHub - teorth/estimates: Code to automatically prove or verify estimates in analysis

https://terrytao.wordpress.com/2025/05/01/a-proof-of-concept-tool-to-verify-estimates/