如何看待陶哲轩等数学家大力推动的 AI 数学证明?

尽管数学极其抽象，但它深根于物质世界和社会世界。数学中的基本概念并非任意发明，它们实际上是从现实世界中抽象出来的。
......
现代数学的许多抽象概念，例如群、环、域、希尔伯特空间、巴拿赫空间等等，都通过抽象的层层递进与现实世界建立联系。尽管数学看似深奥晦涩，它却始终深深扎根于现实世界。这也正是为什么数学结果能够应用于现实世界。例如，关于四维及更高维几何结构的定理可以（并且确实）用于解决现实问题，如通信网络、交通网络和高效数据存储的问题。

虽然我们数学家习惯于在抽象世界中工作，但这种习惯是通过最初（作为学生时）逐步攀登这些抽象层次来形成的。这意味着，我们对概念的理解基于现实——即使我们没有意识到这种基础的存在。（数学家们或许比其他人更清楚自己对心智活动的理解有多么有限，即使是在深入思考问题时。这种认知每当我们「突然灵光一现」获得突破性想法时，就会被迫重新认识到！）

数学是一种由深深扎根于现实、与现实有着根本性联系的生物/心灵所从事的语义活动，它们有动机、有欲望、有好奇心，并驱使自己去理解世界和他人。如下图所示，我们是在数学活动的全景图整个空间中运作。数学知识源于我们作为此类生物使用从世界中抽象出的概念和方法所从事的活动。

相比之下，大型语言模型（LLMs）的活动范围仅限于空间的上层区域，即「数学知识」。它们处理的不是意义，而是纯粹的文本（也就是符号串）。

人类通过研究语义实体中的模式来推动数学进步，而 LLMs 则（隐式地）在它们处理的符号中辨别模式。这些模式反映了符号在人类产生的大量文本中的受欢迎程度（以及，越来越多地，它们自己早期和其他大语言模型的产物，这可能会成为它们和我们的主要问题），见下图。

......
我们是生活在现实世界中的有机生物，作为世界互动的一部分，我们的大脑进化得足以在这个世界中行动、反应和思考。而 LLMs 的输入和输出只是一串符号，仅此而已。这是两种截然不同的活动形式。

任何认为这不是一个巨大区别的人，都应该在图书馆里花些时间，沉浸在标有「人文学科」的丰富文献中。我们能够赋予 LLMs 输出意义，这反映的是我们的人类认知能力，而不是 LLMs 的能力，它们只是按照我们设计的方式工作。（就像我们制造的钟表；钟表本身并没有时间的概念，但我们设计钟表的目的就是让它的状态能够被我们解读为时间。）用「智能」或「思考」这样的词汇来描述 AI 系统是一种类别错误。LLMs 所做的事情和我们完全不同。（可以把它们想象成一个非常高级的钟表，专门设计用来报告互联网中存储的人类知识的「当前状态」。）我们应该以这种视角来看待它们。

凭借未来强大的 AI 能力，你将真的可以开始以一种真正前所未有的规模进行数学运算，未来将会非常激动人心。

记者：你是否尝试过使用 ChatGPT?
Tao: I played with it pretty much as soon as it came out. I posed some difficult math problems, and it gave pretty silly results. It was coherent English, it mentioned the right words, but there was very little depth. Anything really advanced, the early GPTs were not impressive at all.
They were good for fun things—like if you wanted to explain some mathematical topic as a poem or as a story for kids.
陶哲轩：它一出来我就经常用。我问了一些很难的数学问题，结果却很傻。它能用连贯的英语表达，也提到了正确的数学术语，但缺乏深度。对于任何真正前沿的东西，GPTs 都没什么有用之处。
它们只适合用来做一些有趣的事情——比如你想用诗歌或故事的形式给孩子们解释某个数学话题。

Tao: You have a project and ask, “What if I try this approach?” And instead of spending hours and hours actually trying to make it work, you guide a GPT to do it for you.
With o1, you can kind of do this. I gave it a problem I knew how to solve, and I tried to guide the model. First I gave it a hint, and it ignored the hint and did something else, which didn’t work. When I explained this, it apologized and said, “Okay, I’ll do it your way.” And then it carried out my instructions reasonably well, and then it got stuck again, and I had to correct it again. The model never figured out the most clever steps. It could do all the routine things, but it was very unimaginative.
陶哲轩：你有一个命题，然后问：“如果我尝试这种方法会怎么样？” 你无需花费大量时间去实际尝试让它发挥作用，而是引导GPT为你完成。使用 o1，你的确可以做到这一点。
我给它一个我知道如何解决的问题，然后尝试引导模型。我给 o1 一个提示，但它忽略了提示，用了其他证明尝试，提示并没有奏效。
当我解释这一点时，它道歉说：“好的，我会按照你的方式做。” 然后它相当好地执行了我的指令，然后它又卡住了，我不得不再次纠正它。
这个模型从来都找不到最巧妙的步骤。它可以做所有常规的事情，但它非常缺乏想象力。
研究生和人工智能之间的一个关键区别在于，研究生会学习。
你告诉人工智能它的方法行不通，它会道歉，也许会暂时纠正路线，但有时它会突然回到之前尝试过的方法。
而如果你和人工智能开始一个新的会话，你又会回到原点。

记者: 可是您之前也说过，计算机可能会改变数学，使人类更容易相互合作。这是怎么回事？生成式人工智能在这方面到底有什么贡献？
Tao: Technically they aren’t classified as AI, but proof assistants are useful computer tools that check whether a mathematical argument is correct or not. They enable large-scale collaboration in mathematics. That’s a very recent advent.
Math can be very fragile: If one step in a proof is wrong, the whole argument can collapse. If you make a collaborative project with 100 people, you break your proof in 100 pieces and everybody contributes one. But if they don’t coordinate with one another, the pieces might not fit properly. Because of this, it’s very rare to see more than five people on a single project.
陶哲轩：严格来说，它们不算是人工智能，证明助手是检验数学论证正确与否的实用计算机工具。它们能够实现大规模的数学协作。这才刚刚出现。
传统数学研究非常脆弱：如果证明中一步出错，整个论证就可能崩溃。
如果你与100人合作开展一个项目，你可以把你的证明分成100个部分，每个人贡献一个。但只要有一个人不协调(伪证)，所有人的努力都会白费。正因为如此，很少看到超过5个人参与一个项目。
有了证明助手，你无需信任你的同事，因为类型会给你100%的保证。这样你就可以进行大规模工业化的数学证明，而这在目前还不存在。一个人只需专注于证明某些特定类型的结果，这就好比现代供应链，分工合作完成工作。

Tao: The problem is these programs are very fussy. You have to write your argument in a specialized language—you can’t just write it in English. AI may be able to do some translation from human language to the programs. Translating one language to another is almost exactly what large language models are designed to do. The dream is that you just have a conversation with a chatbot explaining your proof, and the chatbot would convert it into a proof-system language as you go.
陶哲轩：唯一的问题是这些程序非常挑剔。你必须用一种专门的语言(Lean)来写你的论证——你不能只用英语。人工智能能够将人类语言翻译成程序语言，将一种语言翻译成另一种语言几乎正是大型语言模型的设计初衷。
理想情况下，你只需与聊天机器人对话，解释你的证明，聊天机器人就会将其转换成证明系统语言(Lean)。