陶哲轩转发、菲尔兹奖得主领衔：AI正在颠覆数学家的工作方式
陶哲轩点赞转发，《美国数学学会通报》用一整期特刊介绍了AI给数学带来的改变。
作者阵容非常豪华，包括菲尔兹奖得主Akshay Venkatesh、华裔数学家郑乐隽、计算机科学家Ernest Davis等多位知名学者。
其中郑乐隽表示，如果最终机器能做得比人类更好，那很好，她将乐意退出数学领域去弹钢琴。
他们提出的观点包括：
在开篇，编委会写道：
现在，是数学家们了解并推动这场辩论，并决定学科未来方向的时候了。
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/
参考链接：[1]https://mathstodon.xyz/@tao/112221953164171331