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

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

接上文

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

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

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

21、学习与吸血鬼（Vampire）和蜘蛛（Spider）一起做数学题

项目简介

该项目旨在通过将无穷级数和超越函数等特定数学结构集成到全自动定理证明器Vampire（吸血鬼）的推理程序中，增强其性能。本项目旨在通过创新的机器学习方法和针对特定数学理论定制的策略组合开发，提升Vampire在标准数学上的表现。该项目还将建立一个网络服务，以促进自动定理证明器的使用，并创建开放数据集，以支持全球自动定理证明工作。

团队简介

安德烈·沃伦科夫（Andrei Voronkov）

安德烈· 沃伦科夫从7岁起就痴迷于证明定理，而从15岁第一次接触穿孔卡片起，他同样痴迷于编写计算机程序。毫不奇怪，他的第一个非玩具计算机程序是一个用于证明定理的程序。

他对计算机定理证明的热情促成了定理证明器Vampire的设计和初步开发，该程序自1999年以来在一阶定理证明中赢得了70个世界冠军头衔。

他在自动推理的诸多领域做出了贡献，包括理论、实现技术和应用。2007年，他为Vampire开发了首个基于机器学习的策略调度程序Spider（蜘蛛）。在业余时间，他还开发了会议管理系统EasyChair，该系统目前已被超过400万研究人员使用。

他认为，当数学家和计算机程序互相传授数学知识、互相学习时，世界将会变得更加美好。他相信，最近在自动推理领域发展起来的技术，例如理论推理和归纳法，能够在未来20到50年内引领计算机辅助数学的革命。

迈克尔·罗森（Michael Rawson）

迈克尔·罗森认为计算机应该能够推理并从过去的经验中学习。他对自动定理证明尤其感兴趣：能够进行严密逻辑论证的计算机系统。他是“古董吸血鬼”（Antique Vampires）团队的一员：该团队负责监督和指导世界领先的定理证明器“吸血鬼”（Vampire）的设计和开发。

22、数学基准（Mathbench）——评估自然语言证明

项目简介

MathBench项目旨在通过引入一个全新的带注释证明数据集，来提升AI模型在数学推理方面的评估能力。该数据集包含与多个不同证明配对的定理，每个证明被分解为关键步骤，并附有摘要、错误论证和逻辑结构元数据的注释。通过利用MathBench，该项目旨在评估AI模型识别关键证明步骤、纠正错误以及区分有效和无效证明的能力，从而了解大语言模型在数学推理和理解方面的能力。

团队简介

悉达多·巴特（Siddharth Bhat）

剑桥大学的博士生。他是形式化验证、函数式编程语言实现和应用范畴论方面的专家。他是Lean定理证明器前20名贡献者之一。他在高性能计算和循环优化方面也拥有丰富的经验。他的长期愿景是构建可扩展的数学定理证明系统，并已为此发表了多项研究成果。

亚历克斯·哈夫里拉（Alex Havrilla）

佐治亚理工学院数学与机器学习博士生。他的研究方向是生成模型的理论与实践，重点是通过强化学习和合成数据改进推理能力。他曾在Meta、微软和谷歌实习，并共同创立了开源RLHF研究小组CarperAI。

斯特拉·比德曼（Stella Biderman）

EleutherAI的执行董事，EleutherAI是一家由草根研究团体转型而来的非营利性研究机构，开创了现代开源AI运动。Stella在 GPT-Neo、Pythia、BLOOM、OpenFold和VQGAN-CLIP等模型上的工作，极大地提升了基础模型的可访问性，同时也为AI的透明度和开放科学树立了标杆。除了开发新模型外，Stella还投入了大量时间致力于开发开源AI库、构建和记录公共数据集以及开展可解释性研究。

帕万·萨桑卡·阿曼纳曼奇（Pawan Sasanka Ammanamanchi）

Ritual的研究员，也是EleutherAI的志愿研究员。他拥有印度理工学院海得拉巴分校的硕士学位，专攻大语言模型的评估。他的贡献包括BLOOM模型和GEM基准测试。他尤其热衷于推动AI在数学领域的应用。

23、AI和机器学习的新范畴和拓扑基础

项目简介

该项目探索基于更定制的数学表示空间和结构（包括层论sheaf theory和范畴论category theory）的新型神经网络架构。这些新型架构或许能够融入数学对象的关键结构对称性和属性，从而能够创建辅助证明构建的新工具，并提供超越当前AI Copilot范式的实用优势。探索能够在丰富类型理论中表示和操纵证明状态的模型的可能性，或许能帮助我们弥合机器学习与传统数学领域之间的差距。

团队简介

皮埃特罗·利奥（Pietro Lio）

剑桥大学计算机科学系的计算生物学教授，他于2004年加入该系任教。他最初在佛罗伦萨和帕维亚学习，专注于遗传学和复杂系统，之后在南安普顿和剑桥担任研究职位。他的工作重点是利用AI和计算生物学来理解疾病过程。

杰米·维卡里（Jamie Vicary）

剑桥大学计算机科学系未来计算教授。他获得物理学和数学学士学位后，在牛津大学担任计算机科学研究员十年，2018年加入伯明翰大学担任高级讲师，并于2020年调至剑桥大学任教。他的研究兴趣广泛，涵盖量子计算、理论计算机科学和机器学习。

24、Polymath Plus（Polymath +）

项目简介

Polymath Plus是一个新一代在线协作平台，它将大规模的人类互动与基于AI的推理相结合，以推进数学探索。在Polymath原项目的基础上，它既利用AI作为管理员来管理讨论，又利用AI作为协作者来贡献想法并验证证明。Polymath Plus旨在将人类直觉与机器辅助的严谨性相结合，简化既定定理，解决尚未解决的挑战，并加速数学界的协作。

团队简介

皮埃特罗·米切鲁奇（Pietro Michelucci）

人类计算研究所的执行主任，也是康奈尔大学的访问学者。作为一名专注于人机混合智能的认知科学家，他致力于运用人机互补的优势来解决社会问题。他创立了“Stall Catchers”公民科学项目，并担任《人类计算手册》的编辑。

杰森·戴尔 (Jason Dyer)

在高中任教11年；在此期间，他参与了Polymath项目，该项目发现了Hales-Jewett定理密度版的新组合证明。之后，他加入了数学和科学学习应用程序Brilliant.org，负责开发课程，并与服务成员安排小型Polymath项目。他目前为欧洲、北美和亚洲的客户提供教育游戏设计咨询服务。

萨姆·沙班（Sam Shaaban）

自1999年创立NuRelm以来，Sam Shaaban一直致力于为研究人员和创新者开发软件。他热衷于帮助创作者集思广益、制作原型、制定预算并交付数字健康应用程序、被动传感器数据收集系统、研究门户、数据处理管道以及改善生活的创造性方法。

迈克尔·斯蒂尔曼（Michael Stillman）

本科就读于伊利诺伊大学，研究生就读于哈佛大学。在芝加哥大学、布兰迪斯大学和麻省理工学院担任博士后后，他加入康奈尔大学数学系任教。他的研究兴趣围绕计算代数几何，包括算法、实现和应用（例如生物学和理论物理学）。他是Macaulay2计算机代数系统的创始人之一。

格雷格·利普斯坦（Greg Lipstein）

DrivenData的联合创始人兼负责人。DrivenData是一家致力于将AI的变革力量带给应对全球最严峻挑战的组织的社会企业。DrivenData的竞赛平台汇聚了全球数据科学家的技能和热情，旨在构建造福社会的解决方案。我们与杰出的社区以及NASA、微软、Meta AI和世界银行等组织合作，已提供超过480万美元的奖金，评估了超过20万份参赛作品，并为公共服务、健康、科学、自然、教育等领域提供了先进的解决方案。

蒂莫西·高尔斯（Timothy Gowers）

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

25、通过数学数据库进行可扩展定理证明

项目简介

该项目旨在通过在Lean数学库(mathlib)和L-函数及模形式数据库(LMFDB)之间建立接口，扩大自动定理证明器可访问的数学内容规模。通过将mathlib约10万个数学结果集合与LMFDB超过10亿个具体语句的存储库连接起来，我们的目标是扩展人类数学家和AI智能体的能力。该项目将开发新的Lean策略，并建立一个将其他数学数据库与形式化定理证明系统集成的框架，为可扩展的数学发现铺平道路。

团队简介

克里斯托弗·伯克贝克（Christopher Birkbeck）

东英吉利大学纯数学讲师，专攻数论。他的研究领域包括p进模形式的研究和计算，目前的研究方向是数学形式化，专注于Lean中的模形式理论。伯克贝克在华威大学获得博士学位，导师是拉西娜·登贝莱（Lassina Dembele）和约翰·克雷莫纳（John Cremona），随后在伦敦大学学院（UCL）获得博士后研究资格。

大卫·罗（David Roe）

麻省理工学院数学系的首席研究科学家，他研究计算数论和算术几何，尤其关注p进数（一种与实数类似但距离概念不同的数，用于测量被某个固定素数整除的可能性）。p进数在他为数学界构建计算工具的历程中扮演了核心角色，这始于他在SageMath中对p进计算的研究。他担任L-函数和模形式数据库(LMFDB)的执行编辑，该数据库汇集了数论和算术几何中出现的数学对象；他也是researchseminars.org的创始人之一，该网站是在疫情期间创建的，旨在帮助数学家参加在线研究研讨会。

安德鲁·萨瑟兰（Andrew Sutherland）

麻省理工学院数学高级研究员，其研究项目专注于算术几何和数论的计算方面。他在多项大型研究合作中发挥了重要作用，包括 “素数间有界间隙”的Polymath项目 、 L-函数和模形式数据库以及 “算术几何、数论和计算”西蒙斯合作项目 。萨瑟兰目前担任《计算数学》Mathematics of Computation的编辑、《数论研究》Research in Number Theory的主编、《L-函数和模形式数据库》 的执行编辑、布朗大学数学计算与实验研究所的科学顾问委员会成员、数论基金会主席以及美国数学会会士。

26、画板（Sketchpad）——高精度且易于使用的自动形式草图生成系统

项目简介

Sketchpad是一个由AI驱动的系统，用于将自然语言证明转换为结构化的形式化草图，旨在协助使用Isabelle和Lean进行形式数学工作的从业者。通过引入基于图形的表示，它能够将证明分解为单个陈述，从而支持细粒度的自动形式化，并与部分或不完整的证明进行更高效的交互。

团队简介

Wenda Li（李文达——音译）

爱丁堡大学混合AI助理教授，专攻数学AI。他为使用大语言模型进行自动形式化的开创性工作做出了贡献，并探索了用非形式化证明指导形式化定理证明的方法。除此之外，他的工作还涵盖了验证量词消元法、格罗滕迪克的概形理论（scheme theory）以及解析数论的各个方面。他在这些领域的成就被评为BCS最佳论文奖亚军。

Mai Luo（罗麦——音译）

爱丁堡大学副教授（西安电子科技大学学士、伦敦帝国理工学院硕博），领导大规模机器学习系统研究组。他担任英国工程与物理研究理事会（EPSRC）机器学习系统博士培训中心联合主任，以及英国ARIA项目“Scaling Compute – Charting the Course”的联合负责人。他的研究涵盖计算机系统、机器学习和数据管理。他领导的AI系统已被各大科技公司采用，并以开源软件的形式广泛发布，并获得了广泛的认可。他是谷歌博士生奖学金和微软亚洲研究院StarTrack奖的获得者，并入围了校长新星研究奖的最终角逐。

拉里·保尔森（Larry Paulson）

亚马逊学者、剑桥大学计算逻辑荣誉教授，也是形式逻辑和证明助手领域的知名专家。他领导了广泛使用的Isabelle证明助手的开发，并率先推出了Sledgehammer，这项突破性的创新已被几乎所有主流证明助手所采用。为了表彰他对证明助手和自动推理的杰出贡献，他被选为ACM院士、皇家学会院士，并获得了Herbrand奖。

辛华剑

爱丁堡大学的博士生（本科毕业于中山大学逻辑学专业，目前是字节跳动伦敦Seed实习生），与Jacques Fleuriot和Wenda Li合作。他的研究重点是使用大语言模型进行自动定理证明，尤其关注能够自动形式化和知识库学习的自主智能体。他的代表作包括：最先进的开源定理证明模型DeepSeek Prover系列；以任务分解和知识积累为特色的LEGO-Prover；以及用于库级证明工程评估的基准数据集APE-Bench。

27、迈向自动化数学发现

项目简介

该项目探索了一个多智能体猜想器-证明器框架，该框架利用大语言模型(LLM) 在Lean定理证明器中生成并证明新颖的数学猜想。该框架从实用性和新颖性的角度量化和形式化“趣味性”的概念，旨在简化开放式数学探索和发现。通过对猜想器和证明器进行迭代改进，这种创新方法旨在推进自动化定理证明，并为新的数学见解的发展做出贡献。

团队简介

亚伦·库维尔（Aaron Courville）

蒙特利尔大学计算机科学与运筹学系(DIRO)的教授，也是IVADO的科学主任。他拥有卡内基梅隆大学机器人研究所的博士学位。Courville是深度学习的早期贡献者：他是Mila——魁北克AI研究所的创始成员之一。他与Ian Goodfellow和Yoshua Bengio共同编写了深度学习的开创性教科书。他目前的研究重点是深度学习模型和方法的开发。他对强化学习、多智能体强化学习、深度生成模型和推理尤其感兴趣。

纳文·戈亚尔（Navin Goyal）

1998年在孟买印度理工学院获得理学学士学位，并于2005年在罗格斯大学获得博士学位。在麦吉尔大学和佐治亚理工学院从事博士后研究后，他于2009年加入微软印度研究院。他的研究始于理论计算机科学，研究范围涵盖算法设计和分析以及计算复杂性等诸多问题。逐渐地，他的工作转向学习理论。他的理论研究有时涉及应用数学各个领域的技术（例如组合学、信息论、傅里叶分析）。这使他对数学和理论计算机科学的多样性和统一性产生了浓厚的兴趣。最近，他一直在进行实证研究，从多个角度理解神经网络，包括其归纳偏差和对其内部工作原理的解释，以及其解决数学问题的能力。他对数学和其他领域的人们如何取得新发现非常感兴趣。

28、犊皮纸（Vellum）——AI辅助形式推理的可扩展框架

项目简介

Vellum项目构建了一个开源框架，其中大语言模型 (LLM) 充当规划器，并与多个交互式定理证明器 (ITP) 和自动求解器交互，旨在简化数学探索和证明过程。通过与不同类型的求解器和工具交互，Vellum促进了大规模的AI辅助形式推理，从而简化了自然语言陈述的自动形式化，并显著降低了数学推理研究的门槛。

团队简介

斯瓦拉特·乔杜里（Swarat Chaudhuri）

德克萨斯大学奥斯汀分校计算机科学教授，同时也是谷歌Deepmind的研究科学家。他的研究融合了自动推理、机器学习和编程语言的理念，旨在创建功能强大、可靠、透明且安全的AI系统。Chaudhuri博士于2001年获得印度理工学院（Kharagpur）计算机科学学士学位，并于2007年获得宾夕法尼亚大学计算机科学博士学位。他是2025年古根海姆学者，并曾获得美国国家科学基金会杰出人才奖、ACM SIGPLAN John Reynolds论文奖、宾夕法尼亚大学Morris and Dorothy Rubinoff论文奖、Meta奖和谷歌研究奖，以及多项ACM SIGPLAN和SIGSOFT杰出论文奖。 Chaudhuri博士曾担任机器学习、形式化方法和编程语言领域所有主要会议的项目委员会成员，并担任CAV 2016和ICLR 2024的项目主席。

宋晓冬（Dawn Song）

加州大学伯克利分校计算机科学教授（1974年出生于辽宁营口，清华大学物理系学士，卡内基梅隆大学计算机系硕士，加州大学伯克利分校博士），伯克利负责任去中心化智能中心联合主任。她的研究领域包括AI与深度学习、安全与隐私以及去中心化技术。她曾获得多项奖项，包括麦克阿瑟奖、古根海姆奖、美国国家科学基金会杰出青年奖、阿尔弗雷德·P·斯隆研究奖、《麻省理工科技评论》TR-35奖、ACM SIGSAC杰出创新奖，以及十余项计算机安全和深度学习领域顶级会议的“经得起时间考验”奖和最佳论文奖。她是计算机安全领域被引用次数最多的学者，被评为最具影响力学者（AMiner奖）。她是ACM会士和IEEE会士，也是美国艺术与科学学院当选院士。她在加州大学伯克利分校获得博士学位。她还是一位连续创业者，并被《Inc.》杂志评选为百强女性创始人，并被《Wired25》评选为创新者。

何静轩

加州大学伯克利分校的博士后研究员。他的研究领域广泛，涵盖计算机安全、机器学习和编程语言，近期专注于提升AI软件程序的安全性和可靠性。他于苏黎世联邦理工学院获得博士学位，并荣获苏黎世联邦理工学院杰出博士论文奖章。他还曾荣获ACM CCS 2023杰出论文奖。

Zhe Ye（叶哲——音译）

加州大学伯克利分校和伯克利研发中心的博士生（上海科技大学信息科学与技术学院计算机科学学士）。他的研究方向包括大语言模型辅助形式化验证、形式化规范合成和计算机安全。他在相关领域发表了多篇论文，其中一些已被IEEE S&P和ISSTA等顶级会议录用。

阿米塔尤什·塔库尔（Amitayush Thakur）

德克萨斯大学奥斯汀分校的博士生，致力于“数学AI”和“代码AI”的交叉研究。他的兴趣在于通过大语言模型进行自动化数学推理，以及其在完全验证的程序合成中的意义，这对于从AI生成工业级代码至关重要。他是Copra（一个用于形式化定理证明的智能体框架）的首席开发者。加入德克萨斯大学之前，他曾在微软担任软件工程师，此前曾在微软研究院担任研究实习生。

乔治·苏卡拉斯（George Tsoukalas）

德克萨斯大学奥斯汀分校的博士生，致力于研究用于自动数学推理和程序合成的神经符号技术。他领导创建了PutnamBench，这是一个前沿的AI数学基准测试，并在ICML 2024 AI数学研讨会上荣获最佳论文奖。他还为COPRA做出了贡献，COPRA是一种基于智能体的LLM形式化定理证明方法。

参考资料

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小乐

公众号主页

加星★

数学科普不迷路！