机器之心报道 编辑：杜伟、大盘鸡 本周二，我们报道了 菲尔兹奖得主陶哲轩的一个开源项目 —— 在大模型的协助下编写了一个概念验证软件工具，来验证涉及任意正参数的给定估计是否成立（在 常数因子范围内）。 在项目中，他开发了一个用于自动（或半自动）证明分析中估计值的框架。估计值是 X≲Y（在渐近记法中表示 X=O (Y)）或 X≪Y（在渐近符号中表示 X=o (Y)） 形式的不等式。 这才几天的时间，这个估计验证工具的 2.0 版本就来了！ 陶哲轩对该工具进行了两次全面改进。 根据项目简介，这是一个利用 Python 开发的轻量级证明助手，其功能远逊于 Lean、Isabelle 或 Rocq 等完整证明助手，但希望它能够轻松用于证明一些简短而繁琐 的任务，例如验证一个不等式或估计是否由其他不等式或估计推导出来。该助手的一个具体目标是为渐近估计（asymptotic estimates）提供支持。 具体实现过程 首先，他将其改造成一个基础的证明助手（proof assistant），同时能够处理一些命题逻辑；接着，他根据评论者的反馈，将其 改造成一个更加灵活的证明助手 （在几个关键方面特意模仿了 Lean 证明助 ...

机器之心报道 在这个项目中，陶哲轩开发了一个用于自动（或半自动）证明分析中估计值的框架。估计值是 X≲Y（在渐近记法中表示 X=O (Y)）或 X≪Y（在渐近符号中表示 X=o (Y)）形式的不等式。 编辑：蛋酱、陈陈 这个五一假期，世界顶级数学家是如何度过的？ 菲尔兹奖得主陶哲轩，似乎是忙着发布自己的开源项目：「我在大模型的协助下编写了一个概念验证软件工具，用于验证涉及任意正参数的给定估计是否成立 （在常数因子范围内）。」 项目地址：https://github.com/teorth/estimates 为什么要做这样一个工具？这就要从近期陶哲轩和 Bjoern Bringmann（陶哲轩曾经的博士生，现为普林斯顿大学助理教授）的讨论说起。 对于代数、微积分和数值分析等领域的许多数学任务来说，符号数学软件包已经非常「发达」了。但目前还没有类似的复杂工具来验证渐近估计 —— 在损失不变 的情况下，对于任意大的参数都应该成立的不等式。尤其重要的是函数估计，其中参数涉及一个未知函数或序列（存在于某个合适的函数空间，如一个空间）。 陶哲轩将二人的讨论结果写成了一篇博客，重点讨论了更简单的渐近估计情况，即涉及有限数量 ...