★加星zzllrr小樂(lè)公眾號(hào)數(shù)學(xué)科普不迷路！

2025年9月17日——文藝復(fù)興慈善基金會(huì)和XTX Markets宣布從AI for Math Fund（數(shù)學(xué)AI基金）獲得1800 萬(wàn)美元的資助，這是有史以來(lái)最大的慈善投入之一，旨在支持開(kāi)發(fā)基于AI人工智能和機(jī)器學(xué)習(xí)的工具來(lái)推動(dòng)數(shù)學(xué)發(fā)展。

該基金首批29個(gè)獲獎(jiǎng)項(xiàng)目涵蓋大學(xué)和機(jī)構(gòu)的數(shù)學(xué)家和研究人員，他們致力于開(kāi)發(fā)有助于推進(jìn)多項(xiàng)關(guān)鍵任務(wù)的數(shù)學(xué)發(fā)現(xiàn)和研究的系統(tǒng)。這些項(xiàng)目包括前沿形式化數(shù)學(xué)數(shù)據(jù)集、促進(jìn)人工智能與數(shù)學(xué)協(xié)同作用的軟件工具，以及一些將人工智能應(yīng)用于基礎(chǔ)數(shù)學(xué)和應(yīng)用的高風(fēng)險(xiǎn)、高回報(bào)的構(gòu)想。資助金額最高可達(dá)100萬(wàn)美元。

作者：文藝復(fù)興慈善基金官網(wǎng)（Renaissance Philanthropy）2025-9-17

譯者：zzllrr小樂(lè)（數(shù)學(xué)科普公眾號(hào)）2025-9-24

該基金于2024年12月啟動(dòng)（參見(jiàn)），XTX Markets承諾注資900萬(wàn)美元，收到了來(lái)自世界各地研究人員和數(shù)學(xué)家團(tuán)隊(duì)的280份申請(qǐng)。由于申請(qǐng)質(zhì)量高，XTX Markets的資金規(guī)模翻了一番，達(dá)到1800萬(wàn)美元。

XTX Markets慈善事業(yè)主管Simon Coyle表示：“AI for Math 基金首輪的提案非常強(qiáng)勁，因此XTX Markets很高興將我們的初始資金翻倍。我們期待這些項(xiàng)目在未來(lái)一年內(nèi)陸續(xù)上線，并支持世界各地?cái)?shù)學(xué)家的工作?！?/p>

數(shù)學(xué)AI基金（AI for Math Fund）旨在通過(guò)支持那些對(duì)數(shù)學(xué)領(lǐng)域至關(guān)重要、但目前缺乏任何學(xué)術(shù)或產(chǎn)業(yè)實(shí)驗(yàn)室動(dòng)力去實(shí)施的項(xiàng)目，來(lái)加快數(shù)學(xué)探索的步伐并提升其影響力。

該基金支持那些在常規(guī)情況下不太可能實(shí)現(xiàn)，但有潛力推動(dòng)整個(gè)領(lǐng)域發(fā)展的項(xiàng)目。

這些項(xiàng)目包括：開(kāi)發(fā)開(kāi)源的、生產(chǎn)級(jí)質(zhì)量的工具；提升訓(xùn)練AI模型所需數(shù)據(jù)集的規(guī)模、多樣性和質(zhì)量；以及提升工具的易用性，使其更容易被數(shù)學(xué)家采用。

該基金的首批 29 項(xiàng)資助將頒發(fā)給大學(xué)和組織的研究人員，以支持他們開(kāi)發(fā)有助于推進(jìn)多項(xiàng)關(guān)鍵任務(wù)的數(shù)學(xué)發(fā)現(xiàn)和研究的系統(tǒng)。

首屆數(shù)學(xué)AI基金投資對(duì)象由研究人員、大學(xué)和組織組成，他們開(kāi)發(fā)的系統(tǒng)有助于推進(jìn)數(shù)學(xué)發(fā)現(xiàn)，涵蓋數(shù)學(xué)AI研究中的一系列關(guān)鍵主題和瓶頸，包括：

• 關(guān)鍵數(shù)據(jù)集開(kāi)發(fā)

• 改進(jìn)證明器與數(shù)學(xué)家之間的互動(dòng)

• 核心功能和覆蓋范圍的改進(jìn)

• 有前景的領(lǐng)域建設(shè)的倡議舉措

• 雄心勃勃的“登月計(jì)劃”

2025年獲選項(xiàng)目及團(tuán)隊(duì)介紹 (1~10)

（按項(xiàng)目英文名排序）

1、一種以AI為中心的語(yǔ)言學(xué)習(xí)策略

項(xiàng)目簡(jiǎn)介

該項(xiàng)目旨在通過(guò)開(kāi)發(fā)一種Lean領(lǐng)域特定策略語(yǔ)言來(lái)增強(qiáng)AI證明智能體，使其更好地與AI的能力和優(yōu)勢(shì)相匹配。通過(guò)分析AI生成證明與人工證明之間的結(jié)構(gòu)差異，該團(tuán)隊(duì)力求理解AI智能體的句法偏好，并據(jù)此提出更有針對(duì)性的AI優(yōu)先策略。這項(xiàng)工作將促成新策略的實(shí)施以及一個(gè)自動(dòng)形式化模型，以優(yōu)化AI的符號(hào)推理和搜索能力。

團(tuán)隊(duì)簡(jiǎn)介

羅伯特·Y·劉易斯（Robert Y. Lewis）

布朗大學(xué)計(jì)算機(jī)科學(xué)系的助理教授。他的研究興趣涉及Lean數(shù)學(xué)形式化驗(yàn)證，重點(diǎn)關(guān)注證明中使用的策略語(yǔ)言。他是Lean數(shù)學(xué)庫(kù)（Mathlib）的維護(hù)者，并已參與形式化數(shù)學(xué)項(xiàng)目十年。

2、一個(gè)現(xiàn)代形式化定理陳述的數(shù)據(jù)集

項(xiàng)目簡(jiǎn)介

該項(xiàng)目創(chuàng)建了一個(gè)公共數(shù)據(jù)集，其中包含數(shù)百個(gè)來(lái)自頂級(jí)期刊（例如《數(shù)學(xué)年鑒》）的最新定理的形式化陳述。此舉將解決數(shù)學(xué)研究前沿領(lǐng)域形式化不足的關(guān)鍵問(wèn)題。通過(guò)專門(mén)的專家形式化研究，該項(xiàng)目將顯著擴(kuò)展形式化數(shù)學(xué)庫(kù)，并為AI系統(tǒng)在各種任務(wù)上提供清晰的目標(biāo)，包括自動(dòng)形式化證明和協(xié)助人類進(jìn)行證明形式化。

團(tuán)隊(duì)簡(jiǎn)介

凱文·巴扎德（Kevin Buzzard）

倫敦帝國(guó)理工學(xué)院的代數(shù)數(shù)論學(xué)家。他目前正在研究費(fèi)馬大定理的Lean形式化。他在2022年國(guó)際數(shù)學(xué)家大會(huì)上發(fā)表了關(guān)于交互式定理證明器的全體會(huì)議報(bào)告。

參閱

以及

3、一種搜索證明的原則性方法及其在Siderenko（西多連科）猜想中的應(yīng)用

項(xiàng)目簡(jiǎn)介

本項(xiàng)目提出了新的證明方法，旨在自動(dòng)化和簡(jiǎn)化重大未解問(wèn)題的證明發(fā)現(xiàn)過(guò)程。為此，本工作旨在建立一個(gè)嚴(yán)謹(jǐn)?shù)睦碚摽蚣堋⒅踩胄宰C明，并開(kāi)發(fā)新的算法，以高效且可擴(kuò)展地推導(dǎo)出開(kāi)放問(wèn)題的證明。作為概念驗(yàn)證，本項(xiàng)目將專注于創(chuàng)建一種理論上合理的方法來(lái)尋找可滿足性 (SAT) 公式的解析證明，并開(kāi)發(fā)機(jī)器學(xué)習(xí)工具來(lái)解決組合數(shù)學(xué)中一個(gè)關(guān)鍵的開(kāi)放問(wèn)題——Siderenko猜想。通過(guò)彌合這些差距，本項(xiàng)目有望推動(dòng)AI在數(shù)學(xué)領(lǐng)域的理論和實(shí)踐發(fā)展。

團(tuán)隊(duì)簡(jiǎn)介

普拉維什·K·科塔里（Pravesh K Kothari）

普林斯頓大學(xué)計(jì)算機(jī)科學(xué)系的助理教授。此前，他曾擔(dān)任卡內(nèi)基梅隆大學(xué)計(jì)算機(jī)科學(xué)系助理教授，并于2016年至2019年期間擔(dān)任普林斯頓高等研究院和普林斯頓大學(xué)計(jì)算機(jī)科學(xué)系聯(lián)合舉辦的計(jì)算機(jī)科學(xué)研究講師。Kothari博士的研究興趣涵蓋理論計(jì)算機(jī)科學(xué)的多個(gè)主題，例如凸優(yōu)化及其在算法設(shè)計(jì)中的應(yīng)用、統(tǒng)計(jì)估計(jì)和平均情況組合優(yōu)化的算法和下界，以及譜方法及其與隨機(jī)矩陣?yán)碚?、編碼理論和極值組合學(xué)的聯(lián)系。Kothari博士曾獲得普雷斯堡（Presburger）獎(jiǎng)（2024年）、印度理工學(xué)院坎普爾分校青年校友獎(jiǎng)（2023年）、斯隆獎(jiǎng)學(xué)金（2022年）和美國(guó)國(guó)家科學(xué)基金會(huì)職業(yè)獎(jiǎng)（2021年）。

拉古·梅卡（Raghu Meka）

加州大學(xué)洛杉磯分校 (UCLA) 計(jì)算機(jī)科學(xué)教授。Meka教授在德克薩斯大學(xué)奧斯汀分校獲得博士學(xué)位，并在普林斯頓高等研究院和羅格斯大學(xué)DIMACS獲得博士后研究。Meka教授的研究領(lǐng)域涵蓋概率論、學(xué)習(xí)理論、組合數(shù)學(xué)和理論計(jì)算機(jī)科學(xué)的交叉領(lǐng)域。他是2025年IEEE W. Wallace MacDowelll獎(jiǎng)的獲得者。他還曾獲得2023年IEEE計(jì)算機(jī)科學(xué)基礎(chǔ)研討會(huì) (FOCS) 和2024年學(xué)習(xí)理論會(huì)議 (COLT) 的最佳論文獎(jiǎng)。

4、一種機(jī)器輔助定理證明策略的結(jié)構(gòu)化表示

項(xiàng)目簡(jiǎn)介

本項(xiàng)目開(kāi)發(fā)了一種機(jī)器學(xué)習(xí)驅(qū)動(dòng)的方法來(lái)創(chuàng)建交互式定理證明策略。該項(xiàng)目將策略表示為高級(jí)語(yǔ)言中的代數(shù)對(duì)象，一旦應(yīng)用，就會(huì)修改證明狀態(tài)。反過(guò)來(lái)，這種語(yǔ)言可以轉(zhuǎn)換為L(zhǎng)ean元程序，并將促進(jìn)大語(yǔ)言模型通過(guò)交互式會(huì)話自動(dòng)創(chuàng)建證明腳本。通過(guò)這項(xiàng)工作，該項(xiàng)目希望發(fā)現(xiàn)新的證明策略，從而進(jìn)一步簡(jiǎn)化定理證明工作。

團(tuán)隊(duì)簡(jiǎn)介

杰德·馬斯特（Jade Master）

擁有應(yīng)用范疇論博士學(xué)位，專攻復(fù)雜系統(tǒng)的組合性。在完成余代數(shù)形式驗(yàn)證博士后研究并擔(dān)任函數(shù)式程序員后，她擔(dān)任ARIA Safeguarded AI項(xiàng)目的首席研究員。她在ARIA（英國(guó)高級(jí)研究與發(fā)明局）的項(xiàng)目旨在開(kāi)發(fā)基于范疇形式主義的可擴(kuò)展世界模型。她計(jì)劃通過(guò)開(kāi)發(fā)用于策略生成的組合技術(shù)，將這項(xiàng)工作與Containers for AI（AI容器）項(xiàng)目結(jié)合起來(lái)。

文森特·王-馬希西亞尼卡（Vincent Wang-Ma?cianica）

在牛津大學(xué)獲得博士學(xué)位，研究重點(diǎn)是連接實(shí)用計(jì)算語(yǔ)義和形式組合結(jié)構(gòu)的幺半范疇理論。他目前是牛津大學(xué)哲學(xué)系以人為中心AI實(shí)驗(yàn)室的高級(jí)研究員。

贊齊·米赫耶夫斯（Zanzi Mihejevs）

擁有超過(guò)10年使用函數(shù)式編程形式化各種范疇結(jié)構(gòu)的經(jīng)驗(yàn)，并且在為咨詢公司構(gòu)建領(lǐng)域特定語(yǔ)言方面擁有豐富的經(jīng)驗(yàn)。她是Glaive的ARIA資助項(xiàng)目的首席研究員，致力于構(gòu)建一種利用范疇論推動(dòng)編程前沿發(fā)展的編程語(yǔ)言。

布魯諾·加夫拉諾維奇（Bruno Gavranovi?）

Bruno Gavranovi?博士，是一位數(shù)學(xué)家和計(jì)算機(jī)科學(xué)家，他通過(guò)與Google DeepMind合作開(kāi)展的研究以及其博士論文《深度學(xué)習(xí)的基本組成部分：一種范疇論方法》開(kāi)創(chuàng)了范疇深度學(xué)習(xí)。他將這一理論成果轉(zhuǎn)化為實(shí)際成果，在為 Symbolica AI 爭(zhēng)取3100萬(wàn)美元融資的過(guò)程中發(fā)揮了關(guān)鍵作用，并創(chuàng)立了Coend公司。Coend是一家開(kāi)發(fā)用于一等類型編程語(yǔ)言代碼生成的基礎(chǔ)模型的公司。

安德烈·維德拉（Andre Videla）

思克萊德大學(xué)博士生，也是Glaive的研究員。他致力于容器、交互系統(tǒng)和編程的未來(lái)發(fā)展，并參與開(kāi)發(fā)和維護(hù)Idris編程語(yǔ)言。Andre的工作將抽象的范疇思維與實(shí)際的編程經(jīng)驗(yàn)相結(jié)合，為現(xiàn)代軟件挑戰(zhàn)提供了新的解決方案。

迪倫·布雷斯韋特（Dylan Braithwaite）

目前正在攻讀理論計(jì)算機(jī)科學(xué)博士學(xué)位。他擁有編程語(yǔ)言的范疇語(yǔ)義學(xué)和概率編程方面的經(jīng)驗(yàn)，并曾擔(dān)任軟件開(kāi)發(fā)人員。作為Glaive的成員，他一直在研究ARIA資助的項(xiàng)目，致力于實(shí)現(xiàn)一種使用范疇結(jié)構(gòu)以更符合人體工程學(xué)的方式表示數(shù)學(xué)結(jié)構(gòu)的編程語(yǔ)言。

5、橋接AI、證明助手和數(shù)學(xué)數(shù)據(jù)（BRIDGE）

項(xiàng)目簡(jiǎn)介

BRIDGE項(xiàng)目旨在通過(guò)創(chuàng)建和管理來(lái)自形式化數(shù)學(xué)庫(kù)的大規(guī)模數(shù)據(jù)集和依賴關(guān)系圖，將AI與證明助手和數(shù)學(xué)數(shù)據(jù)相結(jié)合。該團(tuán)隊(duì)將開(kāi)發(fā)基于AI的工具，以支持?jǐn)?shù)學(xué)結(jié)構(gòu)、證明及其相互依賴關(guān)系的形式化和探索。這些工具（包括推薦系統(tǒng)和用戶引導(dǎo)的發(fā)現(xiàn)功能）有望提高數(shù)學(xué)推理的可訪問(wèn)性和效率。

團(tuán)隊(duì)簡(jiǎn)介

安德烈·鮑爾（Andrej Bauer）

斯洛文尼亞盧布爾雅那數(shù)學(xué)、物理與力學(xué)研究所理論計(jì)算機(jī)科學(xué)系主任，同時(shí)也是盧布爾雅那大學(xué)的計(jì)算數(shù)學(xué)教授。鮑爾的研究領(lǐng)域涵蓋數(shù)學(xué)基礎(chǔ)、構(gòu)造性數(shù)學(xué)和可計(jì)算數(shù)學(xué)、類型論、同倫類型論、形式化數(shù)學(xué)以及編程語(yǔ)言的數(shù)學(xué)原理。他還因其在代數(shù)效應(yīng)和處理程序編程方面的開(kāi)創(chuàng)性工作而聞名。

普里莫日·波托奇尼克（Primo? Poto?nik）

盧布爾雅那數(shù)學(xué)、物理和力學(xué)研究所計(jì)算密集型數(shù)學(xué)方法研究小組的負(fù)責(zé)人，同時(shí)也是斯洛文尼亞盧布爾雅那大學(xué)的數(shù)學(xué)教授。他的研究重點(diǎn)是組合和代數(shù)結(jié)構(gòu)中的對(duì)稱性。他因其高度對(duì)稱的圖形和地圖數(shù)據(jù)集而在數(shù)學(xué)界享有盛譽(yù)。

柳普喬·托多羅夫斯基（Ljup?o Todorovski）

盧布爾雅那大學(xué)數(shù)學(xué)與物理學(xué)院的計(jì)算機(jī)科學(xué)教授。他的研究興趣在于AI，尤其專注于開(kāi)發(fā)機(jī)器學(xué)習(xí)算法，用于從實(shí)驗(yàn)數(shù)據(jù)中計(jì)算發(fā)現(xiàn)科學(xué)知識(shí)和模型。最近，他一直與數(shù)學(xué)家合作，設(shè)計(jì)支持使用證明助手進(jìn)行數(shù)學(xué)形式化的AI工具。

丹尼爾·阿赫曼（Danel Ahman）

愛(ài)沙尼亞塔爾圖大學(xué)計(jì)算機(jī)科學(xué)學(xué)院的編程語(yǔ)言副教授。他的研究重點(diǎn)是編程語(yǔ)言理論，特別是具有高級(jí)類型系統(tǒng)的編程語(yǔ)言的設(shè)計(jì)和元理論。他致力于使用類型來(lái)形式化地指定和驗(yàn)證程序使用數(shù)據(jù)和資源的方式和時(shí)間，開(kāi)發(fā)用于數(shù)據(jù)結(jié)構(gòu)的組合類型理論模型，并應(yīng)用這些技術(shù)構(gòu)建correct-by-constrction（按構(gòu)建逐步校正）且經(jīng)過(guò)驗(yàn)證的軟件。

卡佳·貝爾奇奇（Katja Ber?i?）

斯洛文尼亞盧布爾雅那大學(xué)數(shù)學(xué)、物理和力學(xué)研究所的研究員，同時(shí)也是該大學(xué)的助教。她致力于開(kāi)發(fā)穩(wěn)健且可互操作的數(shù)學(xué)數(shù)據(jù)基礎(chǔ)設(shè)施，并將其與數(shù)學(xué)軟件集成。她的工作基于對(duì)數(shù)學(xué)家在實(shí)踐中如何創(chuàng)建、構(gòu)造和與數(shù)據(jù)交互的分析。她還研究了這些活動(dòng)與更廣泛的研究數(shù)據(jù)管理背景之間的關(guān)系。

6、橋接復(fù)雜性和自動(dòng)化以推進(jìn)自動(dòng)定理證明

項(xiàng)目簡(jiǎn)介

本項(xiàng)目通過(guò)三個(gè)創(chuàng)新研究方向?qū)崿F(xiàn)定理證明的自動(dòng)化，這些方向解決了關(guān)于證明難度、可處理性和性能擴(kuò)展性的關(guān)鍵概念問(wèn)題。具體而言，本項(xiàng)目將研究并尋求形式化定義：

1. 從計(jì)算復(fù)雜性的角度看，證明任務(wù)的難度

2. 解決給定的證明任務(wù)需要多少數(shù)據(jù)（真實(shí)的和/或合成的）

3. 證明復(fù)雜性如何隨可用計(jì)算資源的變化而變化

團(tuán)隊(duì)簡(jiǎn)介

托尼安·皮塔西（Toniann Pitassi）

哥倫比亞大學(xué)計(jì)算機(jī)科學(xué)系的Jeffrey L.和Brenda Bleustein工程學(xué)教授。在2020年加入哥倫比亞大學(xué)之前，Pitassi曾擔(dān)任多倫多大學(xué)的貝爾加拿大計(jì)算機(jī)科學(xué)研究主席。她的主要研究方向是證明復(fù)雜性、復(fù)雜性理論以及機(jī)器學(xué)習(xí)的基礎(chǔ)主題，包括隱私、公平性和自適應(yīng)數(shù)據(jù)分析。Pitassi是美國(guó)國(guó)家科學(xué)院院士，也是ACM會(huì)士。

理查德·澤梅爾（Richard Zemel）

哥倫比亞大學(xué)計(jì)算機(jī)科學(xué)系Trianthe Dakolias工程與應(yīng)用科學(xué)教授。他是美國(guó)國(guó)家科學(xué)基金會(huì)AI與自然智能研究所 (ARNI) 的主任，也是向量AI研究所的聯(lián)合創(chuàng)始人兼首任研究主任。他擔(dān)任加拿大高級(jí)研究院AI主席，并擔(dān)任神經(jīng)信息處理學(xué)會(huì)顧問(wèn)委員會(huì)成員。他的研究貢獻(xiàn)包括：在極少或完全無(wú)監(jiān)督的情況下學(xué)習(xí)有用數(shù)據(jù)表示的系統(tǒng)的基礎(chǔ)性工作；基于圖的機(jī)器學(xué)習(xí)；以及公平穩(wěn)健的機(jī)器學(xué)習(xí)算法。

陳天龍

北卡羅來(lái)納大學(xué)教堂山分校計(jì)算機(jī)科學(xué)系的助理教授。他于2017年在中國(guó)科學(xué)技術(shù)大學(xué) (少年班學(xué)院) 獲得應(yīng)用數(shù)學(xué)和計(jì)算機(jī)雙學(xué)士學(xué)位，于2023年在德克薩斯大學(xué)奧斯汀分校電子與計(jì)算機(jī)工程系獲得博士學(xué)位，并于2024年在麻省理工學(xué)院和哈佛大學(xué)獲得博士后學(xué)位。他的研究方向包括高效可靠的機(jī)器學(xué)習(xí)、大語(yǔ)言模型智能體、多模態(tài)學(xué)習(xí)以及科學(xué)AI。

韓衍雋

紐約大學(xué)柯朗數(shù)學(xué)科學(xué)研究所和數(shù)據(jù)科學(xué)中心的數(shù)學(xué)與數(shù)據(jù)科學(xué)助理教授。他于2021年獲得斯坦福大學(xué)電氣工程博士學(xué)位（之前系2011年安徽省高考理科狀元——705分，保送清華大學(xué)電子工程系），并在加州大學(xué)伯克利分校西蒙斯計(jì)算理論研究所和麻省理工學(xué)院統(tǒng)計(jì)與數(shù)據(jù)科學(xué)中心工作多年。他對(duì)數(shù)據(jù)科學(xué)的數(shù)學(xué)有著廣泛的興趣，包括統(tǒng)計(jì)學(xué)、學(xué)習(xí)理論、強(qiáng)盜算法和信息論。

鄧準(zhǔn)

北卡羅來(lái)納大學(xué)教堂山分校計(jì)算機(jī)科學(xué)系的助理教授。他于浙江大學(xué)竺可楨學(xué)院獲得數(shù)學(xué)學(xué)士學(xué)位，2022年獲得哈佛大學(xué)計(jì)算機(jī)科學(xué)博士學(xué)位（導(dǎo)師Cynthia Dwork），并于2022年至2024年在哥倫比亞大學(xué)擔(dān)任博士后。他的研究興趣涵蓋機(jī)器學(xué)習(xí)、理論計(jì)算機(jī)科學(xué)和統(tǒng)計(jì)學(xué)的交叉領(lǐng)域。近期，他的研究方向?yàn)閿?shù)學(xué)AI、人機(jī)協(xié)作以及智能體AI。

7、橋接證明和計(jì)算——經(jīng)過(guò)驗(yàn)證的Lean–Macaulay2接口

項(xiàng)目簡(jiǎn)介

該項(xiàng)目致力于開(kāi)發(fā)Lean與計(jì)算代數(shù)系統(tǒng)（CAS）Macaulay2（M2）之間的可擴(kuò)展原生接口，以增強(qiáng)CAS與形式化證明驗(yàn)證的集成。通過(guò)創(chuàng)建一種基于Lean的領(lǐng)域特定語(yǔ)言（DSL）用于與M2交互，團(tuán)隊(duì)旨在實(shí)現(xiàn)無(wú)縫的雙向通信，使Lean用戶能夠調(diào)用M2函數(shù)，M2用戶也能夠生成Lean證明。該項(xiàng)目還將致力于形式化M2中的關(guān)鍵算法，并探索為L(zhǎng)ean開(kāi)發(fā)通用的計(jì)算機(jī)代數(shù)系統(tǒng)接口，未來(lái)可能惠及其他CAS系統(tǒng)。

團(tuán)隊(duì)簡(jiǎn)介

馬修·巴拉德（Matthew Ballard）

本科就讀于加州理工學(xué)院數(shù)學(xué)系，后在美國(guó)華盛頓大學(xué)獲得博士學(xué)位。在美國(guó)賓夕法尼亞大學(xué)、威斯康星大學(xué)麥迪遜分校和維也納大學(xué)從事博士后研究后，他加入美國(guó)南卡羅來(lái)納大學(xué)任教，現(xiàn)任該校數(shù)學(xué)系教授。他的研究興趣包括數(shù)學(xué)中的導(dǎo)出范疇和數(shù)學(xué)的形式化。他是Lean定理證明器的主要數(shù)學(xué)庫(kù)Mathlib的維護(hù)者之一。

安東·萊金（Anton Leykin）

本科就讀于烏克蘭哈爾科夫大學(xué)數(shù)學(xué)系，后在美國(guó)明尼蘇達(dá)大學(xué)雙城分校獲得博士學(xué)位。在美國(guó)伊利諾伊大學(xué)芝加哥分校和明尼蘇達(dá)州明尼阿波利斯市數(shù)學(xué)及其應(yīng)用研究所從事博士后研究后，他加入美國(guó)佐治亞理工學(xué)院，現(xiàn)任數(shù)學(xué)學(xué)院教授。他的研究興趣是非線性代數(shù)，著眼于算法及其應(yīng)用。研究?jī)?nèi)容包括理論發(fā)展、在計(jì)算機(jī)代數(shù)系統(tǒng)Macaulay2中實(shí)現(xiàn)由此產(chǎn)生的算法，以及在數(shù)學(xué)、計(jì)算機(jī)科學(xué)和工程等其他領(lǐng)域的應(yīng)用。

達(dá)米亞諾·泰斯塔（Damiano Testa）

本科就讀于意大利羅馬羅馬大學(xué)，研究生就讀于麻省理工學(xué)院。在康奈爾大學(xué)、羅馬羅馬大學(xué)、不來(lái)梅雅各布大學(xué)和牛津大學(xué)擔(dān)任博士后后，他加入華威大學(xué)數(shù)學(xué)系任教。他的研究興趣圍繞代數(shù)幾何、數(shù)論和數(shù)學(xué)形式化。他也是Lean定理證明器主要數(shù)學(xué)庫(kù)Mathlib的維護(hù)者之一。

邁克爾·斯蒂爾曼（Michael Stillman）

本科就讀于伊利諾伊大學(xué)，研究生就讀于哈佛大學(xué)。在芝加哥大學(xué)、布蘭迪斯大學(xué)和麻省理工學(xué)院擔(dān)任博士后后，他加入康奈爾大學(xué)數(shù)學(xué)系任教。他的研究興趣圍繞計(jì)算代數(shù)幾何，包括算法、實(shí)現(xiàn)和應(yīng)用（例如生物學(xué)和理論物理學(xué)）。他是Macaulay2計(jì)算機(jī)代數(shù)系統(tǒng)的創(chuàng)始人之一。

8、定理證明的受約束大語(yǔ)言模型——一種保證自動(dòng)形式化的神經(jīng)符號(hào)方法

項(xiàng)目簡(jiǎn)介

該項(xiàng)目的目標(biāo)是推進(jìn)自動(dòng)形式化——將非形式化數(shù)學(xué)轉(zhuǎn)化為形式化陳述，并使其能夠被Lean等最先進(jìn)的證明助手自動(dòng)檢查。由于即使是最先進(jìn)的模型，在生成語(yǔ)法正確的Lean陳述方面也只能取得有限的成功率，因此本項(xiàng)目將開(kāi)發(fā)新型神經(jīng)模塊，通過(guò)構(gòu)建生成正確的Lean代碼。這些模塊可以無(wú)縫集成到現(xiàn)有的LLM架構(gòu)中，并可進(jìn)行聯(lián)合訓(xùn)練，從而提升整體性能。

團(tuán)隊(duì)簡(jiǎn)介

埃莉奧諾拉·朱奇利亞（Eleonora Giunchiglia）

倫敦帝國(guó)理工學(xué)院I-X項(xiàng)目和電氣與電子工程系的助理教授。她的研究重點(diǎn)是通過(guò)將形式邏輯約束融入深度學(xué)習(xí)系統(tǒng)的設(shè)計(jì)中來(lái)增強(qiáng)其安全性和可信度。加入帝國(guó)理工學(xué)院之前，她于2022年在牛津大學(xué)獲得博士學(xué)位，隨后在維也納工業(yè)大學(xué)擔(dān)任博士后研究員。

薩姆·亞當(dāng)-戴（Sam Adam-Day）

AI安全研究員。在獲得數(shù)學(xué)集合論博士學(xué)位后，他在牛津大學(xué)計(jì)算機(jī)科學(xué)系從事博士后研究，專注于圖神經(jīng)網(wǎng)絡(luò)的理論研究。目前，他正在進(jìn)行一個(gè)機(jī)器學(xué)習(xí)與博弈論交叉領(lǐng)域的獨(dú)立研究項(xiàng)目。他即將在非營(yíng)利性AI安全研究機(jī)構(gòu) FAR.AI 擔(dān)任研究科學(xué)家。

約書(shū)亞·翁（Joshua Ong）

倫敦帝國(guó)理工學(xué)院的一年級(jí)博士生，導(dǎo)師是Eleonora Giunchiglia博士。他的研究興趣在于通過(guò)神經(jīng)符號(hào)方法理解和提升大語(yǔ)言模型的推理能力。他的目標(biāo)是確保LLM以可信、安全且可控的方式生成推理。

米哈埃拉·卡特利娜·斯托伊安（Mihaela C?t?lina Stoian）

牛津大學(xué)計(jì)算機(jī)科學(xué)系的博士研究生，目前在讀最后一年，致力于開(kāi)發(fā)神經(jīng)符號(hào)方法，該方法可在訓(xùn)練期間將背景知識(shí)約束集成到神經(jīng)網(wǎng)絡(luò)中，并在推理時(shí)強(qiáng)制執(zhí)行。她的工作獲得了多項(xiàng)獎(jiǎng)項(xiàng)，包括由G-Research頒發(fā)的牛津大學(xué)博士生亞軍獎(jiǎng)。Mihaela的愿景是彌合神經(jīng)符號(hào)AI與現(xiàn)實(shí)世界應(yīng)用之間的差距，以構(gòu)建更穩(wěn)健、更值得信賴的系統(tǒng)。此前，她曾在Five AI從事3D模型中反射對(duì)稱性的檢測(cè)工作，并在愛(ài)丁堡大學(xué)獲得了語(yǔ)音轉(zhuǎn)文本機(jī)器翻譯碩士學(xué)位。

盧卡·安多爾菲（Luca Andolfi）

他于2020年和2022年分別獲得羅馬大學(xué)計(jì)算機(jī)科學(xué)工程學(xué)士和碩士學(xué)位，并以優(yōu)異成績(jī)（110/110 cum laude）畢業(yè)。他目前正在羅馬大學(xué)攻讀意大利國(guó)家AI博士學(xué)位，導(dǎo)師是Marco Console教授。他的研究主要集中在增強(qiáng)知識(shí)表示方法的表達(dá)能力和提高神經(jīng)符號(hào)機(jī)器學(xué)習(xí)模型的可靠性。

9、Isabelle副駕駛——學(xué)習(xí)邏輯結(jié)構(gòu)以獲得更好的證明體驗(yàn)

項(xiàng)目簡(jiǎn)介

Isabelle是最受歡迎的證明助手之一，在數(shù)學(xué)和計(jì)算機(jī)科學(xué)領(lǐng)域都取得了里程碑式的驗(yàn)證成果。作為一個(gè)匯聚了經(jīng)驗(yàn)豐富的Isabelle設(shè)計(jì)師、開(kāi)發(fā)者和用戶以及AI專家的團(tuán)隊(duì)，我們將通過(guò)智能副駕駛擴(kuò)展該系統(tǒng)，使其能夠充分利用通過(guò)人機(jī)交互獲取的大量高度結(jié)構(gòu)化的信息。Isabelle將“更加關(guān)注”來(lái)自其高智能用戶和開(kāi)發(fā)者的數(shù)據(jù)，自身也將變得更加智能。這將催生出超越Isabelle的、與定理證明相關(guān)的全新AI問(wèn)題。

團(tuán)隊(duì)簡(jiǎn)介

安德烈·波佩斯庫(kù)（Andrei Popescu）

謝菲爾德大學(xué)計(jì)算機(jī)科學(xué)高級(jí)講師（副教授）。此前，他曾在密德薩斯大學(xué)擔(dān)任講師，并在慕尼黑工業(yè)大學(xué)擔(dān)任博士后研究員。他擁有伊利諾伊大學(xué)厄巴納-香檳分校的計(jì)算機(jī)科學(xué)博士學(xué)位和布加勒斯特大學(xué)的數(shù)學(xué)博士學(xué)位。他熱衷于為證明助手尋求更完善的邏輯基礎(chǔ)和規(guī)范機(jī)制，他的大部分工作都為名為Isabelle/HOL的出色證明助手的歸納推理和協(xié)同歸納推理基礎(chǔ)設(shè)施的開(kāi)發(fā)提供了參考。他還參與了使用Isabelle進(jìn)行形式化驗(yàn)證的開(kāi)發(fā)，涵蓋從哥德?tīng)柌煌陚涠ɡ淼然A(chǔ)知識(shí)到應(yīng)用信息流安全等各個(gè)方面。

德米特里·特雷特爾（Dmitriy Traytel）

哥本哈根大學(xué)計(jì)算機(jī)科學(xué)系 (DIKU) 的副教授。他于2015年在慕尼黑工業(yè)大學(xué)Tobias Nipkow的指導(dǎo)下獲得博士學(xué)位，并在蘇黎世聯(lián)邦理工學(xué)院David Basin團(tuán)隊(duì)擔(dān)任博士后研究員，任期至2020年。Dmitriy既是Isabelle證明助手的用戶，也是其開(kāi)發(fā)者，并擔(dān)任Isabelle形式證明檔案庫(kù)的編輯。作為用戶，Dmitriy目前的研究重點(diǎn)是可擴(kuò)展數(shù)據(jù)流處理算法的驗(yàn)證。作為開(kāi)發(fā)者，Dmitriy為Isabelle模塊化歸納和共歸納數(shù)據(jù)類型（包括綁定感知變體）及其定義和推理基礎(chǔ)設(shè)施的設(shè)計(jì)和實(shí)現(xiàn)做出了重要貢獻(xiàn)。

穆罕默德·阿卜杜勒阿齊茲（Mohammad Abdulaziz）

倫敦國(guó)王學(xué)院信息學(xué)系的講師（相當(dāng)于助理教授）。在此之前，他曾在慕尼黑工業(yè)大學(xué)邏輯與驗(yàn)證系擔(dān)任博士后研究員，任期至2022年。他于2018年獲得澳大利亞國(guó)立大學(xué)博士學(xué)位。穆罕默德的研究領(lǐng)域包括兩個(gè)：定理證明在形式驗(yàn)證和數(shù)學(xué)形式化中的應(yīng)用；以及AI規(guī)劃算法的設(shè)計(jì)。他在數(shù)學(xué)形式化方面的工作包括理論計(jì)算機(jī)科學(xué)中的形式化、規(guī)劃語(yǔ)言的語(yǔ)義以及多元微積分。他還設(shè)計(jì)了新的AI規(guī)劃算法，并驗(yàn)證了涵蓋從簡(jiǎn)單、確定性、有限系統(tǒng)到大型、現(xiàn)實(shí)世界隨機(jī)系統(tǒng)等各種場(chǎng)景的AI規(guī)劃軟件。

10、眾包和重塑下一代動(dòng)態(tài)可擴(kuò)展數(shù)學(xué)基準(zhǔn)（Benchmarks）

項(xiàng)目簡(jiǎn)介

該項(xiàng)目旨在創(chuàng)建一個(gè)社區(qū)驅(qū)動(dòng)的平臺(tái)，能夠大規(guī)模生成、驗(yàn)證和迭代基準(zhǔn)（benchmark）數(shù)學(xué)問(wèn)題，從而簡(jiǎn)化AI在數(shù)學(xué)模型評(píng)估和數(shù)據(jù)獲取方面的應(yīng)用。該平臺(tái)將利用半自動(dòng)化工作流程，眾包并驗(yàn)證復(fù)雜的數(shù)學(xué)問(wèn)題，確保基準(zhǔn)定期更新且不受污染。該項(xiàng)目的主要功能包括簡(jiǎn)化的問(wèn)題提交、自動(dòng)驗(yàn)證、專家評(píng)審和大語(yǔ)言模型（LLM）評(píng)估，所有這些都有助于構(gòu)建一個(gè)充滿活力的協(xié)作研發(fā)環(huán)境。

團(tuán)隊(duì)簡(jiǎn)介

詹姆斯·鄒（James Zou）

斯坦福大學(xué)生物醫(yī)學(xué)數(shù)據(jù)科學(xué)、計(jì)算機(jī)科學(xué)和電子工程系副教授。他致力于推進(jìn)AI基礎(chǔ)以及尖端科學(xué)和醫(yī)學(xué)應(yīng)用的發(fā)展。他曾獲得斯隆獎(jiǎng)學(xué)金、奧弗頓（Overton）獎(jiǎng)、美國(guó)國(guó)家科學(xué)基金會(huì)杰出青年獎(jiǎng)、兩項(xiàng)陳-扎克伯格研究員獎(jiǎng)、一項(xiàng)十大臨床成就獎(jiǎng)、多項(xiàng)最佳論文獎(jiǎng)以及谷歌、亞馬遜、Adobe和蘋(píng)果頒發(fā)的研究獎(jiǎng)。

姚驊修（原名姚臻昱）

北卡羅來(lái)納大學(xué)教堂山分校計(jì)算機(jī)科學(xué)系助理教授，同時(shí)兼任數(shù)據(jù)科學(xué)與社會(huì)學(xué)院教授。他曾是斯坦福大學(xué)計(jì)算機(jī)科學(xué)博士后（之前系電子科技大學(xué)學(xué)士、賓夕法尼亞州立大學(xué)博士）。他目前的研究重點(diǎn)是開(kāi)發(fā)具有廣泛泛化能力且與人類偏好高度契合的智能體性、多模態(tài)基礎(chǔ)模型。他的研究成果榮獲多項(xiàng)榮譽(yù)，包括TMLR杰出論文獎(jiǎng)、KDD 2024最佳論文獎(jiǎng)、亞馬遜研究獎(jiǎng)、思科研究獎(jiǎng)、AAAI 2024學(xué)術(shù)新星（New Faculty Highlights）獎(jiǎng)、PharmAlliance早期職業(yè)研究員獎(jiǎng)以及北卡羅來(lái)納大學(xué)青年教師發(fā)展獎(jiǎng)。

張林俊

羅格斯大學(xué)統(tǒng)計(jì)學(xué)系副教授。他于2019年在賓夕法尼亞大學(xué)沃頓商學(xué)院獲得統(tǒng)計(jì)學(xué)博士學(xué)位，畢業(yè)時(shí)分別因在研究和教學(xué)方面的卓越貢獻(xiàn)獲得了J. Parker Bursk紀(jì)念獎(jiǎng)和Donald S. Murray獎(jiǎng)。他還于2024年獲得了美國(guó)國(guó)家科學(xué)基金會(huì)杰出青年職業(yè)獎(jiǎng)（NSF CAREER Award）和羅格斯大學(xué)校長(zhǎng)教學(xué)獎(jiǎng)。他目前的研究興趣包括算法公平性、隱私保護(hù)數(shù)據(jù)分析、深度學(xué)習(xí)理論和高維統(tǒng)計(jì)。

大衛(wèi)·佩諾克（David Pennock）

羅格斯大學(xué)DIMACS的主任和計(jì)算機(jī)科學(xué)教授，他在該校設(shè)計(jì)了人機(jī)交互市場(chǎng)機(jī)制，并開(kāi)創(chuàng)了組合預(yù)測(cè)市場(chǎng)和真實(shí)投注；他早期在推薦系統(tǒng)、網(wǎng)絡(luò)分析和贊助搜索方面的工作曾獲得三項(xiàng)“時(shí)間考驗(yàn)”殊榮。他擁有AI博士學(xué)位，二十年來(lái)致力于塑造經(jīng)濟(jì)學(xué)和計(jì)算領(lǐng)域——共同創(chuàng)立了兩個(gè)研究領(lǐng)域、三個(gè)研討會(huì)、一本ACM期刊和三個(gè)企業(yè)研究實(shí)驗(yàn)室——同時(shí)還擔(dān)任微軟紐約研究院的董事主任助理。他發(fā)表了100多篇論文，申請(qǐng)了20多項(xiàng)專利，在主流媒體發(fā)表文章，并發(fā)表了50多場(chǎng)受邀演講。

魯盼

斯坦福大學(xué)的博士后研究員。他于2018年獲得清華大學(xué)碩士學(xué)位（導(dǎo)師王建勇教授），2024年獲得加州大學(xué)洛杉磯分校（UCLA）計(jì)算機(jī)科學(xué)博士學(xué)位。他的研究重點(diǎn)是開(kāi)發(fā)AI方法和系統(tǒng)，以推進(jìn)復(fù)雜推理、數(shù)學(xué)智能和科學(xué)發(fā)現(xiàn)。他曾擔(dān)任NENLP 2025高級(jí)程序主席、SoCal NLP 2023程序主席以及NeurIPS MATHAI研討會(huì)聯(lián)合主席（2021 - 2024）。他曾榮獲多項(xiàng)獎(jiǎng)項(xiàng)，包括兩項(xiàng)最具影響力論文獎(jiǎng)（NeurIPS 2022、ICLR 2024）、ACL 2023最佳論文榮譽(yù)獎(jiǎng)、KnowledgeNLP研討會(huì)2025最佳論文獎(jiǎng)，以及由亞馬遜、彭博和高通資助的博士生獎(jiǎng)學(xué)金。

——（未完待續(xù)）——

參考資料

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

小樂(lè)數(shù)學(xué)科普近期文章

出版社和作家自薦通道

小樂(lè)數(shù)學(xué)科普薦書(shū)

·開(kāi)放 · 友好 · 多元 · 普適 · 守拙·

讓數(shù)學(xué)

更加

易學(xué)易練

易教易研

易賞易玩

易見(jiàn)易得

易傳易及

歡迎評(píng)論、點(diǎn)贊、在看、在聽(tīng)

收藏、分享、轉(zhuǎn)載、投稿

查看原始文章出處

點(diǎn)擊zzllrr小樂(lè)

公眾號(hào)主頁(yè)

加星★

數(shù)學(xué)科普不迷路！