梦晨发自凹非寺
量子位公众号 QbitAI
陶哲轩点赞转发，《美国数学学会通报》用一整期特刊介绍了 AI 给数学带来的改变。
这些文章读起来很有趣，尽管使我自己即将发表的一篇文章显得多余……这个领域发展太快了！
作者阵容非常豪华，包括菲尔兹奖得主Akshay Venkatesh、华裔数学家郑乐隽、计算机科学家Ernest Davis等多位知名学者。
其中郑乐隽表示，如果最终机器能做得比人类更好，那很好，她将乐意退出数学领域去弹钢琴。
他们提出的观点包括：
AI 的数学能力不完全反映人类的认知过程，依赖于训练数据中的模式，而不是真正理解问题的本质。 合成数学如合成拓扑学和合成微分几何学，提供了一种全新的数学实践方式，允许数学家专注于更深层次的概念和问题。 交互式证明系统与软件工程中的“规范驱动开发”，可以降低数学家的认知负荷、促进数学家之间的合作。 形式化证明技术可能改变数学证明的本质、颠覆数学家的工作方式。 数学届不应被科技公司主导的议程所绑架。
在开篇，编委会写道：
纯粹的数学家习惯于享有很大程度的研究自主和智力自由，这是一种脆弱而宝贵的遗产，可能会因机器的盲目使用而被扫除。另一方面，对同一技术进行深思熟虑和深思熟虑的方法可能会极大地丰富我们的学科。
学科应该如何发展是由我们自己决定的，因此我们邀请数学界认真思考和讨论专刊中提出的问题，并聆听其他领域同行对这些问题进行了深入思考。
现在，是数学家们了解并推动这场辩论，并决定学科未来方向的时候了。
AI 能自动证明定理吗？
计算机已经在数学中发挥了重要作用，尤其是在计算效率方面的提升，但是否能够帮助人类进行数学推理？有一天它们是否会自主进行推理？
数学家Kevin Buzzard概述了神经网络、计算机定理证明器和大型语言模型的最新发展。
Kevin Buzzard 现任英国伦敦帝国理工学院数学教授，他专门研究算术几何和朗兰兹纲领。
回顾整个计算工具的历史，最早 Computer 一词还指人类作为“计算员”，他们的成就不应被低估。
17 世纪早期，苏格兰数学家 John Napier 构造了第一个对数表，他提出如果有更多“计算员”来帮忙，就可以进一步推进这一工作。
另一个代表性成果是 Felkel 和 Vega 在 18 世纪 70 年代发表的整数因式分解表，这使研究素数分布成为可能，最终导致了素数定理的证明。
早期电子计算机出现后，机器在高速计算方面已经远超人类，Computer 一词的含义也发生了变化。
如剑桥大学在 1957 年购买了 EDSAC II 计算机，用于海洋学计算，为现代板块构造理论奠定基础。
这个阶段计算机还只是一个工具，即使目前的计算机也难以像人类一样进行数学推理和定理证明。
神经网络可以用于搜索定理、猜测新定理和寻找反例，如发现了拓扑学中关于结点和边的关系的新定理，以及在表示论中发现了关于 Kazhdan-Lusztig 多项式的新结果，但对于证明深奥复杂的定理还有局限性。
自动定理证明系统（ATP）可以自动证明一些复杂的定理，如罗宾斯猜想。但 ATP 生成的证明往往过于冗长，难以被人类理解。
交互式定理证明系统（ITP）可以用于验证定理的正确性，帮助发现和修正数学文献中的错误，如数学家 Peter Scholze 在液体张量实验（Liquid Tensor Experiment）中承认自己无法掌握所有涉及的数学对象和概念，最终在 Lean 系统帮助下完成。
大模型如 ChatGPT虽然可以生成相关数学内容，但容易产生错误。Buzzard 建议大模型与 ITP 等系统结合使用，通过大模型生成初步证明，然后由 ITP 进行验证，从而提高可靠性。
Buzzard 认为，这些新兴技术可以帮助数学家突破认知障碍，探索更加复杂和更加新颖的数学领域，并最终改变数学家的工作方式，使他们能够将更多时间和精力投入到数学思维和理解上。
另外三篇文章，从不同角度探讨了这些新兴技术如何帮助数学家应对日益增长的复杂性，并开拓新的数学领域。
数学的形式化转向
逻辑学家Jeremy Avigad讨论了自 20 世纪初以来，数学定义和证明可以在具有精确语法和使用规则的形式系统中表示。
Jeremy Avigad 任卡内基梅隆大学哲学和数学教授，在数理逻辑和基础、形式验证和交互式定理证明以及数学哲学和历史领域做出了贡献。
他认为这种转向可能改变数学的本质，依赖机器验证的证明可能减少了数学家对直观理解和洞察的重视，从而可能影响数学发现的过程和数学思想的发展。
纯数学中的抽象边界和规范驱动开发
数学家Johan Commelin和Adam Topaz探讨了抽象边界（Abstraction Boundaries）如何在交互式定理证明器的帮助下，帮助控制数学研究中的复杂性。
Johan Commelin 任荷兰乌得勒支大学助理教授，Adam Topaz 阿尔伯塔大学助理教授，两人研究兴趣的交点是代数几何，共同参与了液体张量试验。
△左：Johan Commelin，右：Adam Topaz
抽象边界是指在数学研究和定理证明过程中，将数学对象的实现细节与其外在属性和行为进行形式化区分的界限。这种界限使得数学家可以在不依赖具体实现细节的情况下，使用和推理这些数学对象。
抽象边界的概念在软件工程中非常常见，例如通过C语言的头文件、面向对象编程中的公共方法或者函数式编程中的 typeclass 来实现。
基于抽象边界的“规范驱动开发”方法，不仅降低了认知负荷，还促进了数学家之间的合作，使得工作可以轻松地分配给具有不同专长的合作者。
奇异新世界：定理证明助手和合成基础
数学家Michael Shulman认为，现有的计算机程序如 Lean 证明助手，能够验证数学证明的正确性，但它们专门的证明语言对许多数学家来说是一道门槛。
Michael Shulman 任圣地亚哥大学副教授，研究领域是范畴论和代数拓扑。
现有的计算机证明助手能够验证数学证明的正确性，但它们专门的证明语言对许多数学家来说是一道门槛。大模型有潜力降低这一门槛，使数学家能够以更熟悉的语言与证明助手进行交互。
这可能允许数学家使用由模型支持的证明助手探索根本上全新的数学领域，现有的证明助手已经在同伦类型论（homotopy type theory）等领域发挥了这一作用。
当前的人工智能可以做严肃的数学吗？
纽约大学计算机科学家Ernest Davis指出，当前 AI 在解决文字描述的数学问题上，无法可靠地结合基础数学和常识推理。
AI 通过三种主要方法尝试解决数学问题，但每种方法都有其优势和局限。
直接生成答案，适用于简单数学问题。 生成可执行代码，已在实践中取得成功。 翻译成逻辑规范，对于复杂问题仍存在挑战。他认为 AI 在解决数学奥林匹克问题时可能会依赖于训练数据中的模式，而不是真正理解问题的本质，这与人类通过直观和逻辑推理解决问题的方式有显著差异。
AI 真正解决数学问题需要三类知识：基础数学、语言理解和世界常识。例如理解硬币的价值和物理特性。常识在解决问题时经常被忽视，但实际上是至关重要的。
基准测试集是评估 AI 系统性能的重要工具，但它们可能无法全面覆盖 AI 的所有能力。
但同时他也指出，尽管 AI 在处理基础问题时存在局限，但这可能不会影响其进行高级数学研究的能力。
一方面，高级数学研究可能不需要与解决基础问题相同的常识推理能力。
另一方面，在棋类游戏上，即使 AI 无法理解棋局的基本概念，在棋局分析和策略制定上的能力能远超人类棋手。
数学家如何看待 AI？
关于自动化与数学研究的一些想法
菲尔兹奖得主Akshay Venkatesh探讨了数学自动化对数学研究的影响。他指出，机器可能大大增强数学解决问题的能力，但也会彻底改变数学的核心问题和价值观，使其难以被人类所认知。
他分析了当前数学界决定“什么是重要”的机制，如期刊、奖项、数学理论在应用领域得到认可、教育体系、聘用和资助过程等，都不足以解释数学界相对较高的共识水平。
他认为“证明”这种特殊的学术交流方式能引发一致同意，类似于自由市场中信息传播的机制。
AI 会导致当前数学界对“重要性”的判断发生剧变。
机器如何使数学更包容
数学家郑乐隽（Eugenia Cheng）认为，技术已经在改变人们研究数学的方式，可以利用这些技术使数学更加包容，而不是使数学家变得多余。
郑乐隽在谢菲尔德大学任教，除了范畴论研究和本科教学之外，她的目标是消除世界上的“数学恐惧症”。
她分析了技术如何影响数学教学、提出问题、协作、传播以及研究：
教学：标准的“粉笔和黑板”式讲授变得没有必要，她开始采用交互性更强的教学方式。同时对于学生来说，记忆现在已经无关紧要，应当将大脑留给更有趣的事情 提出问题：技术使得任何人都可以在网上提问并获得答复，但继承和放大了数学界的精英主义和竞争性。 协作：技术大大便利了远程协作，使地理位置不再是障碍。电子白板等工具也大大增强了协作的便利性。 传播：互联网使论文传播变得普及，不再局限于有限的纸质期刊。这让论文发表过程更加公开透明，论文质量而非发表渠道成为关键。 研究：通过智能手机可以随时随地展开研究，不受地点限制。搜索引擎等也让她不必记住所有事实，可以随时查阅。总的来说，郑乐隽认为技术可以使数学变得更加包容，只要数学家善用这些技术，而不是固步自封。
同时她也提出，如果最终机器能做得比人类更好，那很好，她将乐意退出数学领域去弹钢琴。
机器时代下的证明
数论学家Andrew Granville关注证明的本质以及计算机证明与人类证明之间的关系。
他认为，纯数学中的“客观性”并非如我们所想那样牢不可破。
定义和概念的困难：现代数学中很多概念没有单一明确的定义，存在多种可能的定义和阐释。这就难以谈“客观”。 公理系统的局限性：根据哥德尔不完备性定理，即使采用一致的公理系统，也无法证明所有关于整数的正确语句。这说明“客观的”数学基础是有局限性的。 历史演变的影响：不同时代数学家对“数学证明”的理解和标准有所不同，这体现了客观性标准的变迁。他探讨了计算机自动证明可能同时带来的挑战和机遇。计算机证明可以帮助确认人类直观证明的正确性，提高可信度。但计算机证明可能会取代人类，成为“黑箱”证明。但这种证明可能缺乏人类应有的可理解性和适应性。
Granville 希望未来的计算机证明能够吸收人类证明的优点，在形式化的基础上保持足够的灵活性和易理解性。
自动化迫使数学家反思自己的价值观
哥伦比亚大学数学家Michael Harris强调数学需要吸收其他学科、尤其是人文社科的经验。
他建议经常反思学科的价值追求和物质基础，有助于数学家在面对自动化等挑战时，更好地捍卫数学的核心价值。
此外，他还警示数学界不应被科技公司主导的议程所绑架，科技公司的价值取向与数学家的价值取向并不完全一致，数学家应保持独立思考的勇气，而不是被动接受来自产业的价值导向。
更多精彩内容 7 月发布
特刊的第二部分将于 2024 年 7 月发布，内容将包括：
自动化与哲学：形式化所引发的许多问题并不新鲜。McLarty 的文章描述，庞加莱在一个多世纪前就在讨论“推理机器”。庞加莱已经关注到形式化证明与数学实践之间的关系，这一主题在 de Toffolli 的文章中得到了进一步的探讨。
技术改变思维DeDeo 的文章检验了自动证明对数学家认知过程的潜在影响。
深度学习与数学的互动Bengio 和 Malkin 的文章考虑了进行数学研究对机器学习带来的特定挑战。Fraser 和 Poggio 的文章则提出了与深度学习数学基础相关的问题。
敬请期待～
期刊地址：
https://www.ams.org/journals/bull/2024-61-02/
参考链接：
