在未来，在我们最引以为傲的纯数学和理论物理领域，人类会不会也被AI所取代？在过去几年里，这个看似科幻的问题比以往任何时候都更加接近现实。和基于经验总结的科学不同，数学需要严格的定义、推导和证明。但在过去五年，在纯数学和理论物理领域，通过人工智能算法助力甚至替代人类部分研究工作的情况出现了急剧增长。这看起来有些反直觉。在近期发表于 Nature Reviews Physics 的文章中，伦敦数学科学研究所院士何杨辉提出了三种数学和理论物理发现的方法：“自上而下”、“自下而上”和“元数学”。作者认为，虽然在理论科学领域人类不会被AI系统取代，但人类专业知识与AI算法的结合将成为理论研究不可或缺的一部分，我们需要AI来引导和增强人类的直觉，找到新的洞察力、猜想和推导证明的策略。在未来，数学和理论科学研究将融合三种运用人工智能的方式：自下而上的自动定理证明，自上而下的机器辅助人类直觉，基于元数学的大语言模型。
关键词：AI for Math，人工智能，自动定理证明，大语言模型，元数学
何杨辉 | 作者
隽山 | 编译
董佳阳 | 审校
论文题目：AI-driven research in pure mathematics and theoretical physics
论文链接：https://www.nature.com/articles/s42254-024-00740-1
2.1 自下而上的数学（Bottom-up mathematics）
2.2 元数学（Meta-mathematics）
2.3 自上而下的数学（Top-down mathematics）
3. Brich 测试：自动性、可解释性、非平凡性
在过去五年里，人工智能（AI）在纯数学和理论物理学的研究中取得了令人瞩目的进展。这种进步的方式与 AI 在过去十年中改变人们日常生活的方式大相径庭。本文将用“理论科学”一词来涵盖纯数学以及利用数学发展和检验理论和假设的过程，这包括了理论物理学。文章遵循英国学术界的习惯，将理论物理学和理论计算机科学视作数学的分支。
在许多实际应用中，任务的执行往往依赖于所谓的“黑箱”操作：通过不断试错来学习，并在允许的误差范围内完成任务。比如，医生的首要任务是治愈患者，而对于疾病机制的深入了解则是次要的。深度神经网络擅长的，正是这种基于大量统计样本的黑箱机器学习。然而，对于追求深入理解和善于提出质疑的科学家，尤其是如果他们从事理论科学研究的话，这种方法并不足够。
虽然在 1990 年代，CERN 的实验物理学家在寻找新粒子时就开始使用 AI [1]，但机器学习技术直到 2017-2018 年才在理论物理学和纯数学中崭露头角[2-6]。对可解释性和可理解性（interpretability and explicability）的需求可能是 AI 在理论科学领域比其他科学领域更晚起步的原因。不过，这个领域正在迅速赶上。在理论物理学中，AI 驱动的研究包括了从弦理论中的粒子现象学到建立场论和深度学习之间的联系[7]，再到理论宇宙学、量子场论[8]以及揭示基本对称性[9]的研究。同样，在纯数学领域，AI 的应用也涵盖了代数几何、代数结构与表示理论、符号代数与计算、微分与度量几何、数论、图论与组合数学，以及纽结理论等。
总的来说，人们对于 AI 技术在社会中的角色持有既乐观又焦虑的复杂态度。本文旨在概述和讨论近年来在理论科学中 AI 应用的进步，并强调其关注点和局限性。我们希望人们能够理性看待 AI，既不过分狂热，也不无端恐惧，并相信数学科学未来的发展将是人类与 AI 之间不可避免且希望是和谐的合作。
要回答什么是人工智能驱动或人工智能辅助的理论研究，我们首先需要提出一个更基本的问题：数学家是如何进行数学研究的？这里不打算深入数学哲学或科学哲学的讨论，而是想采取一种实用主义的方法来解决问题。之前的一篇综述中[10]探讨了机器学习如何从两个相反的方向帮助揭示数学结构。现在，随着大型语言模型（Large Language Models，LLMs）的发展，我们认为引入第三个研究方向是恰当的。这三个方向在某种程度上呼应了上世纪初数学领域的三大哲学流派：形式主义、逻辑主义和直觉主义。
我们接下来将数学和理论科学的方法分为以下几类：
关于上面三个术语的使用，我们借用了物理学中的自上而下和自下而上的术语，其中自下而上的模型构建起点是低能量尺度，而自上而下的起点是高能量尺度。在后面的内容中，我们将详细讨论 AI 如何成为这些方法的工具。
2.1 自下而上的数学（Bottom-up mathematics）
在 20 世纪 20 年代初，数学家希尔伯特（Hilbert）提出了一个雄心勃勃的计划，旨在从最基本的公理出发，构建起整个数学体系的真理。然而，大约十年后，哥德尔（Gödel）、丘奇（Church）和图灵（Turing）提出的不可判定性和不完备性定理给了这个计划沉重的打击。这些定理揭示了一个深刻的事实：在任何数学体系中，总有一些陈述是无法被证明其真假的。尽管如此，那些可以被判定且具有研究价值的数学陈述是如此之多，足以让我们先集中精力去探索它们。因此，尽管理论上我们无法从基础出发构建所有的数学陈述，但数学家们从未放弃过对各种命题证明的追求。这种努力最终催生了现代自动定理证明程序（Automated Theorem Proving Programme，ATP）的发展，这是对怀特海（Alfred North Whitehead）和罗素（Bertrand Russell）在数学基础工作的一种现代回应。
到了 20 世纪下半叶，人们逐渐意识到，没有计算机的帮助，许多数学的基本结果的证明几乎是不可能的。从简化为大量暴力计算的问题（比如四色定理）到那些复杂到需要超过人类一生时间去完成的问题（比如简单有限群的分类），计算机在数学证明中的作用越来越重要。这种对机器的依赖促使像陶哲轩这样杰出的数学家在国际数学家大会上呼吁思考数学的未来。虽然第一个基于机器的证明帮助软件[11]在 20 世纪 70 年代就出现了，但像 Isabelle/HOL[12]、Coq[13]、Agda[14] 和 Lean[15] 这样的软件在这个世纪推动了自动定理证明的发展。其中一个引人注目的项目是 Xena 项目，它的目标是将本科生水平的所有数学知识（包括每一个陈述和证明的每一步）都形式化到 Lean 这个系统中。去年，Lean 的 MathLib 库还被用来证明了多项式 Freiman-Ruzsa 猜想。尽管将所有当代数学知识以 Coq 或 Lean 的格式存储的数据库构建工作还远未完成，但这样的数学数据库一旦建成，将能够通过数据挖掘发现新的理论，这将是我们未来发展自动定理证明的思考方向。
2.2 元数学（Meta-mathematics）
数学被视为一种语言，这一观点从《数学原理》延续到现代计算机科学。哲学家维特根斯坦（Ludwig Wittgenstein）启发我们将数学公式和证明看作符号序列。自然语言处理（Natural Language Processing，NLP）基于图灵测试的理念，已经发展到 LLMs 时代，这些模型能够模仿人类交流，但并不真正理解内容。也就是说，LLMs 并没有对底层材料的“理解”。这些模型仅仅基于大量的统计样本语料库，将单词以正确的顺序组合在一起。抛开“理解”的哲学含义（这也是我们选择将这个方向称为“元数学”的原因），很明显 LLMs 在模仿人类沟通方面具有变革性。
在数学和理论物理研究中，LLMs 的应用展示了它们能够识别科学领域内不同子领域之间的差异性。Word2Vec 神经网络可能是最基本的 LLMs 技术，在应用于 arXiv 和 viXra 两种预印本服务器的研究中，Word2Vec 展示了其在理解科学文献领域和区分主流与非主流科学思想方面的潜力。通过分析 arXiv 预印本服务器的标题，Word2Vec 可以区分出理论物理的不同方向。由于 viXra 包含了一些未被主流科学接受的观点和理论，Word2Vec 在 viXra 中的作用不那么显著。这表明主流科学的语法比边缘科学的语法在标题层面上更为自洽。
如今，Word2Vec 已经被其他深度学习架构（如 transformers）所取代，LLMs 在数学领域的应用正在蓬勃发展。值得注意的是，DeepMind 的 AlphaGeo 最近能够为欧几里得几何中的奥林匹克级别问题生成正确的、人类可理解的证明，尽管这一过程中仍部分依赖于传统搜索方法。
这些进步表明，如果存在一个完整的、精确格式的语言数据库，比如“Lean”，用于所有当代数学，那么LLMs 对这一庞大数据集的方法应该能够产生新的数学。
2.3 自上而下的数学（Top-down mathematics）
我们讨论的很多内容都涉及到构建正确的数学陈述。但实际上，很多时候我们并不清楚应该证明什么。实际上，数学家是如何工作的呢？数学论文往往是倒着写的。日复一日，数学家在纸上涂鸦，尝试各种想法、错误和表达，直到找到一些有意义的结果，然后再回过头来，用定义、定理和推导来正式化这些结果，从而得出逻辑上的结论。因此，尽管数学和理论物理的期刊论文看起来是自下而上的，但发现过程恰恰相反，这种双重性被称为“综合与分析”。
历史上，一些最伟大的理论发现就是这样产生的。牛顿（Isaac Newton）和欧拉（Leonhard Euler）在数学解析和收敛的适当概念出现前的几个世纪，就自由地操纵着各种微积分表达式；伽罗瓦（Evariste Galois ）在群（groups）和域（fields）的定义出现之前，通过观察置换群（permutation groups） 的结构展示了五次方程无解的问题。在物理学中，理论家们自由地操纵费曼积分，以获得与实验惊人一致的结果，尽管量子场论的数学严格表述尚不完善。
近年来，人们越来越担心 AI 可能会取代人类数学家。有些人将人类数学家视为自下而上的逻辑理论机器，从定义出发构建证明和推导。但实际上，真正的数学研究是基于灵感、直觉和经验的结合。与学院派严格的自下而上叙述相比，我们称这种方法为基于模糊美学的自上而下。当然，最终所有的陈述都必须是严格的，任何模糊和不准确都必须被提炼出来。
也许与普遍观念相反，即使是最纯粹的数学发现也离不开数据。这些数据不是带有误差和方差的实验数据，而是分类和计算的结果，例如有限群（finite groups）的特征表。这些“纯数据”是精确的，没有统计误差，并且能够揭示底层理论。正如数学家阿诺德（Vladimir Arnold）所说，“数学是物理学中实验成本较低的部分”。
面对寻找质数模式的古老问题，16 岁的高斯（Carl Friedrich Gauss）定义了质数计数函数（prime counting function），该函数给出了不超过正实数 x 的质数数量。他参考了当时的表格，并手工计算了数万个更多的数字，简单地绘制了 π(x)。高斯猜想 π(x) 与 x/ln(x) 大致成比例。这一深刻的观察直到柯西（Augustin-Louis Cauchy）和黎曼（Bernhard Riemann）建立复分析之后，才由阿达玛（Jacques Hadamard）和普桑（Charles Jean de la Vallée Poussin）在 1896 年证明，现在被称为质数定理，是数学中最重要的结果之一。
在 20 世纪，数学家伯奇（Bryan John Birch）和斯温纳顿-戴尔（Peter Swinnerton-Dyerplotted）使用 1960 年代的早期计算机，绘制了椭圆曲线的秩和其他数量，并猜想曲线的 L 函数 L(s）在 s 趋向 1 时消失的阶数等于秩。这一观察被称为伯奇-斯温纳顿-戴尔猜想，是一个千年奖问题，对现代数学至关重要。
以上只是无数例子中的两个，说明通过实验纯数据可以得出深刻的结果。它们强调了猜想的重要性。在理论研究中，找到有趣的问题至关重要，而这个过程往往由几乎无法定义的直觉过程引导。哈代（Godfrey Harold Hardy）对数学的定义是简洁的：“数学家、画家或诗人，都是模式的创造者”。大多数研究现实世界数据的科学家会首先将问题提炼成数学表示。然后，它再次成为从图表和图形到正式符号的数学模式识别游戏。但有一件事是 AI 系统比人类做得更好的，那就是模式识别，特别是在数据维度很高的情况下。这一点在下面的简单实验中得到了体现。
让我们进行以下简单实验。首先，给出序列0， 0， 1， 0， 0， 1， 0， 0， 1， 0， 0， 1， 0， 0， 1， 0， 0， 1，当被问及下一个数字是什么时，任何人都会立即说 0。解释为什么的一种方式是，这个序列显示了 n 是否能被 3 整除，对于正整数 n。接下来，试试 {1， 1， 1， 0， 1， 1， 1， 0， 0，1， 1， 0， 1， 1， 1， 0， 1， 0， 1， 0， 1， 1， 1， 0， 0， 1， 0， 0， 1， 1， 1， 0， 1， 1， 1， 0， 1， 1， 1， 0， 1， 1， 1， 0， 0， 1， 1， 0， 0， 0， 1}。一个有灵感的人可能在一些实验后得出下一个数字是 1；这是 PrimeQ 序列，即第 n 个正整数是否为质数。最后，试试 {1， 1， 1， 0， 1， 1， 1， 0， 0，1， 1， 0， 1， 1， 1， 0， 1， 0， 1， 0， 1， 1， 1， 0， 0， 1， 0， 0， 1， 1， 1， 0， 1， 1， 1， 0， 1， 1， 1， 0， 1， 1， 1， 0， 0， 1， 1， 0， 0， 0， 1}。这是第 n 个正整数具有偶数（0）还是奇数（1）的质因数数量（考虑重复）的序列，是所谓的刘维尔-拉姆达（Liouville lambda） 函数的移位版本。揭示 lambda 函数中的模式将对数学产生难以置信的影响：黎曼猜想（Riemann hypothesis）有等价表述，以这个序列为依据。
如果将这个序列交给 AI 系统来解决（例如，使用监督机器学习算法）会怎么样？为了建立一个合理的训练集，可以选择以下表示方法（实际上，表示方法的选择非常重要）。取上述无限序列 {ai}i=1,2,3中的一个，以及长度为 N 的滑动窗口。换句话说，考虑一组序列{ai}i=1,2,…,N, {ai}i=2,3,…,N+1,…, {ai}i=k,k+1,…,N+k-1}，对于某个 k。在这里，k 将被选得足够大（比如说 100,000）以创建一个足够大的数据集，而 N 将被选得足够大（比如说 100）以提供足够的特征。（毕竟，数学数据是便宜的。）然后，可以将每个有限子序列视为
中的一个单独向量，并用窗口外的下一个数字对其进行标记：
注意，已经谨慎地选择了序列，将所有内容标准化为维度为 N 的二进制向量的二进制分类问题。问题是：在看过 k 个标记样本后，机器学习算法在 k’ 个未见向量上的预测效果如何？这个熟悉的监督机器学习范式可以与人类在同一任务上的表现进行比较。
人们很容易就能验证，如果使用一些基础的机器学习算法，比如决策树、支持向量机，或者简单前馈神经网络，都可以处理上面三个数据序列。对于第一个序列，任何机器学习算法都能很快达到 100%的准确率。对于第二个序列，准确率约为 80%（在这种情况下，由于质数的稀有性——大约是 x/ln(x)，由于质数定理——窗口大小需要相应调整），而对于第三个序列，很难找到任何 AI 算法能够超过 50%的准确率。这意味着第一个序列，对于人类来说是一个简单问题，对于 AI 系统来说也是简单的；对于第二个序列，AI 方法可能正在找到某种版本的埃拉托斯特尼筛法（Sieve of Eratosthenes）来检查 PrimeQ；而对于最后一个序列，AI 系统并没有比随机猜测更好。当然，如果有人找到了一个算法能够做到这一点，那么人们可能已经在寻找黎曼猜想的新方法上取得了进展。
引言中引用的许多论文都使用了前一段中类似的想法，但应用在更复杂的情况上。实际上，有什么（可计算的）数学，从图灵机的意义上说，不落入上述三个序列方程的某种版本？我们可以通过将每个 N 向量包装成 m×n=N 矩阵，将其解释为一个像素化的图像，其中 1 是黑色，0 是白色，使这种情况更加可视化，更适合 AI。例如，假设 N=100，第二个序列的第一个向量可以被包装成一个 10×10 矩阵，连同一个标签 1（因为 101 是质数），随后进行了说明。作为一个更高级的例子，考虑计算代数几何中流形的拓扑不变量（这涉及到高级计算）。然而，人们可以通过张量化流形作为代数簇的多度数信息，将流形表示为一个像素化的图像。以类似的方式，人们可以将任何数学计算重新构建为图像识别问题。从许多计算中学习并获得经验和直觉——正如数学家和理论家在他们的职业生涯中所做的——类似于训练一个神经网络。我们可以将这种范式大致总结为：自下而上的数学（和元数学）是语言处理，而自上而下的数学是图像处理。
3. Brich 测试：
自动性、可解释性、非平凡性
在自上而下的数学研究中，我们首先需要识别出问题所在，然后确定一个策略来解决这个问题。这两个步骤都依赖于丰富的经验和直觉。虽然大型语言模型，比如应用于数据库的 Lean 的 MathLib，在这方面已经取得了一些初步的进展，但在提出猜想这一环节，我们还有很长的路要走。历史上，像高斯和 Birch-Swinnerton-Dyer 这样的数学家们以其卓越的直觉提出了重要的猜想。现在的问题是，AI 是否能够帮助我们区分哪些猜想是有价值的，哪些是无用的？我们能否从数学数据中发现一些模式，引导我们走向有趣而非平凡的数学发现？这些问题已经引起了人工智能领域内一些系统的思考。
2023 年，文章作者参与协助组织了一个在剑桥举行的为期六个月的工作会议（https://www.newton.ac.uk/event/blh/），期间参与者们尝试为人工智能驱动的理论发现，尤其是人工智能辅助的猜想提出、制定一些标准。这些标准包括：
这些标准是由 Birch 的一次演讲启发的，因此被称为 Birch 测试。这些标准非常严格，到目前为止，还没有任何一个人工智能辅助的理论发现能够完全满足这三个条件。下面我们通过一些例子来看看在这些标准下，人工智能在哪些方面做得好，哪些方面还有待提高。
例如，早期通过深度学习来获取拓扑不变量的实验[16]，这些实验的准确率已经提高到了 99.9%以上，这暗示了在代数几何中可能存在一些我们尚未知晓的结构，这些结构能够帮助我们进行计算，而不必依赖于那些标准且计算成本高昂的方法。但这些结果也暴露了深度神经网络方法的一个典型问题：我们无法从中提取出一个可解释的公式。因此，它们没有通过 Birch 测试的可解释性条件。另一个例子是，支持向量机通过绘制 Cayley 乘法表找到了简单和非简单有限群之间的分离[17]，但分离的超曲面非常复杂，并且随着更多群样本的添加而进一步变形，因此可解释性条件仍未满足。通过显著性分析发现的结不变量关系和解开极其复杂的结所需的 Reidemeister 移动，虽然新颖、有趣且精确，但要么已经被证明，要么在该领域没有足够的影响力，因此它们没有通过非平凡性条件。类似地，拉马努金机器（Ramanujan machine）发现的连分数恒等式或 AI Feynman 发现的物理守恒定律也属于这一类。即使在实际任务中，比如 DeepMind 发现的更快的矩阵乘法算法，也很快被人类研究人员设计的算法超越。
在所有 AI 引导的理论发现中，最接近满足这三个标准的是数论中的 murmuration 猜想。这种方法满足了可解释性和非平凡性，但没有满足自动性，因为人类研究人员在过程中进行了干预。他们对 AI 在 Birch-Swinnerton-Dyer 猜想背景下区分椭圆曲线的等级做得如此之好感到非常惊讶。
从事理论研究的人们可以放心，至少在可预见的未来，他们的工作不会被取代。人类还没有建立起一个全面的、自下而上的数学数据库，覆盖所有的数学领域。即使有了这样的数据库，大型语言模型在面对证明策略的巨大搜索空间时也会遇到挑战。再加上自上而下数学中 Birch 测试的严格标准，我们离完全自动化的理论发现还很远。不过，人工智能已经开始，并且将继续在与人类数学家和理论科学家的合作中扮演关键角色。在我们讨论的三个方向上，我们既有紧迫的任务，也有长远的目标。
-
对于自下而上的数学，Wiles 的证明已经被正式化了，下一步应该是开始正式化并交叉检验有限单群的分类定理，这是数学中一个基础但从未被严格审查过的定理（整个证明长达约 10000 页）。由于目前 Lean 在算术几何方面的覆盖比其他数学分支更多，这项工作可能需要好几年的时间。
-
对于元数学，科学界应该共同努力，利用大型语言模型挖掘 arXiv 上的数学知识。虽然已经有类似的尝试在数学物理领域进行，arXiv 也有自己的内部语言模型，比如自动分类提交。现在，Llama 已经将其大型语言模型扩展到了 arXiv。使用 Llama 提取新的数学思想将是非常棒的。不过，元数学也是充满挑战的。比如，你可以让 ChatGPT 求导一个函数，它会非常准确地完成，而不需要进行任何数学计算。但是，当面对一个看似简单得多的问题，比如“找到 7/11 的小数展开中的第 20 位数字”，它就会彻底失败，不会比随机猜测表现得更好。这个问题只能通过实际进行长除法来解决。即使是为“数学的大型语言模型”投入更多的计算资源，也不能解决这个问题；我们需要知道何时调用真正的数学软件，正如 WolframAlpha 与 ChatGPT 结合时开始做的那样。
-
对于自上而下的数学，我们正接近通过 Birch 测试的阶段。在未来几年，我们可以期待完全自动化地生成非平凡的猜想。挑战在于如何建立一个系统来选择这些猜想，并引导人类数学家。这与数学家 Jordan Ellenberg 的观点不谋而合：“有些人想象一个计算机给我们所有答案（在数学中）。我的梦想更大。我希望它们能提出好问题。”
回顾历史，在十八和十九世纪，数学巨匠高斯凭借其超凡的直觉和洞察力，就能够发现素数定理等深刻的理论科学成果。到了二十世纪，Birch 和 Swinnerton-Dyer 需要计算机实验与他们的洞察力相结合，才能提出猜想。然而，在二十一世纪，仅凭个人直觉和简单的计算机实验已经不足以应对日益复杂的科学问题。因此，我们需要AI来引导和增强人类的直觉，找到新的洞察力、猜想和推导证明的策略，AI已成为推动科学发展的关键力量。
展望未来，数学和理论科学的研究将融合以下三种运用人工智能的方式：
• 首先是自下而上的自动定理证明，这将依赖于AI的强大计算能力来验证和推导数学命题；
• 其次是自上而下的机器辅助的人类直觉，AI将帮助研究者识别模式、提出猜想，并在复杂的数据中发现潜在的联系；
• 最后是基于元数学的大语言模型，这些模型将整合广泛的数学知识，预测新的研究方向，并辅助证明过程。
这种协同工作模式将最大化地发挥AI的计算能力和人类的创造性思维，共同开启理论科学研究的新篇章。通过这种合作，我们不仅能够解决当今世界面临的复杂问题，还能够探索未知的科学边界，推动人类知识的进步。
[1] Perret-Gallix, D. & Wójcik, W. New computing techniquesin physics research. In Proc. 1st Int. Workshop on Software Engineering, Artificial Intelligence and Expert Systemsin High-energy and Nuclear Physics (CNRS, 1990).
[2] He, Y.-H. Deep-learning the landscape. Phys. Lett. B774, 564–568 (2017).
[3] Carifio, J., Halverson, J., Krioukov, D. & Nelson, B. D. Machine learning in the string landscape. J. High Energy Phys.09, 157 (2017).
[4] Krefl, D. & Seong, R.-K. Machine learning of Calabi–Yau volumes. Phys. Rev. D96, 066014 (2017).
[5] Ruehle, F. Evolving neural networks with genetic algorithms to study the string landscape. J. High Energy Phys.08, 038 (2017).
[6] Liu, J. Artificial neural network in cosmic landscape. J. High Energy Phys.12, 149 (2017).
[7] Demirtas, M., Long, C., McAllister, L. & Stillman, M. The Kreuzer–Skarke axiverse. J. High Energy Phys.04, 138 (2020).
[8] Chen,H.-Y., He, Y.-H., Lal, S. & M ajumder, S. Machine learning lie structures & applications to physics. Phys. Lett. B817, 136297 (2021).
[9] Lemos, P., Jefrey, N., Cranmer, M., Ho, S. & Battaglia, P. Rediscovering orbital mechanics with machine learning. Mach. Learn. Sci. Technol.4, 045002 (2023).
[10] He, Y.-H. Machine-learning mathematical structures. Preprint at https://arxiv.org/abs/2101.06317 (2021).
[11] De Bruijn, N. G.in Studiesin Logic and the Foundations of Mathematics Vol. 133, 73–100 (Elsevier, 1994).
[12] Nipkow, T. et al. (eds) Isabelle/HOL: A Proof Assistant for Higher-order Logic Vol. 2283 (Springer, 2002).
[13] Bertot, Y. & Castéran, P. Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions(Springer, 2004).
[14] Wadler, P. Programming language foundationsin Agda. In Formal Methods: Foundations and Applications (SBMF 2018) (eds Massoni, T. & Mousavi, M.) 56–73 (Springer, 2018).
[15] De Moura, L., Kong, S., Avigad, J., van Doorn, F. & von Raumer, J.in Automated Deduction-CADE-25: 25th International Conference on Automated Deduction, Berlin, Germany, August1–7,2015, Proceedings (eds Felty, A. P. & Middeldorp, A.) 378–388(Springer, 2015).
[16] He, Y.-H. The Calabi–Yau Landscape: From Geometry, to Physics, to Machine Learning (Springer Cham, 2018).
[17]. He, Y.-H. & Kim, M. Learning algebraic structures: preliminaryinvestigations. Preprint at https://arxiv.org/abs/1905.02263 (2019).
数十年来，人工智能的理论发展和技术实践一直与科学探索相伴而生，尤其在以大模型为代表的人工智能技术应用集中爆发的当下，人工智能正在加速物理、化学、生物等基础科学的革新，而这些学科也在反过来启发人工智能技术创新。在此过程中，数学作为兼具理论属性与工具属性的重要基础学科，与人工智能关系甚密，相辅相成。一方面，人工智能在解决数学领域的诸多工程问题、理论问题乃至圣杯难题上屡创记录。另一方面，数学持续为人工智能构筑理论基石并拓展其未来空间。这两个关键领域的交叉融合，正在揭开下个时代的科学之幕。
为了探索数学与人工智能深度融合的可能性，集智俱乐部联合同济大学特聘研究员陈小杨、清华大学交叉信息学院助理教授袁洋、南洋理工大学副教授夏克林三位老师，共同发起“人工智能与数学”读书会，希望从 AI for Math，Math for AI 两个方面深入探讨人工智能与数学的密切联系。读书会已完结，现在报名可加入社群并解锁回放视频权限。
详情请见：
人工智能与数学读书会启动：AI for Math，Math for AI
6. 加入集智，一起复杂！
点击“阅读原文”，报名读书会
