目录：

写作目的

最近半年有个愈演愈烈的想法，以至我无法忽视。暂记于此，看看十年后我怎么看我现在的想法。

一点拙见，还望看客海涵。如能抛砖引玉，当不胜荣幸。

先前想法

以前我觉得，数学相比于其他学科，最吸引我的点在于：

  • 重复劳动少，如果同样的证明方法出现了几次，那一定有人会去研究这些证明方法的本质，然后给出某种理论或者范畴，从而减少重复劳动。这种对已总结规律的高阶归纳，在其他学科里都看不见。大概是其他学科里，规律本身是昂贵稀缺的东西，因而很难基于这些规律再总结。
  • 知识贬值慢，上一次数学的范式革命还是集合论，而这些丝毫没有影响到线性代数、抽象代数之类的发展。而老师一直津津乐道的“爱因斯坦借助黎曼几何完成了广义相对论”，数学领先其他学科如斯。因此，短期内数学定理无用在我看来并不成问题：只要它还是先进知识，我就可以等。我也很喜欢数学那种跨时空的交流。
  • 自成体系，不假外物。数学不依赖实验，因此其知识产出成本相对低，而且成本和外界变化的关系不大。举个例子，高能物理受限于实验设备，犹有所待者也；而数学真正能做到“彼且恶乎待哉”，工具不足说明自身能力不足，不致屈贾谊于长沙。
  • 没有学术造假。相比于其他学科不得不信任作者实验数据，数学优势在于可以独立验证作者产出的正确性。这促使我们可以更加信任其他人成果（开源比闭源更让人信任，尤其是当作者已经作古），也令我们更安心地借鉴他人成果，而不是第一步先做实验复现。虽然我认为这一点还不够，最佳状态应该是不依赖于人本身注意力的无条件正确（比如通过形式验证证明），但是目前形式注明成本居高不下，而数学已经是所有学科中最接近这一理想的了。在我看来，这是任何分布式共同体必然承担的代价。

目前观察、展望

我承认，陶哲轩在今年3月发表的博客震惊到我了。他说，他使用AI来写Lean，成功将完成Lean证明的时间缩小到了普通数学家可接受的水平。

与此同时，“世纪定理”有限单群分类定理的证明整合在过去几十年一直令人头疼，谁也不能保证一万页的证明里真的不会藏着一两个漏洞。AI+Lean为我们带来了曙光：一旦形式化，那么证明的正确性就可以通过机器验证，每一篇论文也都可以被归类到合适的引理附近。目前机器不擅长证明定理，但是仿写却是它最擅长的。最关键的是，AI借此可以学习大量的证明方法，用在后续的自我进化中。

接下来有几个很有想象力的时间节点，依次列举如下：

一行

AI+Lean可以独立完成人类花费1行左右的证明。这意味着，AI可以完成大多数人认为“显然”的证明，而人类只需要按照原有计划写出证明本身。这标志着形式化证明的成本与人类写作的成本相当，而且AI+Lean的证明正确性可以被机器验证。陶哲轩3月的博客来看，这个时间节点感觉应该很快了（也许10年内？）。

在我看来，此后数学审稿理应变化（但是由于守旧性，可能大家仍然会坚持原来的审稿方式，毕竟改变共识的成本未必低于共识改变所能节省的成本）。此时理想的数学审稿应该作者提供证明思路、概要，然后AI+Lean完成证明，审稿人只需要验证论文创新性。这样一来，数学审稿的成本将会大幅降低。

半页

AI+Lean可以独立完成（人类花费）半页纸的证明（允许借助人类写的证明思路概要），基本达到低年级数学本科生水平。在这个时间点，人类的写作将会局限于写证明思路、概要，以及这个研究的来源、意义和研究可能相关的方向。

我必须解释为什么我这么想：比如20页的证明里，大概50%是常规的证明方法，在其他论文里早就出现过类似方法，只不过作者为了完整性不得不写出。读者本身也就是想知道大概怎么分类的或者主要证明思想是什么，然后确认证明本身正确。读者不会关心细节，也不会真的用这些细节。那么完成这些常规证明的劳动，我认为是重复劳动，而且是可被AI取代的重复劳动。

但是如果我们仍然必须读Lean的证明，那么这件事本身就将成为成本大头，因为Lean的证明本身冗长（本质上我们仍然必须证明大量人类认为“显然”的命题），因此随着机器证明成本的降低，人类必然无法再直接阅读机器证明本身，而是只能阅读人类写的证明思路、概要。

此时，由于AI产出会极大加快数学论文写作流程和增加写作质量，那么我相信，此时审稿很可能要求附带形式注明+审稿人只验证创新性，以降低审稿成本。

十页

AI+Lean可以独立完成十页甚至更多的证明。

我认为这时候AI+Lean应该算是当今的数学博士水平了，但是廉价得多。到时候，数学民工（指AI）不限量情况下，还需要现在这么多理论数学家吗？如果不需要的话，也许那一批理论数学家，就是最后的维持现有形式的理论数学家（能兼做大学数学基础课、数学专业课等等的教书老师和数学研究工作者）了，之后教研或许分离，或者数学家转做应用。应用数学家仍然大量需要：总要有人负责在实际问题和数学之间架起桥梁，充当翻译。

当然，这个畅想的时间点不知道有生之年能不能看见，因此我觉得大可以相信后人智慧。我也实在无法想象这个时间点的数学长什么样。

大胆猜测：在这个时间点，数学的工作将会变成寻找刻画命题价值的函数，以及寻找合适的AI温度。整个数学的价值将会被重新评估。希尔伯特的梦想也许将重新照回现实。

更有想象力的猜测（翻译：更不负责任的猜测）：目前整个观察仍然局限在数学体系之内，Lean负责验证逻辑链。有没有可能，AI可以自己学会逻辑链，并应用于其他学科？现在GPT就是“掌握百科全书的6岁儿童”：掌握大量知识，但是完全没有逻辑分析能力，像6岁儿童一样分不清事实和想象，容易被诱导；可以学别人说话，但是看起来不能指望他完全理解自己在说什么。如果AI可以将逻辑知识迁移到这里，区分事实和想象，甚至通过实验自己掌控的设备主动剔除知识库中的不可靠内容，去芜存菁，那么AI的应用范围将极大延伸。如果可以更进一步，用逻辑整合已有知识，那AI前途更不可估量。唯一的难点：如何让AI学会逻辑，或者给AI外挂逻辑？毕竟这些逻辑似乎并不能真的写成Lean命题。反正我目前没想法。

工作展望

  • 这样除去AI+Lean方向的研究，剩下的所有理论研究，在我看来，未来知识都会贬值：因为这些研究并不会立刻应用，而AI+Lean会在数十年后降低这些研究的成本。
  • AI+Lean的研究不会贬值，是因为这些劳动是贬值的必要条件，必然发生在贬值之前、期间，无法置于AI+Lean浪潮之后。
  • 又或者，寻找应用数学的研究，因为这些研究会立刻应用，而且AI+Lean无法立刻应用，因此不受AI+Lean浪潮影响。
  • 我计划接下来学习Lean，以及尝试用AI辅助完成一些证明。希望它对未来有用。
  • 本想深入研究AI+Lean作为未来课题，但是不知道现在开始晚不晚……毕竟我已经博士快毕业了，之前完全没有涉及这个方向。叹叹。

吴老师评论

我曾经和吴老师讨论过这个话题，暂记下他的态度：

  1. 我们都不了解Lean，不应该在这个基础上讨论AI+Lean的未来。
  2. 他也无意具体了解AI+Lean，他认为这是邪道。
  3. 他认为数学家看到密切相关的工作，必然会想要读全文证明，而不是只读摘要、证明思路。那么附上AI+Lean生成的证明只会徒增成本。
  4. 他认为没有杂志会接受AI+Lean完成的论文——尤其我认为某个时刻以后，数学家本人很可能完全不会看AI生成的内容，他认为这极不负责任。
  5. AI工作不具有创新性，而数学家的研究意义在于其创新性。所以他认为，需要借助AI完成证明的工作是无趣的。
  6. AI很难形成某种价值判断，以评估每个命题的价值。单纯生成一堆正确的命题，远不如提出“chaos”这样的概念并推而广之——数学史证明了这一点。
  7. （这点他是没说，但我觉得我完全可以推论）在可见的未来，AI+Lean并不能大幅降低数学的各环节成本，AI+Lean只能帮助写作，而不是思考。因此，数学家的工作不会被AI+Lean取代。