近几个月来，著名数学家陶哲轩热衷于用 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 个小时后，陶哲轩玩到了「高级乘法」，并计划之后在空闲时间继续玩下去