麻省理工学院数学系的David Roe '06和Andrew Sutherland '90, 博士'07是Renaissance Philanthropy和XTX Markets颁发的首批“AI助力数学（AI for Math）”奖金的获得者之一。

另外四位麻省理工校友——Anshula Gandhi '19、Viktor Kunčak SM '01, 博士'07；Gireeja Ranade '07；以及Damiano Testa 博士'05——也因各自不同的项目而获奖。

首批29个获奖项目将支持在大学和组织中工作的数学家和研究人员，他们致力于开发人工智能系统，以帮助在多个关键任务中推进数学发现和研究。

Roe和Sutherland将与东安格利亚大学的Chris Birkbeck合作，利用他们的奖金来促进自动定理证明的发展，方法是在L函数与模形式数据库（LMFDB）和Lean4数学库（mathlib）之间建立连接。

Sutherland表示：“自动定理证明器在技术上非常复杂，但其开发资源却严重不足。”随着大型语言模型（LLMs）等人工智能技术的发展，这些形式化工具的进入门槛正在迅速降低，使得形式化验证框架可以被在职数学家所使用。

Mathlib是一个庞大、由社区驱动的、为Lean定理证明器服务的数学库。Lean是一个形式系统，用于验证证明中每一步的正确性。Mathlib目前包含大约10⁵个数学结果（如引理、命题和定理）。LMFDB是一个大规模的协作在线资源，是现代数论的“百科全书”，包含超过10⁹个具体陈述。Sutherland和Roe是LMFDB的管理编辑。

Roe和Sutherland的奖金将用于一个旨在增强这两个系统的项目：将LMFDB的结果作为尚未被正式证明的断言提供给mathlib，并为LMFDB中存储的数值数据提供精确的形式化定义。这种连接将使人类数学家和AI代理都能受益，并为将其他数学数据库连接到形式定理证明系统提供一个框架。

自动化数学发现和证明的主要障碍在于：形式化数学知识的有限性、形式化复杂结果的高昂成本，以及计算可访问性与形式化可行性之间的差距。

为应对这些障碍，研究人员将利用这笔资金来构建从mathlib访问LMFDB的工具，使一个大型的非形式化数学知识数据库可供形式化证明系统使用。这种方法使证明助手能够在不需要预先形式化整个LMFDB语料库的情况下，识别出形式化的具体目标。

Roe说：“将大量非形式化的数论事实数据库在mathlib中可用，将为数学发现提供一种强大的技术，因为代理在寻找定理或证明时可能考虑的事实集合，比最终证明定理所需的需要形式化的事实集合要大得多。”

研究人员指出，证明数学知识前沿的新定理通常涉及依赖于非平凡计算的步骤。例如，安德鲁·怀尔斯（Andrew Wiles）对费马大定理的证明在其关键一步中使用了所谓的“3-5技巧”。

Sutherland解释说：“这个技巧依赖于模曲线 X₀(15) 只有有限多个有理点，并且没有一个有理点对应于半稳定椭圆曲线这一事实。”“这个事实在怀尔斯的工作之前就已经广为人知，并且可以使用现代计算机代数系统中可用的计算工具轻松验证，但它不是仅靠纸笔就能现实地证明的，也不一定容易形式化。”

虽然形式定理证明器正在与计算机代数系统连接以实现更高效的验证，但利用现有数学数据库中的计算输出来连接具有其他几项好处。

使用存储的结果可以利用创建LMFDB时已花费的数千CPU年计算时间，节省了需要重复这些计算的成本。拥有预先计算好的信息也可以使得在不知道搜索范围多广的情况下搜索实例或反例成为可能。此外，数学数据库是经过精心策划的存储库，而不仅仅是事实的随机集合。

Sutherland说：“数论学家强调导子（conductor）在椭圆曲线数据库中的作用，这一事实已被证明对于使用机器学习工具取得的一项值得注意的数学发现——‘群聚现象’（murmurations）——至关重要。”

Roe表示：“我们的下一步是建立团队，与LMFDB和mathlib社区合作，开始形式化支撑LMFDB中椭圆曲线、数域和模形式部分的定义，并实现在mathlib内部运行LMFDB搜索的可能性。如果麻省理工学院的学生有兴趣参与，请随时与我们联系！”