陶哲轩可太喜爱 GPT 系列大语言模型了！
近几个月来，闻名数学家陶哲轩热衷于用 ChatGPT、GPT-4 等 AI 东西辅佐处理数学问题。咱们也一直在持续地重视，这不今天又看到了他运用 GPT-4 来帮助自己证明数学定理。
不由猎奇，是什么样的数学定理呢？
依据陶哲轩的介绍，他最近在包括有限多个实变量的不等式理论中有一个完成的示例成果，并很快会发表在 arXiv 上。
因此，他最终决定开端了解 Lean4 交互式证明系统，运用必要的辅佐 AI 东西（GPT-4）来帮助自己来运用。他期望能够实现相当简单的形式化。
咱们也搜到了一篇陶哲轩的关于麦克劳林（Maclaurin）型不等式的论文，不知道是不是同一篇。
论文地址：browse.arxiv.org/pdf/2310.05…
陶哲轩在 IPAM 机器辅佐证明研讨会上看过几次 Lean 演示，在那里有人主张他玩一玩自然数游戏，以此了解 Lean 中用来证明定理的根本语法和策略。
他发现自己很能上手这个游戏，其间证明成果与其本科实剖析书中前面的章节十分相似，比方依据皮亚诺公理树立乘法交换律和结合律等根本管用现实。此外还让他想起了自己在《QED-an interactive textbook》中编码过的逻辑游戏。
大约 3 个小时后，陶哲轩玩到了「高档乘法」，并方案之后在闲暇时刻继续玩下去。
自然数游戏地址：www.ma.imperial.ac.uk/~buzzard/xe…
然而，考虑到自然数游戏中有限的可用东西集，陶哲轩还没有发现 GPT-4 对回答该游戏直接有用，它给出的回答方案通常包括未纳入游戏的方法。不过，他发现 GPT-4 当然对 Lean 很有帮助，他能够从中得到有关问题的有用答复。
随着关卡越来越难，GPT-4 肯定会更有用。比方，在 Z 是 X 的明显成果以及 Y 正在处理各种奇妙语法问题（不然这些问题会十分令人沮丧）的情况下，问它「假如我知道了 X 和 Y，怎么证明 Z 呢？」。陶哲轩发现，自然数游戏似乎具有比文档实际发表的更多的 lean 库。
关于陶哲轩的测验，有网友表示很帅。Lean 十分好。有很多工作需要编写经过验证的证明查看器，比方 SAT、SMT、sharp-SAT 等也运用 Lean。
还有人问陶哲轩，「假如让你猜的话，LLM 需要多少年才能具有逾越全人类的写证明能力呢？」
看来，要想回答这个问题，陶哲轩的大模型试验之旅还将继续下去。
博客链接：
mathstodon.xyz/@tao/111206…
