数学研究，在许多时候都是一项孤独的工作。
张益唐远离数学圈 20 年，独自一人潜心思考孪生素数猜想；佩雷尔曼“隐退”长达七年，全身心投入到庞加莱猜想的攻克中，除了偶尔在超市与店员的交集外，他几乎与世隔绝；；安德鲁·怀尔斯(Andrew Wiles) 隐居在书房里用了七年时间证明费马大定理……
图丨张益唐（来源：University of New Hampshire）
这种孤独，在一定程度上源于解决问题所需的深度专注与沉浸，也是因为，他们各自的思索，在很多时候难以向其他人言明与分享。
但近年来，这种状况正在发生改变。
随着交互式定理证明工具（interactive theorem prover，ITP）等计算机工具与 AI 技术的发展，数学领域中越来越多的部分被精细地拆解为各个组成部分，从而转换为能够让计算机理解定理和证明概念的编程语言，这一过程，即为“形式化”（formalisation）。
近期，伦敦帝国理工学院Kevin Buzzard教授所发起的形式化费马大定理证明的项目，就利用了ITP工具 Lean，能够将证明分解为许多小引理，无需理解整个证明，也能为项目做出贡献，便于数学家们进行众包操作。
图丨费马大定理形式化项目的当前进展（来源：Imperial College London）
而这种研究方法，正是菲尔茨奖得主、加州大学洛杉矶分校（UCLA）教授陶哲轩对于数学未来发展的期待。
在接受《科学光谱》（Spektrum der Wissenschaft）采访时，他表示，这些新型的形式化方法正为数学界的合作铺设一条崭新的道路。
尤其是当人工智能领域的发展与数学融合时，可以预见，在不远的将来，数学研究的工作模式将会经历一场革新。那些长久以来悬而未决的重大数学难题，或许将不再遥不可及，我们距离它们的解答可能从未如此之近。
图丨陶哲轩（来源：UCLA）
一种做数学的新方式
在旧金山举行的联合数学会议上，陶哲轩在演讲中似乎暗示了数学家之间缺乏信任。他解释道：“我们是相互信任的，但通常这种信任建立在个人熟悉的基础上。
除非能逐行核对对方的工作，否则与未曾谋面的人合作确实存在难度。一般情况下，五人左右是合作人数的上限。”
然而，自动证明验证器的出现正在改变这一现状。现在，数学家真的可以与数百位素未谋面的人共同合作。无需直接的信任，因为他们上传的代码会由 Lean 编译器进行验证。
陶哲轩指出，现在，我们可以开展比以往规模更大的数学研究。在他形式化多项式 Freiman-Ruzsa（PFR）猜想的过程中，他就与超过 20 人一同工作。
图丨陶哲轩等人的多项式 Freiman-Ruzsa（PFR）猜想的证明形式化项目（来源：Lean）
“我们将证明过程分解为许多小步骤，每个人负责其中一小部分的证明。我不需要逐行检查每个人的贡献是否正确，我只需管理整个项目，确保一切按正确的方向前进。这是一种做数学的新方式，更加现代化。”
而在这些形式化的项目中，也并不需要每个人都必须是程序员。
此前，德国数学家、菲尔兹奖得主Peter Scholze也合作开展了一个 Lean 项目，尽管他甚至对计算机并不了解。
图丨Peter Scholze 的液态张量实验（来源：Lean）
陶哲轩说，“有些人可以专注于数学方向，你只是将一个大的数学任务分解为许多小部分。然后有专门的人将这些小部分转化为形式证明。我们不需要每个人都成为程序员，只需要一部分人具备编程能力即可。这是一种劳动分工。”
二十年前，当机器辅助证明还处于理论阶段时，人们普遍认为必须从零开始——先形式化公理，再做基础几何或代数，而要达到更高层次的数学几乎是无法想象的。那么，是什么变化让形式数学变得切实可行呢？
其中一个重要的变化就是标准数学库的发展。特别是 Lean，有一个名为 mathlib 的庞大项目。所有本科数学的基本定理，如微积分、拓扑等，都已逐一被收入这个库中。人们已经投入大量努力，从公理出发达到了一个相对较高的水平。
图丨Lean Community（来源：Lean）
“而我们的目标就是将库扩展到研究生教育的水平。这样，形式化新数学领域将变得更加容易。此外，搜索功能也得到了改善，因为如果你想证明某个结论，你必须能够找到那些已被确认为真的东西。因此，智能搜索引擎的发展也是一个重大突破。”陶哲轩说道。
而这种变化，并非是计算能力的问题。陶哲轩表示，在完成了整个PFR项目的正式化后，验证它只需要大约半小时。真正的瓶颈在于，如何让更多人使用它，提高其易用性和用户友好性。
在三年内，AI 将成为数学家的有力助手
那么，我们需要形式化所有数学项目吗？
陶哲轩并不这么认为。在他看来，我们尚未到达可以常规性地形式化一切的地步，目前的形式化还需要耗费较多精力，我们必须有所选择。
只有当形式化真正对我们有益时，比如当其他人非常关心结果是否正确时，我们才会选择去形式化。但技术会不断进步，或许更明智的做法是等待时机，直到形式化的操作变得更简单。那时，形式化所需的时间可能将是传统方法的两倍，而非十倍。
甚至，借助人工智能，这一比例还能进一步缩小，乃至小于传统方法所需的时间。未来，我们或许不再需要手动编写证明，而是向类似 GPT 的系统解释证明思路。GPT 将在你讲解过程中尝试在 Lean 中形式化证明。
如果一切检验无误，GPT 会说，“这是你的 LaTeX 论文，这是你的 Lean 证明。如果你愿意，我可以按下按钮，帮你将论文提交给期刊。“在未来，它们可能成为我们出色的助手。
不过，目前为止，证明思路仍然源自人类数学家的想法，陶哲轩表示，最快的形式化路径还是从找到人类的证明开始。人类提出想法，形成证明的初稿，然后再将其转化为形式证明。
未来，这一过程或许会有变化。可能会出现合作项目，其中整体证明方法未知，但人们有各自的小部分证明思路，他们将这些思路形式化并试图整合起来。
他设想，在未来，一个重大定理可能由 20 个人类和一群 AI 共同证明，每个个体负责小部分证明。随着时间推移，这些证明将彼此连接，创造出惊人的成果。这种愿景十分美好，但要实现它，还需多年，部分原因就是当前的形式化过程实在过于痛苦。
此前，Tony Wu 、Christian Szegedy 与 Elon Musk 等xAI的创始人表示，两到三年后，AI 将“解决”数学问题，就像 AlphaGo 在国际象棋上的表现一样——机器在寻找证明方面将比任何人都要好。
图丨Tony Wu 等人此前用 AI 证明奥赛级别的数学定理（来源：Nature）
而陶哲轩的看法则是，在三年内，AI 将成为数学家的有力助手。
当我们试图证明一个定理，遇到某个看似正确却难以证实的步骤时，我们可以求助于 AI，问它能否帮上忙。AI 可能会回应，“我想我能证明这一点。”
但他并不认为数学会在三年内被“解决”，即机器能在寻找证明方面超越任何人类。如果 AI 领域再次取得重大突破，这或许有可能。但更主要的是，在三年内，我们将见证显著的进步，AI 的实际应用将变得越来越便捷。
即使 AI 能够处理当前类型的数学问题，我们也只会转向更高级别的数学研究。比如，我们现在是逐个证明定理，就像工匠一个个手工制作木偶，仔细描绘每一个细节。
但 AI 的介入将使我们能够同时证明数百乃至数千个定理。人类数学家将指导 AI 完成各种任务。因此，陶哲轩认为数学研究的方式会发生变化，但 Tony Wu 等人预测的时间表可能有点激进。
形式化给数学研究带来新的合作方式
在形式化项目中，我们可以与那些不完全理解整个项目数学内容，但精通其中一小部分的人合作。这就像现代设备的制造过程，没有人能独立完成一台电脑的全部制作，从开采金属到软件开发。我们依赖各种专家和庞大的供应链，最终才能生产出智能手机等产品。
在数学合作中，目前要求每个人都需掌握大部分相关数学知识，这是个障碍。但通过形式化，我们可以将项目分割，参与者只需了解自己负责的那一部分。
陶哲轩甚至认为，教科书也应该被形式化。一旦教科书被形式化，就可以创建高度互动的版本，其中对结果的证明可以在高层次上描述，假设读者已有一定知识背景。如果遇到不懂的步骤，读者可以深入查看详细信息，甚至追溯到公理层面。
目前，教科书并未采用这种方式，因为工作量太大。但如果已经在进行形式化，计算机可以自动生成这些互动教科书，这将大大降低数学家跨领域贡献的门槛，因为他们可以精确地承担大型任务中的子任务，而无需理解全部内容。
不过，数学证明不仅仅是验证正确性，它关乎理解。证明可以优美，也可以技术性很强却丑陋，好的证明能加深我们对事物本质的理解。那么，如果把这一过程交给机器，我们是否还能理解它们的发现？
陶哲轩的看法是，数学家的工作是在真与假的空间中探索，通过证明来揭示为什么某些事情是真的。验证真伪的过程耗时且枯燥，但在未来，我们或许可以直接询问 AI，“这是真的吗？”这样可以更高效地探索数学空间，专注于我们真正关心的问题。
AI 将极大地加速这一进程，但在可预见的未来，人类仍将主导这一过程。也许 50 年后情况会有所不同，但短期内，AI 将首先自动化那些无聊且琐碎的任务。
而在解决数学中未解的重大难题方面的表现，陶哲轩表示，“AI 尚且并未超过人类”。要证明一个尚未解决的猜想，首要任务通常是将其分解为更小的部分，每一部分都更有可能被证明。然而，在这个过程中，问题往往会变成更难的形式，而非更简单的。
所以，将问题拆分并探索的过程中，我们会学到许多新知。以费马大定理为例，这原本是一个关于自然数的简单猜想，但为了证明它而发展出的数学理论已远远超出了自然数的范畴。因此，攻克一个证明远不止于证实单一实例那么简单。
假设 AI 给出了一种复杂的证明，我们可以与其合作，对其进行分析。例如，如果这份证明基于 10 个假设得出一个结论，那么如果我们删去其中一个假设，证明是否依然成立？这是一门尚未真正形成的新科学，因为我们还没有大量的 AI 生成证明。
但陶哲轩认为，未来会出现一种新型数学家，他们将致力于使 AI 生成的数学证明变得更加易于理解。这类似于理论科学与实验科学的关系，我们经常通过实证方法发现新知，然后通过更多实验探索自然法则。
目前，数学界尚未采取这样的做法，但他相信将来会有一批人专门从事从初始缺乏直观理解的 AI 证明中提炼洞见的工作。
AI 会终结数学研究，还是给数学带来更光明的未来？
在陶哲轩看来，AI 的介入将催生出全新的数学研究方式，这是我们所未曾经历的。未来将出现项目管理型数学家，他们能够组织复杂项目，虽然未必理解所有数学细节，但擅长将大问题分解为小任务，并分配给其他人，同时具备出色的团队协作能力。
此外，还有专注于特定领域的专家，擅长训练 AI 处理特定类型数学问题的人才，以及能够将 AI 证明转化为人类可读形式的研究者。
“数学研究将更加类似于其他现代行业的工作模式，如同新闻业一样，不同角色拥有各自的专业技能——编辑、记者、商业人士等，数学界最终也将呈现类似的分工格局。”
我们做的数学运算是与我们的大脑相匹配的，但如果 AI 在某个时候变得比人类聪明，它们是否会进入一个我们难以理解的领域？
陶哲轩并不这么认为，因为数学的范围早已超出任何单一人类的认知。数学家们经常依赖他人已经证明的结果，他们大致明白其正确性，有某种直觉，但通常无法将其彻底还原至最基本的公理。他们知道在哪里查找答案，或者至少知道向谁求助。
实际上，目前我们已经有了大量仅由计算机验证的定理，其中涉及巨大的计算量。这些定理理论上可以通过人工验证，但没人愿意投入如此多时间，且这并无实际价值。
因此，他觉得人类能够适应这种变化。并非必须让一个人检查一切。让计算机代劳检查工作，并没有什么问题。
在数学前沿领域，跨学科融合正蓬勃发展，从表面看似无关的领域中汲取灵感。对于 AI 而言，如果它掌握了这些领域的知识，或许能给出启示：“何不看看这里？这可能有助于你解决问题。”
对此，陶哲轩充满期待地说：“利用 AI 来创建或至少指出潜在的联系，这是一个非常激动人心的潜在应用。不过，目前AI的成功率还相当低，它可能会给出十个建议，其中可能只有一个是有价值的，其余九个都是无用的。事实上，这甚至还不如随机选择。但未来这一状况可能有所改变。”
就像 Stephen Wolfram 所说的，关键在于——找到那些“足够有趣”的方向。
图丨Stephen Wolfram的访谈（来源：Imagination In Action）
谈及数学 AI 训练面临的挑战，他分析，数据不足是关键问题之一。尽管互联网上有大量可供训练的论文资源，但他认为很多直觉并未体现在印刷的期刊文章中，而是存在于数学家之间的交流、讲座以及指导学生的过程中。
“有时候我会开玩笑说，我们需要让 GPT 这样的系统接受标准的研究生教育，坐在研究生课堂上像学生那样提问和学习，模仿人类学习数学的方式。”
而这种数据缺乏的原因之一在于，人们所发表的证明，往往是高度浓缩的，即使将人类历史上所有已发表的数学成果汇总，相较于 AI 模型的训练数据规模也显得微不足道。
陶哲轩说道，“人们只发表成功的故事。真正珍贵的数据来自于尝试过程中的失败，即当某人尝试某种方法但未能奏效，但他们知道如何修正。然而，他们通常只发表成功的部分，而不记录整个尝试的过程。”
当前，数学界还没有医学界那种注册登记研究（Registry）的文化。但也许未来形式化将变得非常高效，可以实时形式化。
届时，在使用某种先进的 AI 技术进行研究项目，并寻求资金支持时，数学界就可能需要同意记录下尝试和失败的过程。这样记录下来的信息可以用于训练未来的 AI，或者帮助其他正在研究相似问题的团队避免重复犯错。
而目前，数学家们浪费了太多时间。陶哲轩直言不讳地说：“非常多的知识被局限在个别数学家的头脑中，只有极小一部分得以明确表达。但随着我们不断形式化知识，越来越多的隐性知识将变得显性化，这将带来意想不到的好处。”
参考资料：
[1]. https://www.spektrum.de/news/wie-ki-und-beweispruefer-die-arbeit-von-mathematikern-veraendern/2210083
本文内容不代表平台立场，不构成任何投资意见和建议，以个人官网/官方/公司公告为准。
热门跟贴