★加星zzllrr小乐公众号数学科普不迷路！
该基金首批29个获奖项目涵盖大学和机构的数学家和研究人员，他们致力于开发有助于推进多项关键任务的数学发现和研究的系统。这些项目包括前沿形式化数学数据集、促进人工智能与数学协同作用的软件工具，以及一些将人工智能应用于基础数学和应用的高风险、高回报的构想。资助金额最高可达100万美元。
XTX Markets慈善事业主管Simon Coyle表示：“AI for Math 基金首轮的提案非常强劲，因此XTX Markets很高兴将我们的初始资金翻倍。我们期待这些项目在未来一年内陆续上线，并支持世界各地数学家的工作。”
数学AI基金（AI for Math Fund）旨在通过支持那些对数学领域至关重要、但目前缺乏任何学术或产业实验室动力去实施的项目，来加快数学探索的步伐并提升其影响力。
该基金支持那些在常规情况下不太可能实现，但有潜力推动整个领域发展的项目。
这些项目包括：开发开源的、生产级质量的工具；提升训练AI模型所需数据集的规模、多样性和质量；以及提升工具的易用性，使其更容易被数学家采用。
该基金的首批 29 项资助将颁发给大学和组织的研究人员，以支持他们开发有助于推进多项关键任务的数学发现和研究的系统。
首届数学AI基金投资对象由研究人员、大学和组织组成，他们开发的系统有助于推进数学发现，涵盖数学AI研究中的一系列关键主题和瓶颈，包括：
关键数据集开发
改进证明器与数学家之间的互动
核心功能和覆盖范围的改进
有前景的领域建设的倡议举措
雄心勃勃的“登月计划”
2025年获选项目及团队介绍 (1~10)
（按项目英文名排序）
1、一种以AI为中心的语言学习策略
项目简介
该项目旨在通过开发一种Lean领域特定策略语言来增强AI证明智能体，使其更好地与AI的能力和优势相匹配。通过分析AI生成证明与人工证明之间的结构差异，该团队力求理解AI智能体的句法偏好，并据此提出更有针对性的AI优先策略。这项工作将促成新策略的实施以及一个自动形式化模型，以优化AI的符号推理和搜索能力。
团队简介
罗伯特·Y·刘易斯（Robert Y. Lewis）
布朗大学计算机科学系的助理教授。他的研究兴趣涉及Lean数学形式化验证，重点关注证明中使用的策略语言。他是Lean数学库（Mathlib）的维护者，并已参与形式化数学项目十年。
2、一个现代形式化定理陈述的数据集
项目简介
该项目创建了一个公共数据集，其中包含数百个来自顶级期刊（例如《数学年鉴》）的最新定理的形式化陈述。此举将解决数学研究前沿领域形式化不足的关键问题。通过专门的专家形式化研究，该项目将显著扩展形式化数学库，并为AI系统在各种任务上提供清晰的目标，包括自动形式化证明和协助人类进行证明形式化。
团队简介
凯文·巴扎德（Kevin Buzzard）
伦敦帝国理工学院的代数数论学家。他目前正在研究费马大定理的Lean形式化。他在2022年国际数学家大会上发表了关于交互式定理证明器的全体会议报告。
3、一种搜索证明的原则性方法及其在Siderenko（西多连科）猜想中的应用
项目简介
本项目提出了新的证明方法，旨在自动化和简化重大未解问题的证明发现过程。为此，本工作旨在建立一个严谨的理论框架、植入性证明，并开发新的算法，以高效且可扩展地推导出开放问题的证明。作为概念验证，本项目将专注于创建一种理论上合理的方法来寻找可满足性 (SAT) 公式的解析证明，并开发机器学习工具来解决组合数学中一个关键的开放问题——Siderenko猜想。通过弥合这些差距，本项目有望推动AI在数学领域的理论和实践发展。
团队简介
普拉维什·K·科塔里（Pravesh K Kothari）
普林斯顿大学计算机科学系的助理教授。此前，他曾担任卡内基梅隆大学计算机科学系助理教授，并于2016年至2019年期间担任普林斯顿高等研究院和普林斯顿大学计算机科学系联合举办的计算机科学研究讲师。Kothari博士的研究兴趣涵盖理论计算机科学的多个主题，例如凸优化及其在算法设计中的应用、统计估计和平均情况组合优化的算法和下界，以及谱方法及其与随机矩阵理论、编码理论和极值组合学的联系。Kothari博士曾获得普雷斯堡（Presburger）奖（2024年）、印度理工学院坎普尔分校青年校友奖（2023年）、斯隆奖学金（2022年）和美国国家科学基金会职业奖（2021年）。
拉古·梅卡（Raghu Meka）
加州大学洛杉矶分校 (UCLA) 计算机科学教授。Meka教授在德克萨斯大学奥斯汀分校获得博士学位，并在普林斯顿高等研究院和罗格斯大学DIMACS获得博士后研究。Meka教授的研究领域涵盖概率论、学习理论、组合数学和理论计算机科学的交叉领域。他是2025年IEEE W. Wallace MacDowelll奖的获得者。他还曾获得2023年IEEE计算机科学基础研讨会 (FOCS) 和2024年学习理论会议 (COLT) 的最佳论文奖。
4、一种机器辅助定理证明策略的结构化表示
项目简介
本项目开发了一种机器学习驱动的方法来创建交互式定理证明策略。该项目将策略表示为高级语言中的代数对象，一旦应用，就会修改证明状态。反过来，这种语言可以转换为Lean元程序，并将促进大语言模型通过交互式会话自动创建证明脚本。通过这项工作，该项目希望发现新的证明策略，从而进一步简化定理证明工作。
团队简介
杰德·马斯特（Jade Master）
拥有应用范畴论博士学位，专攻复杂系统的组合性。在完成余代数形式验证博士后研究并担任函数式程序员后，她担任ARIA Safeguarded AI项目的首席研究员。她在ARIA（英国高级研究与发明局）的项目旨在开发基于范畴形式主义的可扩展世界模型。她计划通过开发用于策略生成的组合技术，将这项工作与Containers for AI（AI容器）项目结合起来。
文森特·王-马希西亚尼卡（Vincent Wang-Maścianica）
在牛津大学获得博士学位，研究重点是连接实用计算语义和形式组合结构的幺半范畴理论。他目前是牛津大学哲学系以人为中心AI实验室的高级研究员。
赞齐·米赫耶夫斯（Zanzi Mihejevs）
拥有超过10年使用函数式编程形式化各种范畴结构的经验，并且在为咨询公司构建领域特定语言方面拥有丰富的经验。她是Glaive的ARIA资助项目的首席研究员，致力于构建一种利用范畴论推动编程前沿发展的编程语言。
布鲁诺·加夫拉诺维奇（Bruno Gavranović）
Bruno Gavranović博士，是一位数学家和计算机科学家，他通过与Google DeepMind合作开展的研究以及其博士论文《深度学习的基本组成部分：一种范畴论方法》开创了范畴深度学习。他将这一理论成果转化为实际成果，在为 Symbolica AI 争取3100万美元融资的过程中发挥了关键作用，并创立了Coend公司。Coend是一家开发用于一等类型编程语言代码生成的基础模型的公司。
安德烈·维德拉（Andre Videla）
思克莱德大学博士生，也是Glaive的研究员。他致力于容器、交互系统和编程的未来发展，并参与开发和维护Idris编程语言。Andre的工作将抽象的范畴思维与实际的编程经验相结合，为现代软件挑战提供了新的解决方案。
迪伦·布雷斯韦特（Dylan Braithwaite）
目前正在攻读理论计算机科学博士学位。他拥有编程语言的范畴语义学和概率编程方面的经验，并曾担任软件开发人员。作为Glaive的成员，他一直在研究ARIA资助的项目，致力于实现一种使用范畴结构以更符合人体工程学的方式表示数学结构的编程语言。
5、桥接AI、证明助手和数学数据（BRIDGE）
项目简介
BRIDGE项目旨在通过创建和管理来自形式化数学库的大规模数据集和依赖关系图，将AI与证明助手和数学数据相结合。该团队将开发基于AI的工具，以支持数学结构、证明及其相互依赖关系的形式化和探索。这些工具（包括推荐系统和用户引导的发现功能）有望提高数学推理的可访问性和效率。
团队简介
安德烈·鲍尔（Andrej Bauer）
斯洛文尼亚卢布尔雅那数学、物理与力学研究所理论计算机科学系主任，同时也是卢布尔雅那大学的计算数学教授。鲍尔的研究领域涵盖数学基础、构造性数学和可计算数学、类型论、同伦类型论、形式化数学以及编程语言的数学原理。他还因其在代数效应和处理程序编程方面的开创性工作而闻名。
普里莫日·波托奇尼克（Primož Potočnik）
卢布尔雅那数学、物理和力学研究所计算密集型数学方法研究小组的负责人，同时也是斯洛文尼亚卢布尔雅那大学的数学教授。他的研究重点是组合和代数结构中的对称性。他因其高度对称的图形和地图数据集而在数学界享有盛誉。
柳普乔·托多罗夫斯基（Ljupčo Todorovski）
卢布尔雅那大学数学与物理学院的计算机科学教授。他的研究兴趣在于AI，尤其专注于开发机器学习算法，用于从实验数据中计算发现科学知识和模型。最近，他一直与数学家合作，设计支持使用证明助手进行数学形式化的AI工具。
丹尼尔·阿赫曼（Danel Ahman）
爱沙尼亚塔尔图大学计算机科学学院的编程语言副教授。他的研究重点是编程语言理论，特别是具有高级类型系统的编程语言的设计和元理论。他致力于使用类型来形式化地指定和验证程序使用数据和资源的方式和时间，开发用于数据结构的组合类型理论模型，并应用这些技术构建correct-by-constrction（按构建逐步校正）且经过验证的软件。
卡佳·贝尔奇奇（Katja Berčič）
斯洛文尼亚卢布尔雅那大学数学、物理和力学研究所的研究员，同时也是该大学的助教。她致力于开发稳健且可互操作的数学数据基础设施，并将其与数学软件集成。她的工作基于对数学家在实践中如何创建、构造和与数据交互的分析。她还研究了这些活动与更广泛的研究数据管理背景之间的关系。
6、桥接复杂性和自动化以推进自动定理证明
项目简介
本项目通过三个创新研究方向实现定理证明的自动化，这些方向解决了关于证明难度、可处理性和性能扩展性的关键概念问题。具体而言，本项目将研究并寻求形式化定义：
从计算复杂性的角度看，证明任务的难度
解决给定的证明任务需要多少数据（真实的和/或合成的）
证明复杂性如何随可用计算资源的变化而变化
团队简介
托尼安·皮塔西（Toniann Pitassi）
哥伦比亚大学计算机科学系的Jeffrey L.和Brenda Bleustein工程学教授。在2020年加入哥伦比亚大学之前，Pitassi曾担任多伦多大学的贝尔加拿大计算机科学研究主席。她的主要研究方向是证明复杂性、复杂性理论以及机器学习的基础主题，包括隐私、公平性和自适应数据分析。Pitassi是美国国家科学院院士，也是ACM会士。
理查德·泽梅尔（Richard Zemel）
哥伦比亚大学计算机科学系Trianthe Dakolias工程与应用科学教授。他是美国国家科学基金会AI与自然智能研究所 (ARNI) 的主任，也是向量AI研究所的联合创始人兼首任研究主任。他担任加拿大高级研究院AI主席，并担任神经信息处理学会顾问委员会成员。他的研究贡献包括：在极少或完全无监督的情况下学习有用数据表示的系统的基础性工作；基于图的机器学习；以及公平稳健的机器学习算法。
陈天龙
北卡罗来纳大学教堂山分校计算机科学系的助理教授。他于2017年在中国科学技术大学 (少年班学院) 获得应用数学和计算机双学士学位，于2023年在德克萨斯大学奥斯汀分校电子与计算机工程系获得博士学位，并于2024年在麻省理工学院和哈佛大学获得博士后学位。他的研究方向包括高效可靠的机器学习、大语言模型智能体、多模态学习以及科学AI。
韩衍隽
邓准
北卡罗来纳大学教堂山分校计算机科学系的助理教授。他于浙江大学竺可桢学院获得数学学士学位，2022年获得哈佛大学计算机科学博士学位（导师Cynthia Dwork），并于2022年至2024年在哥伦比亚大学担任博士后。他的研究兴趣涵盖机器学习、理论计算机科学和统计学的交叉领域。近期，他的研究方向为数学AI、人机协作以及智能体AI。
7、桥接证明和计算——经过验证的Lean–Macaulay2接口
项目简介
该项目致力于开发Lean与计算代数系统（CAS）Macaulay2（M2）之间的可扩展原生接口，以增强CAS与形式化证明验证的集成。通过创建一种基于Lean的领域特定语言（DSL）用于与M2交互，团队旨在实现无缝的双向通信，使Lean用户能够调用M2函数，M2用户也能够生成Lean证明。该项目还将致力于形式化M2中的关键算法，并探索为Lean开发通用的计算机代数系统接口，未来可能惠及其他CAS系统。
团队简介
马修·巴拉德（Matthew Ballard）
本科就读于加州理工学院数学系，后在美国华盛顿大学获得博士学位。在美国宾夕法尼亚大学、威斯康星大学麦迪逊分校和维也纳大学从事博士后研究后，他加入美国南卡罗来纳大学任教，现任该校数学系教授。他的研究兴趣包括数学中的导出范畴和数学的形式化。他是Lean定理证明器的主要数学库Mathlib的维护者之一。
安东·莱金（Anton Leykin）
本科就读于乌克兰哈尔科夫大学数学系，后在美国明尼苏达大学双城分校获得博士学位。在美国伊利诺伊大学芝加哥分校和明尼苏达州明尼阿波利斯市数学及其应用研究所从事博士后研究后，他加入美国佐治亚理工学院，现任数学学院教授。他的研究兴趣是非线性代数，着眼于算法及其应用。研究内容包括理论发展、在计算机代数系统Macaulay2中实现由此产生的算法，以及在数学、计算机科学和工程等其他领域的应用。
达米亚诺·泰斯塔（Damiano Testa）
本科就读于意大利罗马罗马大学，研究生就读于麻省理工学院。在康奈尔大学、罗马罗马大学、不来梅雅各布大学和牛津大学担任博士后后，他加入华威大学数学系任教。他的研究兴趣围绕代数几何、数论和数学形式化。他也是Lean定理证明器主要数学库Mathlib的维护者之一。
迈克尔·斯蒂尔曼（Michael Stillman）
本科就读于伊利诺伊大学，研究生就读于哈佛大学。在芝加哥大学、布兰迪斯大学和麻省理工学院担任博士后后，他加入康奈尔大学数学系任教。他的研究兴趣围绕计算代数几何，包括算法、实现和应用（例如生物学和理论物理学）。他是Macaulay2计算机代数系统的创始人之一。
8、定理证明的受约束大语言模型——一种保证自动形式化的神经符号方法
项目简介
该项目的目标是推进自动形式化——将非形式化数学转化为形式化陈述，并使其能够被Lean等最先进的证明助手自动检查。由于即使是最先进的模型，在生成语法正确的Lean陈述方面也只能取得有限的成功率，因此本项目将开发新型神经模块，通过构建生成正确的Lean代码。这些模块可以无缝集成到现有的LLM架构中，并可进行联合训练，从而提升整体性能。
团队简介
埃莉奥诺拉·朱奇利亚（Eleonora Giunchiglia）
伦敦帝国理工学院I-X项目和电气与电子工程系的助理教授。她的研究重点是通过将形式逻辑约束融入深度学习系统的设计中来增强其安全性和可信度。加入帝国理工学院之前，她于2022年在牛津大学获得博士学位，随后在维也纳工业大学担任博士后研究员。
萨姆·亚当-戴（Sam Adam-Day）
约书亚·翁（Joshua Ong）
伦敦帝国理工学院的一年级博士生，导师是Eleonora Giunchiglia博士。他的研究兴趣在于通过神经符号方法理解和提升大语言模型的推理能力。他的目标是确保LLM以可信、安全且可控的方式生成推理。
米哈埃拉·卡特利娜·斯托伊安（Mihaela Cătălina Stoian）
牛津大学计算机科学系的博士研究生，目前在读最后一年，致力于开发神经符号方法，该方法可在训练期间将背景知识约束集成到神经网络中，并在推理时强制执行。她的工作获得了多项奖项，包括由G-Research颁发的牛津大学博士生亚军奖。Mihaela的愿景是弥合神经符号AI与现实世界应用之间的差距，以构建更稳健、更值得信赖的系统。此前，她曾在Five AI从事3D模型中反射对称性的检测工作，并在爱丁堡大学获得了语音转文本机器翻译硕士学位。
卢卡·安多尔菲（Luca Andolfi）
他于2020年和2022年分别获得罗马大学计算机科学工程学士和硕士学位，并以优异成绩（110/110 cum laude）毕业。他目前正在罗马大学攻读意大利国家AI博士学位，导师是Marco Console教授。他的研究主要集中在增强知识表示方法的表达能力和提高神经符号机器学习模型的可靠性。
9、Isabelle副驾驶——学习逻辑结构以获得更好的证明体验
项目简介
Isabelle是最受欢迎的证明助手之一，在数学和计算机科学领域都取得了里程碑式的验证成果。作为一个汇聚了经验丰富的Isabelle设计师、开发者和用户以及AI专家的团队，我们将通过智能副驾驶扩展该系统，使其能够充分利用通过人机交互获取的大量高度结构化的信息。Isabelle将“更加关注”来自其高智能用户和开发者的数据，自身也将变得更加智能。这将催生出超越Isabelle的、与定理证明相关的全新AI问题。
团队简介
安德烈·波佩斯库（Andrei Popescu）
谢菲尔德大学计算机科学高级讲师（副教授）。此前，他曾在密德萨斯大学担任讲师，并在慕尼黑工业大学担任博士后研究员。他拥有伊利诺伊大学厄巴纳-香槟分校的计算机科学博士学位和布加勒斯特大学的数学博士学位。他热衷于为证明助手寻求更完善的逻辑基础和规范机制，他的大部分工作都为名为Isabelle/HOL的出色证明助手的归纳推理和协同归纳推理基础设施的开发提供了参考。他还参与了使用Isabelle进行形式化验证的开发，涵盖从哥德尔不完备定理等基础知识到应用信息流安全等各个方面。
德米特里·特雷特尔（Dmitriy Traytel）
哥本哈根大学计算机科学系 (DIKU) 的副教授。他于2015年在慕尼黑工业大学Tobias Nipkow的指导下获得博士学位，并在苏黎世联邦理工学院David Basin团队担任博士后研究员，任期至2020年。Dmitriy既是Isabelle证明助手的用户，也是其开发者，并担任Isabelle形式证明档案库的编辑。作为用户，Dmitriy目前的研究重点是可扩展数据流处理算法的验证。作为开发者，Dmitriy为Isabelle模块化归纳和共归纳数据类型（包括绑定感知变体）及其定义和推理基础设施的设计和实现做出了重要贡献。
穆罕默德·阿卜杜勒阿齐兹（Mohammad Abdulaziz）
伦敦国王学院信息学系的讲师（相当于助理教授）。在此之前，他曾在慕尼黑工业大学逻辑与验证系担任博士后研究员，任期至2022年。他于2018年获得澳大利亚国立大学博士学位。穆罕默德的研究领域包括两个：定理证明在形式验证和数学形式化中的应用；以及AI规划算法的设计。他在数学形式化方面的工作包括理论计算机科学中的形式化、规划语言的语义以及多元微积分。他还设计了新的AI规划算法，并验证了涵盖从简单、确定性、有限系统到大型、现实世界随机系统等各种场景的AI规划软件。
10、众包和重塑下一代动态可扩展数学基准（Benchmarks）
项目简介
该项目旨在创建一个社区驱动的平台，能够大规模生成、验证和迭代基准（benchmark）数学问题，从而简化AI在数学模型评估和数据获取方面的应用。该平台将利用半自动化工作流程，众包并验证复杂的数学问题，确保基准定期更新且不受污染。该项目的主要功能包括简化的问题提交、自动验证、专家评审和大语言模型（LLM）评估，所有这些都有助于构建一个充满活力的协作研发环境。
团队简介
詹姆斯·邹（James Zou）
斯坦福大学生物医学数据科学、计算机科学和电子工程系副教授。他致力于推进AI基础以及尖端科学和医学应用的发展。他曾获得斯隆奖学金、奥弗顿（Overton）奖、美国国家科学基金会杰出青年奖、两项陈-扎克伯格研究员奖、一项十大临床成就奖、多项最佳论文奖以及谷歌、亚马逊、Adobe和苹果颁发的研究奖。
姚骅修（原名姚臻昱）
北卡罗来纳大学教堂山分校计算机科学系助理教授，同时兼任数据科学与社会学院教授。他曾是斯坦福大学计算机科学博士后（之前系电子科技大学学士、宾夕法尼亚州立大学博士）。他目前的研究重点是开发具有广泛泛化能力且与人类偏好高度契合的智能体性、多模态基础模型。他的研究成果荣获多项荣誉，包括TMLR杰出论文奖、KDD 2024最佳论文奖、亚马逊研究奖、思科研究奖、AAAI 2024学术新星（New Faculty Highlights）奖、PharmAlliance早期职业研究员奖以及北卡罗来纳大学青年教师发展奖。
张林俊
罗格斯大学统计学系副教授。他于2019年在宾夕法尼亚大学沃顿商学院获得统计学博士学位，毕业时分别因在研究和教学方面的卓越贡献获得了J. Parker Bursk纪念奖和Donald S. Murray奖。他还于2024年获得了美国国家科学基金会杰出青年职业奖（NSF CAREER Award）和罗格斯大学校长教学奖。他目前的研究兴趣包括算法公平性、隐私保护数据分析、深度学习理论和高维统计。
大卫·佩诺克（David Pennock）
罗格斯大学DIMACS的主任和计算机科学教授，他在该校设计了人机交互市场机制，并开创了组合预测市场和真实投注；他早期在推荐系统、网络分析和赞助搜索方面的工作曾获得三项“时间考验”殊荣。他拥有AI博士学位，二十年来致力于塑造经济学和计算领域——共同创立了两个研究领域、三个研讨会、一本ACM期刊和三个企业研究实验室——同时还担任微软纽约研究院的董事主任助理。他发表了100多篇论文，申请了20多项专利，在主流媒体发表文章，并发表了50多场受邀演讲。
鲁盼
斯坦福大学的博士后研究员。他于2018年获得清华大学硕士学位（导师王建勇教授），2024年获得加州大学洛杉矶分校（UCLA）计算机科学博士学位。他的研究重点是开发AI方法和系统，以推进复杂推理、数学智能和科学发现。他曾担任NENLP 2025高级程序主席、SoCal NLP 2023程序主席以及NeurIPS MATHAI研讨会联合主席（2021 - 2024）。他曾荣获多项奖项，包括两项最具影响力论文奖（NeurIPS 2022、ICLR 2024）、ACL 2023最佳论文荣誉奖、KnowledgeNLP研讨会2025最佳论文奖，以及由亚马逊、彭博和高通资助的博士生奖学金。