转载自新智元微信公众号。

编辑：桃子 KingHZ

【新智元导读】

没想到，才几天的时间，这款工具迎来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中，定义一个函数就可以了。

def linarith_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)    return p

在交互式 Python 环境中：

>>> from main import *>>> p = linarith_exercise()Starting proof.  Current proof state:x: pos_realy: pos_realz: pos_realh1: x < 2*yh2: y < 3*z+1|- x < 7*z+2

自定义证明任务