最近,一直冲锋在探索AI辅助研究功能前线的数学大神陶哲轩,总结了ChatGPT对自己数学研究过程的帮助。有趣的是,他发现AI辅助在数学方面的用处倒是有限,但它大大提升的,是自己在次要任务上的能力,比如编码和制作图表。所以说,想要搞好数学研究,还是需要扎实的数学基础,纯靠AI是没用的。数学不好的人,其实AI的帮助可能也没那么大
陶哲轩表示,使用#Python的matplotlib.pyplot库的一个额外收获是,自己现在可以相对轻松地创建定性图表,来说明更多非正式关系了。在以前,他只能用文字或者草草绘制的手写草图来表达这种非正式关系。为此,陶哲轩发现了一个有效的工作流:向ChatGPT请求一个简化示例的代码,然后自己调整和修改代码,直到输出符合预期为止。比如,通过下面这几轮对话,在几分钟内他就得到了自己想要的图表。最后陶哲轩总结道,AI辅助在自己主要研究的数学领域倒是用处有限,但它大大提高了自己在编码、制作图表这类次要任务中的能力,同时也将自己在一般任务中的能力,提升到了至少是初学者的水平。同时他也点出,在自己看来,对于那些精通编程但并不那么精通数学的人来说,AI辅助可能就不会起到这么大的作用。https://chatgpt.com/share/064ae58d-7400-4589-a027-d66a8a8a236e陶哲轩问:「在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:import numpy as np
import matplotlib.pyplot as plt
import matplotlib.animation as animation
# Define the range for x
x = np.linspace(0, 1, 400)
# Define the functions
functions = [lambda x: x, lambda x: x**2, lambda x: x**3, lambda x: x**4]
# Create a figure and axis
fig, ax = plt.subplots()
line, = ax.plot(x, functions[0](x))
# Set axis labels and title
ax.set_xlabel('x')
ax.set_ylabel('f(x)')
ax.set_title('Animated Functions')
# Initialize the animation function
def init():
line.set_ydata([np.nan] * len(x))
return line,
# Update the animation function
def update(frame):
line.set_ydata(functions[frame](x))
ax.set_title(f'Function: $x^{frame+1}$')
return line,
# Create the animation
ani = animation.FuncAnimation(
fig, update, frames=len(functions), init_func=init, blit=True, repeat=True, interval=1000
)
# Save the animation as a gif
ani.save('animated_functions.gif', writer='imagemagick')
plt.show()
同时, ChatGPT还给出了相应解释:首先要导入必要模块,比如导入numpy进行数值运算,导入pyplot进行绘图,导入animation创建动画。然后需要定义x的范围,创建一个从0到1的数组x,包含400个点。接着需要定义函数、创建图形和坐标轴、初始化动画函数等等。
ChatGPT给出的答案很好,但每个动画中只能显示一个函数。为了达到目的,陶哲轩进一步提问道:「如果我想让每个动画显示两个函数呢?例如,第一帧显示$x$和$x^2$,第二帧显示$x^2$和$x^3$,第三帧显示$x^3$和$x^4$。」ChatGPT表示:「要在动画的每一帧显示两个函数,可以修改代码,为每一帧绘制两条线。」1. Install matplotlib if you haven't already:2. Use the following code to create the animation with two functions per frame:import numpy as np
import matplotlib.pyplot as plt
import matplotlib.animation as animation
x = np.linspace(0, 1, 400)
functions = [lambda x: x, lambda x: x**2, lambda x: x**3, lambda x: x**4]
fig, ax = plt.subplots()
line1, = ax.plot(x, functions[0](x), label='$x$')
line2, = ax.plot(x, functions[1](x), label='$x^2$')
ax.set_xlabel('x')
ax.set_ylabel('f(x)')
ax.legend()
ax.set_title('Animated Functions')
def init():
line1.set_ydata([np.nan] * len(x))
line2.set_ydata([np.nan] * len(x))
return line1, line2
def update(frame):
line1.set_ydata(functions[frame](x))
line2.set_ydata(functions[frame+1](x))
ax.legend([f'$x^{frame+1}$', f'$x^{frame+2}$'])
return line1, line2
ani = animation.FuncAnimation(
fig, update, frames=len(functions)-1, init_func=init, blit=True, repeat=True, interval=1000
)
ani.save('animated_double_functions.gif', writer='imagemagick')
plt.show()
随后ChatGPT照例给出了详细解释:为了在「0,1」的区间上创建($x$和$x^2$,$x^2$和$x^3$,$x^3$和$x^4$)的函数,需要定义x的范围、定义函数、创建图形和坐标轴、初始化动画函数等。陶哲轩表示:「这样就差不多可以了,但图例似乎无法随动画更新,它会停留在x^3和 x^4。有没有办法在每一帧都更新图例?」针对这个问题,ChatGPT给出了对策,就是通过清除现有图例并创建新的图例,来更新每一帧的图例。随后,ChatGPT贴心地给出了可以正确更新图例的修改后的代码。import numpy as np
import matplotlib.pyplot as plt
import matplotlib.animation as animation
# Define the range for x
x = np.linspace(0, 1, 400)
# Define the functions
functions = [lambda x: x, lambda x: x**2, lambda x: x**3, lambda x: x**4]
# Create a figure and axis
fig, ax = plt.subplots()
line1, = ax.plot(x, functions[0](x), label='$x$')
line2, = ax.plot(x, functions[1](x), label='$x^2$')
# Set axis labels and title
ax.set_xlabel('x')
ax.set_ylabel('f(x)')
ax.set_title('Animated Functions')
# Initialize the animation function
def init():
line1.set_ydata([np.nan] * len(x))
line2.set_ydata([np.nan] * len(x))
return line1, line2
# Update the animation function
def update(frame):
line1.set_ydata(functions[frame](x))
line2.set_ydata(functions[frame+1](x))
ax.legend([f'$x^{frame+1}$', f'$x^{frame+2}$'])
return line1, line2
# Create the animation
ani = animation.FuncAnimation(
fig, update, frames=len(functions)-1, init_func=init, blit=True, repeat=True, interval=1000
)
# Save the animation as a gif
ani.save('animated_double_functions.gif', writer='imagemagick')
plt.show()
ChatGPT解释道:更新函数中的ax.legend()调用,就可以清除现有图例,并且使用每帧的新标签进行更新了。这样就可以确保,图例反映的是当前显示函数的功能。
「我想让Python绘制一个用数字描述,但用字符串标注的函数图。例如,我想绘制这样一幅图:横轴上标有『今天』、『下周』和『明年』,分别代表x=1、x=2和x=3的位置,纵轴上标有『初级』、『中级』和『专家』,分别代表y=1、y=4和y=9的位置(因此纵向标签的间距并不相等),要绘制的图形是抛物线y=x^2的图形。如何绘制?」ChatGPT回答:「要绘制横轴和纵轴用字符串标注但与特定数值相对应的图表,可以使用matplotlib库并自定义刻度标签。」1. Install matplotlib if you haven't already:2. Use the following code to create the plot:import numpy as np
import matplotlib.pyplot as plt
x_values = [1, 2, 3]
y_values = [1, 4, 9]
x_labels = ["Today", "Next week", "Next year"]
y_labels = ["Beginner", "Intermediate", "Expert"]
x = np.linspace(1, 3, 100)
y = x**2
fig, ax = plt.subplots()
ax.plot(x, y, label='$y=x^2$')
ax.set_xlabel('Time')
ax.set_ylabel('Level')
ax.set_xticks(x_values)
ax.set_xticklabels(x_labels)
ax.set_yticks(y_values)
ax.set_yticklabels(y_labels)
ax.legend()
ax.set_title('Parabola $y=x^2$ with Custom Axis Labels')
plt.show()
网友:图表存在「幻觉」
在陶哲轩的评论区,有网友指出了此图的准确性有问题:两条线之间的山谷意味着什么?那里的相对位移应该更大才对。在他看来,用手绘涂鸦来表达这类非正式想法是比较合适的,可以让形式与内容相匹配,避免了使用和标准化这些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