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

公眾號主頁

加星★

數學科普不迷路！