陶哲轩点破“天机”：不懂数学别想靠ChatGPT飞升

使用ChatGPT一年半了，陶哲轩的感想如何？

最近，一直冲锋在探索AI辅助研究功能前线的数学大神陶哲轩，总结了ChatGPT对自己数学研究过程的帮助。

有趣的是，他发现AI辅助在数学方面的用处倒是有限，但它大大提升的，是自己在次要任务上的能力，比如编码和制作图表。

所以说，想要搞好数学研究，还是需要扎实的数学基础，纯靠AI是没用的。

数学不好的人，其实AI的帮助可能也没那么大

陶哲轩表示，使用#Python的matplotlib.pyplot库的一个额外收获是，自己现在可以相对轻松地创建定性图表，来说明更多非正式关系了。

在以前，他只能用文字或者草草绘制的手写草图来表达这种非正式关系。

为此，陶哲轩发现了一个有效的工作流：向ChatGPT请求一个简化示例的代码，然后自己调整和修改代码，直到输出符合预期为止。

比如，通过下面这几轮对话，在几分钟内他就得到了自己想要的图表。

最后陶哲轩总结道，AI辅助在自己主要研究的数学领域倒是用处有限，但它大大提高了自己在编码、制作图表这类次要任务中的能力，同时也将自己在一般任务中的能力，提升到了至少是初学者的水平。

同时他也点出，在自己看来，对于那些精通编程但并不那么精通数学的人来说，AI辅助可能就不会起到这么大的作用。

陶哲轩和ChatGPT的对话，具体如下：

陶哲轩问：“在Python中，我知道如何使用pyplot软件包制作图形的单个图像。有什么方法可以让我用Python制作多个图形的幻灯片或其他动画图像吗？比如，制作一个幻灯片，展示函数$x$， $x^2$， $x^3$， $x^4$对于$x \in [0，1]$的图形。”

ChatGPT回答说：“是的，你可以使用matplotlib包中的matplotlib.animation模块，在Python中创建多个图形的幻灯片或动画图像。 ”

接下来，ChatGPT就给出了创建该函数动画的具体步骤，详细给出了代码：

1. Install matplotlib if you haven't already:

2. Use the following code to create an animation:

同时， ChatGPT还给出了相应解释：首先要导入必要模块，比如导入numpy进行数值运算，导入pyplot进行绘图，导入animation创建动画。

然后需要定义x的范围，创建一个从0到1的数组x，包含400个点。

接着需要定义函数、创建图形和坐标轴、初始化动画函数等等。

ChatGPT给出的答案很好，但每个动画中只能显示一个函数。

为了达到目的，陶哲轩进一步提问道：“如果我想让每个动画显示两个函数呢？例如，第一帧显示$x$和$x^2$，第二帧显示$x^2$和$x^3$，第三帧显示$x^3$和$x^4$。”

ChatGPT表示：“要在动画的每一帧显示两个函数，可以修改代码，为每一帧绘制两条线。”

接下来，ChatGPT还是给出了详细的代码。

随后ChatGPT照例给出了详细解释：为了在“0，1”的区间上创建（$x$和$x^2$，$x^2$和$x^3$，$x^3$和$x^4$）的函数，需要定义x的范围、定义函数、创建图形和坐标轴、初始化动画函数等。

陶哲轩表示：“这样就差不多可以了，但图例似乎无法随动画更新，它会停留在x^3和 x^4。有没有办法在每一帧都更新图例？”

针对这个问题，ChatGPT给出了对策，就是通过清除现有图例并创建新的图例，来更新每一帧的图例。

随后，ChatGPT贴心地给出了可以正确更新图例的修改后的代码。

ChatGPT解释道：更新函数中的ax.legend()调用，就可以清除现有图例，并且使用每帧的新标签进行更新了。这样就可以确保，图例反映的是当前显示函数的功能。

陶哲轩继续提问：“我想让Python绘制一个用数字描述，但用字符串标注的函数图。例如，我想绘制这样一幅图：横轴上标有‘今天’‘下周’‘明年’，分别代表x=1、x=2和x=3的位置，纵轴上标有‘初级’‘中级’‘专家’，分别代表y=1、y=4和y=9的位置（因此纵向标签的间距并不相等），要绘制的图形是抛物线y=x^2的图形。如何绘制？”

ChatGPT回答：“要绘制横轴和纵轴用字符串标注但与特定数值相对应的图表，可以使用matplotlib库并自定义刻度标签。”

并且给出了相应解释。

至此，陶哲轩的问题就被ChatGPT完美解决了。

网友：图表存在“幻觉”

在陶哲轩的评论区，有网友指出了此图的准确性存在问题：两条线之间的山谷意味着什么？那里的相对位移应该更大才对。

在他看来，用手绘涂鸦来表达这类非正式想法是比较合适的，可以让形式与内容相匹配，避免了使用和标准化这些AI工具过程中带来的缺点。

对于这名网友的“找茬”，陶哲轩进行了详尽的回复。

他解释道，如果自己想要传达复杂关系的图像，手绘图是很不方便的，一方面原因是自己不擅长手绘，另一方面，也是因为无法很轻松地编辑出一个草图，让它部分地传达自己的想法。

而借助Python，自己就可以轻松地循环，进行十几次尝试，然后找到一个能捕捉到自己想要的细微差别的方法了。

例如，他确实有意让初级领域和次级领域之间的山谷，在AI的帮助下获得更高的推动力（这个山谷代表着两个相邻的领域）。

在陶哲轩看来，纯数学是自己的主要领域，而计算机编程是次要技能；自己对于设置和安装机器学习软件包并没有直接经验，但后者与这两个专业相邻，所以他会把它放在这个图的中间位置。

而对于图表不够精确这个问题，陶哲轩解释道，数轴上没有数字标签，应该就已经意味着这是一张非正式图像。

或者，他建议我们可以创建其他信号，来更加强调图形的非正式性，比如让线条更厚、更模糊，同时选择不那么“专业”的字体。

这些在Python中是很容易做到的，但如果要手工完成，就只能重绘图像了。

同时，针对这位网友的建议，陶哲轩也表示，在使用ChatGPT/Python之前，自己的确也提前手绘了草图。

随后，陶哲轩又在图表上进行了一些调整，添加了一些不建议使用AI辅助的情况：在几乎没有先验知识的情况下尝试用AI处理中等难度的任务，或者在只有中等先验知识的情况下尝试处理专家难度的任务。

陶哲轩表示，在这种特殊情况下，此类更新在手绘图像上是可行的，并且只需要添加新绘图就可以了，而不是删除或修改现有绘图。

但他强调，对于许多其他类型的修订，使用手绘图像作为主图像来源会很不方便。

“资深用户”陶哲轩

其实早在2023年3月，陶哲轩就开始探索如何将AI加入到自己的工作流里了。

起初，陶哲轩想让ChatGPT根据他的描述直接得到“Kummer定理”这个名字。不过，AI给出的结果却是一个Legendre公式。好在，后续可以根据这个线索，通过传统搜索引擎轻松找到答案。

据此，陶哲轩认为，AI在数学中的作用是提供一个初步解答，然后可以通过更传统的方法进行细化。

接下来，陶哲轩从原理上对比了传统计算机软件工具和AI工具，发现二者的工作流极为不同。

例如，对于传统的LaTeX到PDF编译器来说，只要输入的代码正确，那么一定可以得到一份完美的PDF。但如果输入的代码有格式错误，结果要么是编译错误，要么是一份严重混乱的PDF。

而AI LaTeX编译器则可以更加优雅地处理噪声或格式错误的输入，但它不能以“一键完成”的方式使用，而是需要进行大量的互动。

随后，在大量的尝试中，陶哲轩又发现了一些ChatGPT在处理数学问题时的小亮点。

比如，一旦AI“学会”了用户的需求，用户就可以用最少的解释或预格式化来提供进一步的数据，而AI依然可以推断出一个令人满意的输出。

例如，在随后的此类请求中，即使输入不是MathSciNet格式，AI仍然能够继续之前在附加请求中隐含引入的参考命名约定。

总的来说，这些AI工具并不能帮助直接攻克未解的数学问题，但它们在各种相关的任务中相当有用，尽管之后常常需要一些手动调整。

2023年4月，在经过一段时间的使用之后，陶哲轩针对AI和人类（主要是自己）各自的优势进行了一波总结。

1. 对于每天都要做的任务，陶哲轩已经掌握了足够的技术来优化工作流。在这方面，AI工具的帮助不大。最明显的就是在研究数学，同时也包括他已经极为熟练的邮件撰写。

2. 对于有一些专业知识但很少实践的任务，AI工具是有帮助的。比如创建初稿或者提供灵感，然后陶哲轩自己再去进行验证和完善。这一类的例子包括数据处理、翻译成外语，或以很少使用的格式编写文本（比如，公开演讲、规则文件等）。

3. 对于几乎没有专业知识且不需要极高质量和可靠输出的任务，也可以询问AI工具，并或多或少地听从它的建议。在这里，AI的功能相当于一个操作更简便的搜索引擎。

4. 对于没有专业知识但需要质量和可靠性的任务，就必须咨询人类专家了。一个例子是修理复杂、昂贵且精密的设备。

比如，第二类任务：陶哲轩让GPT用LaTeX输出流程图后，得到了下面这张图片。

可以看到，这张流程图还比较粗糙，不过对于熟练使用LaTeX的陶哲轩来说，只需简单修改一下，即可得到下面这个成品。

再比如，第三类任务：陶哲轩让GPT把自己之前的帖子总结为流程图，结果如下。

2023年9月，陶哲轩对ChatGPT的探索，已经深入到用它来写代码了。

作为实验，他要求ChatGPT写一段Python代码，为每个自然数n计算1，...，n的最长子序列的长度()，其中欧拉全能函数ϕ不递减。

很快，AI便生成了一段极其巧妙的代码。虽然还存在一些偏差，但距离最终答案已经非常接近了。

随后，陶哲轩基于这段初始代码作为起点，手动生成了自己想要的代码，这大概节省了他半个小时的工作量。

因为ChatGPT给出的结果非常好，陶哲轩表示，自己以后还会经常使用它，为类似的计算提供初始代码。

一看陶哲轩对AI的尝试已经来到了代码领域，坐不住的网友们便给他安利一波AI加持的VSCode。

对此，陶哲轩本人十分“听劝”，竟然放下了自己已经用了近10年的TeXnicCenter+MiKTeX，立刻将工作流升级到了VSCode+TeX Live+LaTeX workshop+GitHub Copilot。

在初次尝试中，他主要用的是很基础的代码片段功能（code snippets feature）——

通过输入触发词（比如“cor”），并按下Tab键来创建整个推论环境（corollary environment），非常节省时间。

就在不到一个月之后，陶哲轩表示，他已经在用Github Copilot为自己的博客文章撰写提供助力了。

比如在下面这个例子中，陶哲轩将一个积分分成三部分，并描述了如何估计第一部分，随后Copilot正确地给出了剩下两部分的估计方法。

他预计，在最终的成稿中，大约有十几句来自Copilot的建议会以某种形式呈现出来。

随着AI自身的进化，以及愈发熟练地掌握知识，陶哲轩发现AI已经不再局限于外围的任务，而是可以涉足数学领域本身了。

比如，在使用Lean进行自然数游戏研究时，他便通过GPT-4的辅助得到了关于有限多个实变量不等式理论的成果。

并且，随着关卡变得越来越难，GPT的作用也越加能够凸显出来。

而在这波体验之后，大神本人也算是彻底“入坑”了。

OK，自然数游戏已经完成，现在我要去安装Lean并编写一个“hello world”程序了。

几天之后，又是一大波心得总结：

• Github Copilot在完成简短论证时非常有用，尽管它的较长建议通常是错误的。但即使是错误的建议也能帮助我学到正确的语法。

  
  

• GPT-4在澄清Lean语法的细微差别并提供我用数学英语解释的步骤的Lean翻译建议方面有一定帮助。然而，它似乎更受Lean3语法和最佳实践的影响，而不是Lean4。

终于，在经过差不多100个小时的努力之后，陶哲轩用Lean4完成了Maclaurin型不等式论文的形式化。

大神毕竟是大神，陶哲轩很快又再一次跑通了用AI工具辅助数学研究——形式化多项式Freiman-Ruzsa猜想的证明，大获成功。

参考资料：

https://mathstodon.xyz/@tao/112735110429475270

https://mathstodon.xyz/@tao/110250470289337319

本文来自微信公众号：新智元（ID：AI_era），作者：Aeneas、好困