2025年数学AI人工智能再提速——文艺复兴慈善基金会揭晓首批1800万美元AI数学基金资助的29个项目（二）

★加星zzllrr小乐公众号数学科普不迷路！

接上文

本文介绍文艺复兴慈善基金会揭晓首批1800万美元AI数学基金资助的29个项目（二）[11 ~ 20]

作者：文艺复兴慈善基金官网（Renaissance Philanthropy）2025-9-17

译者：zzllrr小乐（数学科普公众号）2025-9-25

11、结构化动机证明数据库

项目简介

该项目旨在通过开发一个全面的动机证明数据库，清晰记录每个想法的起源，从而显著增强AI驱动的数学研究。通过实施“证明-发现步骤”作为Lean策略，团队将促进这些证明的形式化和识别，从而创建一个以Lean方式表达的并行数据库。这种创新方法有望促进数学领域AI模型的训练、评估和解释，为传统的定理-证明配对提供一种更适合实际数学任务的替代方案。该项目有望通过提供一个透明且结构化的框架来理解数学家的推理方式，从而显著提高AI在数学任务中的表现。

团队简介

蒂莫西·高尔斯（Timothy Gowers）

法兰西学院的组合数学教授，同时兼任剑桥大学数学系教授和三一学院研究员。在剑桥大学，他领导着一个自动定理证明小组，专注于理解人类数学家寻找证明的过程。他于1981年在国际数学奥林匹克竞赛（IMO）中获得满分，并于1998年因其在泛函分析和组合数学领域的杰出贡献荣获菲尔兹奖。他是牛津通识读本《数学：极简导论》Mathematics: A Very Short Introduction一书的作者，也是《普林斯顿数学指南》的主编。

阿南德·拉奥·塔迪帕特里（Anand Rao Tadipatri）

剑桥大学Timothy Gowers以人为本（中心）的自动定理证明研究小组的二年级博士生。他与研究小组的其他成员合作，开发了一个自动推广证明的程序，并在Lean上设计了一个适合证明发现的环境。他是Lean社区的成员，期待有一天交互式定理证明器能够成为数学家的主流，并积极协助证明发现过程。

安舒拉·甘地（Anshula Gandhi）

剑桥大学数学专业的博士生，专攻自动定理证明以及失败和泛化（推广）在数学研究中的作用。她的研究背景还涵盖结理论、机器人技术和计算天体物理学。

雅各布·洛德（Jacob Loader）

Jacob Loader在悉尼大学完成了数学和计算机科学的本科学位，随后在剑桥大学获得了数学硕士学位。他的研究涵盖了纯数学的多个领域，包括概率论、表示论和解析数论。他目前的研究方向是利用反例引导迭代法解决存在性问题，并通过Lean 4中的元编程来实现这些想法。

约万·格布沙伊德（Jovan Gerbscheid）

Jovan Gerbscheid完成了剑桥数学tripos学位考试，并在国际数学奥林匹克竞赛中获得了一枚金牌和两枚铜牌。他目前正在完成自动定理证明博士学位的第一年学习。他是Lean社区的活跃成员，专注于Lean元编程，最近还担任了mathlib的官方审阅者。

乔纳斯·拜耳（Jonas Bayer）

Jonas Bayer在不来梅雅各布大学获得数学学士学位。他目前是剑桥大学的博士生，研究自动定理证明。他因与马可·大卫（Marco David）合作在Isabelle中成功形式化戴维斯、普特南、罗宾逊和马蒂亚塞维奇提出的希尔伯特第十问题的解而闻名。

12、DEEPER——用于精确专家推理的深度探索引擎

项目简介

“DEEPER”（Deep Exploratory Engine for Precise Expert Reasoning）项目旨在通过整合先进的机器学习技术，为最先进的自动定理证明器 (ATP，automatic theorem provers) 提供指导，从而彻底革新自动定理证明。通过结合神经学习和符号学习方法，该团队致力于增强证明指导，特别是针对高阶和依赖类型演算的证明指导，这些演算对于形式化复杂数学问题至关重要。该项目专注于开发基于AI的自动推理系统指导，设计高效的证明自动化，并将这些进步融入现代证明助手中。

团队简介

切扎里·卡利齐克（Cezary Kaliszyk）

墨尔本大学的教授，专攻自动推理、证明辅助自动化和交互式定理证明。在荷兰拉德堡德大学获得博士学位后，他担任因斯布鲁克大学的终身副教授。他的研究领域包括学习引导式证明搜索、名义逻辑以及Coq和形式集合论的锤子系统开发。

马丁·苏达（Martin Suda）

Martin Suda领导着捷克信息学、机器人学和控制论研究所（CIIRC）的自动推理小组，该研究所隶属于布拉格捷克技术大学。他的研究探索了机器学习与自动定理证明的交叉领域，重点是增强像“吸血鬼证明器”（Vampire prover）这样的系统。他拥有萨尔大学博士学位，并在曼彻斯特和维也纳担任过博士后。

扬·雅库布夫（Jan Jakubův）

捷克布拉格技术大学CIIRC的高级研究员，专攻自动推理和形式验证。他于赫瑞瓦特大学获得博士学位，研究方向为过程演算和类型系统。他近期的研究重点是机器学习技术在定理证明中的应用，同时也是ENIGMA的主要开发者。

13、文档级自动形式化

项目简介

该项目将开发开源工具，实现数学文档形式化的自动化，并利用Lean证明助手对研究级数学进行算法验证。项目团队将充分利用其在数论和几何优化领域高等数学形式化的经验，以及在自然语言处理和形式验证方面的专业知识。通过将大语言模型与自动符号推理相结合，该项目将创建一个基于Lean蓝图的模块化形式化框架，从而推动数学结果形式化验证的民主化。

团队简介

安托万·博塞吕（Antoine Bosselut）

瑞士洛桑联邦理工学院（EPFL）计算机与通信科学学院的助理教授。此前，他曾在斯坦福大学担任博士后研究员，并在艾伦AI研究所（AI2）担任青年研究员。他于2020年获得华盛顿大学博士学位。他的研究重点是开发能够有效转化为解决医疗、教育和弱势群体等重要社会问题的AI推理方法。他于2021年入选《福布斯》杂志30位30岁以下科学与医疗保健领域杰出人物榜单，并担任瑞士AI计划指导委员会成员。

维克托·昆恰克（Viktor Kunčak）

洛桑联邦理工学院 (EPFL) 计算机与通信科学学院的副教授，他于2007年获得麻省理工学院 (MIT) 博士学位后加入该学院。此后，他一直领导洛桑联邦理工学院自动推理与分析实验室，指导了16篇已完成的博士论文。他的团队开发了Stainless软件验证器和Lisa形式化证明助手。Viktor曾是欧洲自动推理、验证和综合网络（COST 行动）的发起人和协调员之一，并获得了欧洲研究理事会 (ERC) 为期5年、金额为150万欧元的程序综合研究经费。

玛丽娜·维亚佐夫斯卡（Maryna Viazovska）

1984年出生于乌克兰基辅。她于2005年获得基辅国立大学数学学士学位，并于2007年获得凯泽斯劳滕大学硕士学位。她曾是马克斯·普朗克数学研究所Don Zagier教授的博士生，并于波恩大学获得博士学位。在柏林洪堡大学完成博士后研究后，她于2017年加入洛桑联邦理工学院（EPFL），并于2018年成为该学院的全职教授。2022年，她因解决八维球体堆积问题而荣获菲尔兹奖。

参阅

14、特定领域Mathlib文档

项目简介

该项目旨在通过创建易于理解、针对特定领域的Lean定理证明指南，为对形式化感兴趣的数学家们搭建桥梁。该项目面向研究生及以上水平的数学家，重点关注代数数论和图论等领域。在这些领域，现有的Mathlib API虽然已经非常成熟，但对于非专业人士来说仍然颇具挑战性。通过提供参考成功资源的概述、示例和练习，该项目旨在增强对形式化的理解和参与，最终扩展可用于AI模型训练的高质量Lean代码。

团队简介

约翰·塔尔博特（John Talbot）

曾任牛津大学政府通信总部 (GCHQ) 研究员，后获伦敦大学学院皇家学会大学研究员称号。他目前是伦敦大学学院纯数学副教授，研究极值和概率组合学。他最近对Lean证明形式化产生了兴趣。

理查德·M·希尔（Richard M. Hill）

曾在哥廷根和马克斯普朗克研究所（波恩）担任研究职务，现任伦敦大学学院纯数学教授。

15、游戏结束还是QED？——将Lean游戏服务器提升到新的水平

项目简介

Lean游戏服务器项目旨在通过提供易于理解的数学形式化和验证入门，拓展计算机辅助定理证明的覆盖范围和影响力。该服务器将进行扩展，以吸引多元化的学生和研究人员群体，鼓励他们参与形式化数学，提升其教育价值，并在数学AI领域培育更庞大的贡献者社区。

团队简介

马库斯·齐布罗维斯（Marcus Zibrowius）

Marcus Zibrowius是杜塞尔多夫海因里希·海涅大学的拓扑学和几何学教授。他的博士论文在剑桥大学Burt Totaro的指导下完成。他的核心研究领域是K-理论，但最近他也领导了使用拓扑数据分析方法研究大语言模型的研究。

16、GNN-SMT——基于联盟的Lean 4证明自动化

项目简介

斯坦福Centaur实验室在Lean 4中采用双管齐下的方法实现证明自动化：Lean-SMT和通用定理证明智能体。Lean-SMT集成了SMT（可满足性模理论）求解器，以扩展Lean的功能并提供一种新的证明策略。通用定理证明智能体的灵感源自真正的数学家进行数学运算的方式，并使用机器学习辅助的蒙特卡洛树搜索（AlphaGo等AI突破背后的技术）基于启发式过程探索大量的证明状态空间。

团队简介

克拉克·巴雷特（Clark Barrett）

斯坦福大学计算机科学（研究）教授。他的专长是自动推理及其应用。他是可满足性模理论（SMT）和形式化硬件验证的早期先驱。近年来，他还开创了将形式化方法应用于AI系统的技术。他是斯坦福自动推理中心（Centaur，Center for Automated Reasoning）主任和斯坦福AI安全中心联合主任。他是ACM会士，并两度荣获计算机辅助验证（CAV）奖。

莱尼·阿尼瓦（Leni Aniva）

斯坦福大学计算机科学博士生。她是Pantograph工具的主要作者，该工具被学术界和工业界的众多机器辅助定理证明项目广泛使用。她拥有多年的软件工程经验，曾参与SMT求解器、证明助手和机器学习智能体的开发，尤其注重可诊断性和效率。

阿卜杜勒曼·穆罕默德（Abdalrhman Mohamed）

斯坦福大学的博士生，研究方向为定理证明和模型检查的交叉领域。他是cvc5和Lean-SMT（一种将cvc5集成到Lean中的策略）的核心开发人员。他的研究重点是SMT求解及其在形式验证中的应用。

哈伦·可汗（Harun Khan）

斯坦福大学计算机科学专业的博士生。他的研究重点是形式化验证、定理证明和自动推理。他致力于Lean定理证明器中的数学形式化，包括“所有方法的稳健均值估计”，以及形式化证明规则，以实现SMT求解器与Lean的集成。

17、LeanAide——通过自动形式化连接AI和数学

项目简介

该项目旨在通过开发一套无缝集成自然语言处理、大语言模型 (LLM) 和Lean的工具，重新审视数学概念的形式化和发现方式。通过创建一个易于访问的无代码AI+Lean环境，该项目旨在简化Lean用户的形式化流程，并为数学家提供包括智能体解决方案在内的全新创新研究工具。

团队简介

悉达多·加吉尔（Siddhartha Gadgil）

印度科学研究所的数学教授。他拥有加州理工学院几何拓扑学博士学位，并在相关领域工作多年。近十年来，他主要致力于自动定理证明的研究。在过去三年左右的时间里，他致力于开发Lean Prover，尤其致力于构建与AI集成的工具。他的主要研究目标是使AI和Lean能够应用于数学发现，而无需任何特殊的（非数学）专业知识。

维拉杰·库马尔（Viraj Kumar）

Kotak-IISc AI-ML中心的客座教授。他的研究重点是计算机教育，尤其关注如何重新思考生成式AI时代的教学法和评估方法。他拥有伊利诺伊大学厄巴纳-香槟分校计算机科学博士学位（2007年），并且是ACM印度理事会的当选成员，并担任其教育项目的联合主席。

阿尼鲁德·古普塔（Anirudh Gupta）

目前正在班加罗尔印度科学技术学院 (IISc Bengaluru) 攻读理学学士学位。他的兴趣包括数学、计算机科学和印度古典长笛演奏。他是一位敬业且充满热情的人，喜欢与团队合作，并尽其所能地投入工作。对他来说，从事研究工作不仅仅是一种职业追求，更是一份激发他求知欲的真挚热情。他渴望做出有意义的贡献，在学术环境中茁壮成长，不断寻求探索和发现的机会。

姆里甘克（Mrigank）

印度科学研究所的一名即将升入大四的学生，正在攻读数学和计算机专业的理学学士学位。他的研究重点是开发用于提升软件质量和自动化软件工程流程的工具。他尤其感兴趣的是探索如何将传统的软件测试和分析技术与日益强大的大语言模型相结合，以大规模地解决此类问题。Mrigank希望通过模糊数学与软件界限的定理证明器，将软件工程的进步带入日益发展的形式化和自动化数学领域。

斯瓦尔纳瓦·查克拉博蒂（Swarnava Chakraborty）

目前正在印度理工学院攻读数学与计算机学士学位，已完成二年级学业。他一直对自动定理证明领域充满兴趣。他的主要研究兴趣在于利用Lean方法实现自动形式化，以及将AI融入这一广阔领域。

舒巴姆·库马尔（Shubham Kumar）

专攻使用OCaml进行函数式编程以及使用Coq进行形式化验证。他对形式化方法的兴趣始于学习期间，并通过在多核OCaml上的工作得以巩固。这段经历促使他开始使用OCaml开发系统，并使用Coq和coq-of-ocaml应用形式化验证技术。

18、LeanTutor——本科数学证明辅导

项目简介

LeanTutor借助交互式定理证明器 (ITP) 和大语言模型 (LLM)，重新审视了本科生学习数学证明的方式。LeanTutor旨在自动形式化学生（本科生）的自然语言证明，使用ITP评估证明的正确性，利用ITP的反馈生成后续步骤，并为学生提供个性化指导。LeanTutor的设计借鉴了教育研究、机器学习和形式化方法的洞见，旨在开发一个系统，让学生和AI智能体能够一起进行有意义的数学学习。

团队简介

吉雷贾·拉纳德（Gireeja Ranade）

加州大学伯克利分校电气工程与计算机科学 (EECS) 系的副教授。在此之前，她曾在华盛顿州雷德蒙德市的微软研究院担任研究员。她在加州大学伯克利分校获得电气工程与计算机科学博士学位，并在马萨诸塞州剑桥市的麻省理工学院获得本科学位。她因其研究和教学成果荣获多项奖项，例如美国国家科学基金会杰出人才奖 (NSF CAREER Award)、加州大学伯克利分校电气工程杰出教学奖、加州大学伯克利分校杰出GSI指导奖等。

19、大语言模型——用于反应式程序的格论推理

项目简介

该项目旨在通过开发一种新颖的方法，利用基于合成的精化命题数据集进行微调的大语言模型 (LLM) 来证明精化定律，从而推动数学推理AI的发展。团队致力于创建包含证明和反例的综合数据集，以提高训练数据集的多样性和质量，从而弥补数学AI领域的重大差距。该项目将LLM与最先进的精化检查技术相结合，以提高精化证明的准确性和效率。这项工作不仅有望超越现有方法，还将为未来数学推理AI模型训练提供宝贵的基准数据集。

团队简介

佩德罗·里贝罗（Pedro Ribeiro）

英国约克大学计算机科学讲师（助理教授）。此前，他曾担任约克大学物理工程与技术学院的研究员，更早之前担任计算机科学的助理研究员。他在约克大学获得了博士学位，研究方向为通过统一程序设计理论中的完整格理论处理过程演算中的非确定性问题。他在机器人技术和信息物理系统相关的软件工程形式化方法方面拥有十多年的经验。他的研究兴趣涵盖了整个工程生命周期，从领域特定符号及其语义的设计和开发，到使用自动化数学证明技术（例如模型检查和定理证明）进行测试和形式化推理。他是约克大学RoboStar机器人软件工程卓越中心的成员，也是欧洲形式化方法协会传播委员会的创始成员。

弗兰克·索博岑斯基（Frank Soboczenski）

约克大学计算机科学 (AI/ML) 助理教授，并在伦敦国王学院担任副科学家。他的研究重点是深度学习和Transformer模型、可解释机器学习和量子机器学习，主要侧重于太空和医疗保健领域的应用。Frank是NASA和NOAA的GLOBE计划的STEM科学家、NASA GeneLab AI重点工作组成员（负责载人航天数据）、IBM量子研究人员计划科学家、NASA Nancy Grace Roman航天器工作组成员、激光干涉仪空间天线 (LISA) 工作组成员、欧洲学习和智能系统实验室 (ELLIS) 学者、国际天文学联合会(IAU) 成员。Frank经常与NASA中心合作，包括领导肯尼迪航天中心过去的机器学习研讨会并担任NASA生物医学研讨会的发言人。他的工作获得了多项荣誉，例如NASA TechLeap奖；NASA/NOAA/美国国务院对杰出指导的认可；以及多个前沿发展实验室的荣誉。

20、Leaning and Rocq'ing（Lean和Rocq Prover）

项目简介

该项目利用大语言模型 (LLM) 的强大功能，促进不同交互式定理证明器 (ITP)（例如Lean和Rocq Prover）之间以及同一证明器不同版本（例如Lean 3与Lean 4）之间陈述和证明的转换。通过实现跨平台证明和库的转换，该项目旨在创建一个统一的形式化知识库，增强形式化方法社区内的协作和资源共享。这项工作不仅可以连接MathLib和Mathematical Components等重要资源，还能在未来的重大更新（例如Lean 5）期间支持更顺畅的过渡。

团队简介

纪尧姆·鲍达特（Guillaume Baudart）

Inria IRIF实验室PICUBE团队的研究员。2017年至2020年，他曾担任IBM TJ Watson研究中心AI编程模型团队的研究员。他的研究重点是概率编程，最近又转向了用于交互式定理证明的生成式AI。

西里尔·科恩（Cyril Cohen）

Inria里昂高等师范学院LIP CASH团队的研究员。他的主要研究方向是利用数学知识丰富Rocq证明器。他也是数学组件库的主要架构师之一。

尼古拉斯·塔巴罗（Nicolas Tabareau）

Inria高级研究员，领导着位于南特的Gallinette团队。他专注于交互式定理证明器 (ITP) 的开发和实现，并在Rocq Prover的持续开发中发挥着积极作用。

马克·勒拉奇（Marc Lelarge）

Inria高级研究员，也是巴黎高等师范学院计算机科学系的讲师。他的研究涵盖机器学习、深度学习和图论，近期专注于用于交互式定理证明的生成式AI。

参考资料

https://www.renaissancephilanthropy.org/ai-for-math-fund-projects

https://www.renaissancephilanthropy.org/news-and-insights/ai-for-math-fund-announces-18-million-in-grants-to-accelerate-breakthrough-discoveries-in-mathematicsnbsp

小乐数学科普近期文章

出版社和作家自荐通道

小乐数学科普荐书

·开放 · 友好 · 多元 · 普适 · 守拙·

让数学

更加

易学易练

易教易研

易赏易玩

易见易得

易传易及

欢迎评论、点赞、在看、在听

收藏、分享、转载、投稿

查看原始文章出处

点击zzllrr小乐

公众号主页

加星★

数学科普不迷路！