陶哲轩：我用GPT-4辅助证明不等式定理，论文还会上传arXiv

横槊赋诗

陶哲轩可太喜欢 GPT 系列大语言模型了！
图片

近几个月来，著名数学家陶哲轩热衷于用 ChatGPT、GPT-4 等 AI 工具辅助解决数学问题。我们也一直在持续地关注，这不今天又看到了他使用 GPT-4 来帮助自己证明数学定理。

不禁好奇，是什么样的数学定理呢？

根据陶哲轩的介绍，他最近在包含有限多个实变量的不等式理论中有一个完成的示例结果，相关论文很快会发表在 arXiv 上。

因此，他最终决定开始了解 Lean4 交互式证明系统，使用必要的辅助 AI 工具（GPT-4）来帮助自己来使用。他希望能够实现相当简单的形式化。

我们搜到了一篇陶哲轩的关于麦克劳林（Maclaurin）不等式的论文，经查证是他所说的论文。

图片

论文地址：https://browse.arxiv.org/pdf/2310.05328.pdf

陶哲轩在 IPAM 机器辅助证明研讨会上看过几次 Lean 演示，在那里有人建议他玩一玩自然数游戏，以此熟悉 Lean 中用来证明定理的基本语法和策略。

他发现自己很能上手这个游戏，其中证明结果与其本科实分析书中前面的章节非常相似，比如根据皮亚诺公理建立乘法交换律和结合律等基本算数事实。此外还让他想起了自己在《QED-an interactive textbook》中编码过的逻辑游戏。

大约 3 个小时后，陶哲轩玩到了「高级乘法」，并计划之后在空闲时间继续玩下去。

图片

自然数游戏地址：https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game

然而，考虑到自然数游戏中有限的可用工具集，陶哲轩还没有发现 GPT-4 对解答该游戏直接有用，它给出的解答方案通常包含未纳入游戏的方法。不过，他发现 GPT-4 当然对 Lean 很有帮助，他可以从中得到有关问题的有用答复。

随着关卡越来越难，GPT-4 肯定会更有用。比如，在 Z 是 X 的明显结果以及 Y 正在解决各种微妙语法问题（否则这些问题会非常令人沮丧）的情况下，问它「如果我知道了 X 和 Y，如何证明 Z 呢？」。陶哲轩发现，自然数游戏似乎拥有比文档实际披露的更多的 lean 库。

对于陶哲轩的尝试，有网友表示很酷。Lean 非常好。有很多工作需要编写经过验证的证明检查器，比如 SAT、SMT、sharp-SAT 等也使用 Lean。

图片

还有人问陶哲轩，「如果让你猜的话，LLM 需要多少年才能拥有超越全人类的写证明能力呢？」

图片

看来，要想回答这个问题，陶哲轩的大模型试验之旅还将继续下去。

三叶草

他能合法的翻墙吗？

横槊赋诗

三叶草 发表于 2024-10-14 10:49
他能合法的翻墙吗？

他是澳大利亚人，华裔

再说国内也有镜像的

agent124

像他那个档次，用ai来作为自己的助手，没什么问题。但对普通人来说，很容易变成完全依赖ai来做事。所谓的危险就在这里。

123zxy

三叶草 发表于 2024-10-14 10:49
他能合法的翻墙吗？

陶教授去大陆工作啦?

陶哲轩（Terence Chi-Shen Tao），1975年7月17日出生于澳大利亚阿德莱德，华裔数学家，菲尔茨奖获得者，美国加州大学洛杉矶分校James and Carol Collins讲席教授、博士生导师。

tdl416

GPT-4辅助功能厉害。