http://www.youtube.com/watch?v=tfr8VPGLtrc
在这期 SAIR Podcast 访谈视频 David Roe: The IGP24 Competition, the LMFDB, and Scientific Computing 中，麻省理工学院（MIT）的首席研究科学家 David Roe 深入探讨了计算数论、数学数据库、逆伽罗瓦问题竞赛（IGP24）以及人工智能对科学计算与数学研究带来的改变。
1. 嘉宾介绍与数学数据库（LMFDB）的价值
- 个人背景 [00:06]：David Roe 是开源数学软件 SageMath 的早期核心贡献者之一，近 8 年来担任 LMFDB（L-函数与模形式数据库）的管理编辑。
- 数学数据库的作用 [01:03]：传统的计算机代数系统用于“实时计算”，而 LMFDB 则是将预先计算好的海量深奥数学对象（如代数曲线、模形式、代数数域）储存并提供可搜索接口。这让抽象的朗兰兹纲领等理论有了具体实例，方便数学家验证猜想或寻找反例。
2. 逆伽罗瓦问题（IGP）与 IGP24 竞赛
- 什么是逆伽罗瓦问题 [08:13]：给定任意有限群，是否存在以该群为根对称群（伽罗瓦群）的多项式？对于可解群（Solvable groups），理论上已证实存在；但对于不可解群，一般性结论依然悬而未决。
- 为何选择 24 次多项式 [12:56]：24 是一个高度合成数，对应的 24 次传递置换群共有 25,000 个，计算极其复杂。以往研究大多停留在 23 次以下。
- 竞赛取得的突破 [15:21]：
- 竞赛前，LMFDB 数据库中仅包含 286 个 24 次群的多项式。
竞赛仅开展一个月，参赛者已找到了 24,737 个群的具体多项式，未解决的只剩 263 个。结合 Shafarevich 定理，弱形式下的 24 次逆伽罗瓦问题已基本得到解决。
积分与防混评分机制 [04:59]：竞赛通过 $1/2^k$（$k$ 为找到该结果的人数）的动态权重评分，激励大家去寻找没有人发现过的全新群结构。
3. AI 在数学搜索与系统验证中的应用
- 解决 AI 信任问题 [20:18]：IGP24 属于“搜索与验证”类问题。参赛者可以用 AI 生成候选多项式，随后用计算机代数系统（如 Magma）验证其伽罗瓦群。我们不需要信任 AI 的推导，只需信任代数系统的验证结果即可。
- Lean 证明助手与 LLM 结合 [38:30]：对于无法用常规程序验证的纯理论证明，AI（如 Claude/GPT）负责编写 Lean 形式化证明代码，Lean 的内核则负责校验并反馈错误。这种交互循环将极大地推动数学证明形式化的进程。
- 利用 AI 进行开源代码维护 [43:58]：David Roe 分享了他尝试用 AI 在一天内批量修复了 LMFDB 项目的 40 个 GitHub 悬而未决的 Issue，并认为 AI 在代码跨语言移植（如 Magma 移植到 Sage）上有巨大的潜力。
Top comments (0)