麻省理工学院（MIT）数学系研究人员大卫·罗（David Roe ’06）和安德鲁·萨瑟兰（Andrew Sutherland ’90, PhD ’07）成为首届“文艺复兴慈善基金会与XTX Markets人工智能助力数学”（AI for Math） grants的获奖者。此外，四位MIT校友——安舒拉·甘地（Anshula Gandhi ’19）、维克托·昆查克（Viktor Kunčak SM ’01, PhD ’07）、吉里贾·拉纳德（Gireeja Ranade ’07）和达米亚诺·特斯塔（Damiano Testa PhD ’05）也因各自项目获此殊荣。 此次共有29项获奖项目，旨在支持全球高校与研究机构开发人工智能系统，推动数学发现与研究。罗与萨瑟兰将与英国东安格利亚大学的克里斯·伯克贝克（Chris Birkbeck）合作，利用资助资金，连接“L-函数与模形式数据库”（LMFDB）与“Lean4数学库”（mathlib），以提升自动化定理证明能力。 mathlib是一个由社区维护的大型形式化数学库，用于Lean定理证明器，确保每一步证明的逻辑正确性。目前包含约10万项数学成果。而LMFDB作为现代数论的“百科全书”，收录超过10亿个具体数学陈述。萨瑟兰与罗均担任该数据库的联合主编。 他们计划开发工具，使mathlib能直接访问LMFDB，从而将大量尚未形式化的数学知识引入形式化系统。这一突破将使AI辅助证明系统能精准定位待证明目标，无需预先形式化全部数据库内容。 “在寻找定理或证明时，可能需要考虑的数学事实数量呈指数级增长，但最终真正需要形式化的部分却非常有限。”罗表示。借助AI技术，特别是大语言模型，形式化工具的使用门槛正迅速降低，使更多数学家能参与严谨证明。 该研究还将节省大量计算资源。LMFDB已积累数千CPU年计算成果，这些预计算结果可直接复用，避免重复劳动。同时，数据库内容经过专业筛选，非随机堆砌，其结构对发现具有重要意义。例如，数论学家强调“导子”在椭圆曲线数据库中的作用，这一特性已助力机器学习发现“murmurations”现象。 下一步，团队将组建核心团队，联动LMFDB与mathlib社区，逐步形式化椭圆曲线、数域与模形式等关键领域的定义，并实现从mathlib内直接调用LMFDB搜索功能。罗呼吁MIT学生积极参与：“如果你对这项工作感兴趣，欢迎联系！”