★加星zzllrr小樂公眾號數學科普不迷路！

接上文

本文介紹文藝復興慈善基金會揭曉首批1800萬美元AI數學基金資助的29個項目（三）[21 ~ 28]

作者：文藝復興慈善基金官網（Renaissance Philanthropy）2025-9-17

譯者：zzllrr小樂（數學科普公眾號）2025-9-26

21、學習與吸血鬼（Vampire）和蜘蛛（Spider）一起做數學題

項目簡介

該項目旨在通過將無窮級數和超越函數等特定數學結構集成到全自動定理證明器Vampire（吸血鬼）的推理程序中，增強其性能。本項目旨在通過創(chuàng)新的機器學習方法和針對特定數學理論定制的策略組合開發(fā)，提升Vampire在標準數學上的表現。該項目還將建立一個網絡服務，以促進自動定理證明器的使用，并創(chuàng)建開放數據集，以支持全球自動定理證明工作。

團隊簡介

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

安德烈· 沃倫科夫從7歲起就癡迷于證明定理，而從15歲第一次接觸穿孔卡片起，他同樣癡迷于編寫計算機程序。毫不奇怪，他的第一個非玩具計算機程序是一個用于證明定理的程序。

他對計算機定理證明的熱情促成了定理證明器Vampire的設計和初步開發(fā)，該程序自1999年以來在一階定理證明中贏得了70個世界冠軍頭銜。

他在自動推理的諸多領域做出了貢獻，包括理論、實現技術和應用。2007年，他為Vampire開發(fā)了首個基于機器學習的策略調度程序Spider（蜘蛛）。在業(yè)余時間，他還開發(fā)了會議管理系統(tǒng)EasyChair，該系統(tǒng)目前已被超過400萬研究人員使用。

他認為，當數學家和計算機程序互相傳授數學知識、互相學習時，世界將會變得更加美好。他相信，最近在自動推理領域發(fā)展起來的技術，例如理論推理和歸納法，能夠在未來20到50年內引領計算機輔助數學的革命。

邁克爾·羅森（Michael Rawson）

邁克爾·羅森認為計算機應該能夠推理并從過去的經驗中學習。他對自動定理證明尤其感興趣：能夠進行嚴密邏輯論證的計算機系統(tǒng)。他是“古董吸血鬼”（Antique Vampires）團隊的一員：該團隊負責監(jiān)督和指導世界領先的定理證明器“吸血鬼”（Vampire）的設計和開發(fā)。

22、數學基準（Mathbench）——評估自然語言證明

項目簡介

MathBench項目旨在通過引入一個全新的帶注釋證明數據集，來提升AI模型在數學推理方面的評估能力。該數據集包含與多個不同證明配對的定理，每個證明被分解為關鍵步驟，并附有摘要、錯誤論證和邏輯結構元數據的注釋。通過利用MathBench，該項目旨在評估AI模型識別關鍵證明步驟、糾正錯誤以及區(qū)分有效和無效證明的能力，從而了解大語言模型在數學推理和理解方面的能力。

團隊簡介

悉達多·巴特（Siddharth Bhat）

劍橋大學的博士生。他是形式化驗證、函數式編程語言實現和應用范疇論方面的專家。他是Lean定理證明器前20名貢獻者之一。他在高性能計算和循環(huán)優(yōu)化方面也擁有豐富的經驗。他的長期愿景是構建可擴展的數學定理證明系統(tǒng)，并已為此發(fā)表了多項研究成果。

亞歷克斯·哈夫里拉（Alex Havrilla）

佐治亞理工學院數學與機器學習博士生。他的研究方向是生成模型的理論與實踐，重點是通過強化學習和合成數據改進推理能力。他曾在Meta、微軟和谷歌實習，并共同創(chuàng)立了開源RLHF研究小組CarperAI。

斯特拉·比德曼（Stella Biderman）

EleutherAI的執(zhí)行董事，EleutherAI是一家由草根研究團體轉型而來的非營利性研究機構，開創(chuàng)了現代開源AI運動。Stella在 GPT-Neo、Pythia、BLOOM、OpenFold和VQGAN-CLIP等模型上的工作，極大地提升了基礎模型的可訪問性，同時也為AI的透明度和開放科學樹立了標桿。除了開發(fā)新模型外，Stella還投入了大量時間致力于開發(fā)開源AI庫、構建和記錄公共數據集以及開展可解釋性研究。

帕萬·薩?？āぐ⒙{曼奇（Pawan Sasanka Ammanamanchi）

Ritual的研究員，也是EleutherAI的志愿研究員。他擁有印度理工學院海得拉巴分校的碩士學位，專攻大語言模型的評估。他的貢獻包括BLOOM模型和GEM基準測試。他尤其熱衷于推動AI在數學領域的應用。

23、AI和機器學習的新范疇和拓撲基礎

項目簡介

該項目探索基于更定制的數學表示空間和結構（包括層論sheaf theory和范疇論category theory）的新型神經網絡架構。這些新型架構或許能夠融入數學對象的關鍵結構對稱性和屬性，從而能夠創(chuàng)建輔助證明構建的新工具，并提供超越當前AI Copilot范式的實用優(yōu)勢。探索能夠在豐富類型理論中表示和操縱證明狀態(tài)的模型的可能性，或許能幫助我們彌合機器學習與傳統(tǒng)數學領域之間的差距。

團隊簡介

皮埃特羅·利奧（Pietro Lio）

劍橋大學計算機科學系的計算生物學教授，他于2004年加入該系任教。他最初在佛羅倫薩和帕維亞學習，專注于遺傳學和復雜系統(tǒng)，之后在南安普頓和劍橋擔任研究職位。他的工作重點是利用AI和計算生物學來理解疾病過程。

杰米·維卡里（Jamie Vicary）

劍橋大學計算機科學系未來計算教授。他獲得物理學和數學學士學位后，在牛津大學擔任計算機科學研究員十年，2018年加入伯明翰大學擔任高級講師，并于2020年調至劍橋大學任教。他的研究興趣廣泛，涵蓋量子計算、理論計算機科學和機器學習。

24、Polymath Plus（Polymath +）

項目簡介

Polymath Plus是一個新一代在線協作平臺，它將大規(guī)模的人類互動與基于AI的推理相結合，以推進數學探索。在Polymath原項目的基礎上，它既利用AI作為管理員來管理討論，又利用AI作為協作者來貢獻想法并驗證證明。Polymath Plus旨在將人類直覺與機器輔助的嚴謹性相結合，簡化既定定理，解決尚未解決的挑戰(zhàn)，并加速數學界的協作。

團隊簡介

皮埃特羅·米切魯奇（Pietro Michelucci）

人類計算研究所的執(zhí)行主任，也是康奈爾大學的訪問學者。作為一名專注于人機混合智能的認知科學家，他致力于運用人機互補的優(yōu)勢來解決社會問題。他創(chuàng)立了“Stall Catchers”公民科學項目，并擔任《人類計算手冊》的編輯。

杰森·戴爾 (Jason Dyer)

在高中任教11年；在此期間，他參與了Polymath項目，該項目發(fā)現了Hales-Jewett定理密度版的新組合證明。之后，他加入了數學和科學學習應用程序Brilliant.org，負責開發(fā)課程，并與服務成員安排小型Polymath項目。他目前為歐洲、北美和亞洲的客戶提供教育游戲設計咨詢服務。

薩姆·沙班（Sam Shaaban）

自1999年創(chuàng)立NuRelm以來，Sam Shaaban一直致力于為研究人員和創(chuàng)新者開發(fā)軟件。他熱衷于幫助創(chuàng)作者集思廣益、制作原型、制定預算并交付數字健康應用程序、被動傳感器數據收集系統(tǒng)、研究門戶、數據處理管道以及改善生活的創(chuàng)造性方法。

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

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

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

DrivenData的聯合創(chuàng)始人兼負責人。DrivenData是一家致力于將AI的變革力量帶給應對全球最嚴峻挑戰(zhàn)的組織的社會企業(yè)。DrivenData的競賽平臺匯聚了全球數據科學家的技能和熱情，旨在構建造福社會的解決方案。我們與杰出的社區(qū)以及NASA、微軟、Meta AI和世界銀行等組織合作，已提供超過480萬美元的獎金，評估了超過20萬份參賽作品，并為公共服務、健康、科學、自然、教育等領域提供了先進的解決方案。

蒂莫西·高爾斯（Timothy Gowers）

法蘭西學院的組合數學教授，同時兼任劍橋大學數學系教授和三一學院研究員。在劍橋大學，他領導著一個自動定理證明小組，專注于理解人類數學家尋找證明的過程。他于1981年在國際數學奧林匹克競賽（IMO）中獲得滿分，并于1998年因其在泛函分析和組合數學領域的杰出貢獻榮獲菲爾茲獎。他是牛津通識讀本《數學：極簡導論》Mathematics: A Very Short Introduction一書的作者，也是《普林斯頓數學指南》的主編。

25、通過數學數據庫進行可擴展定理證明

項目簡介

該項目旨在通過在Lean數學庫(mathlib)和L-函數及模形式數據庫(LMFDB)之間建立接口，擴大自動定理證明器可訪問的數學內容規(guī)模。通過將mathlib約10萬個數學結果集合與LMFDB超過10億個具體語句的存儲庫連接起來，我們的目標是擴展人類數學家和AI智能體的能力。該項目將開發(fā)新的Lean策略，并建立一個將其他數學數據庫與形式化定理證明系統(tǒng)集成的框架，為可擴展的數學發(fā)現鋪平道路。

團隊簡介

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

東英吉利大學純數學講師，專攻數論。他的研究領域包括p進模形式的研究和計算，目前的研究方向是數學形式化，專注于Lean中的模形式理論。伯克貝克在華威大學獲得博士學位，導師是拉西娜·登貝萊（Lassina Dembele）和約翰·克雷莫納（John Cremona），隨后在倫敦大學學院（UCL）獲得博士后研究資格。

大衛(wèi)·羅（David Roe）

麻省理工學院數學系的首席研究科學家，他研究計算數論和算術幾何，尤其關注p進數（一種與實數類似但距離概念不同的數，用于測量被某個固定素數整除的可能性）。p進數在他為數學界構建計算工具的歷程中扮演了核心角色，這始于他在SageMath中對p進計算的研究。他擔任L-函數和模形式數據庫(LMFDB)的執(zhí)行編輯，該數據庫匯集了數論和算術幾何中出現的數學對象；他也是researchseminars.org的創(chuàng)始人之一，該網站是在疫情期間創(chuàng)建的，旨在幫助數學家參加在線研究研討會。

安德魯·薩瑟蘭（Andrew Sutherland）

麻省理工學院數學高級研究員，其研究項目專注于算術幾何和數論的計算方面。他在多項大型研究合作中發(fā)揮了重要作用，包括 “素數間有界間隙”的Polymath項目 、 L-函數和模形式數據庫以及 “算術幾何、數論和計算”西蒙斯合作項目 。薩瑟蘭目前擔任《計算數學》Mathematics of Computation的編輯、《數論研究》Research in Number Theory的主編、《L-函數和模形式數據庫》 的執(zhí)行編輯、布朗大學數學計算與實驗研究所的科學顧問委員會成員、數論基金會主席以及美國數學會會士。

26、畫板（Sketchpad）——高精度且易于使用的自動形式草圖生成系統(tǒng)

項目簡介

Sketchpad是一個由AI驅動的系統(tǒng)，用于將自然語言證明轉換為結構化的形式化草圖，旨在協助使用Isabelle和Lean進行形式數學工作的從業(yè)者。通過引入基于圖形的表示，它能夠將證明分解為單個陳述，從而支持細粒度的自動形式化，并與部分或不完整的證明進行更高效的交互。

團隊簡介

Wenda Li（李文達——音譯）

愛丁堡大學混合AI助理教授，專攻數學AI。他為使用大語言模型進行自動形式化的開創(chuàng)性工作做出了貢獻，并探索了用非形式化證明指導形式化定理證明的方法。除此之外，他的工作還涵蓋了驗證量詞消元法、格羅滕迪克的概形理論（scheme theory）以及解析數論的各個方面。他在這些領域的成就被評為BCS最佳論文獎亞軍。

Mai Luo（羅麥——音譯）

愛丁堡大學副教授（西安電子科技大學學士、倫敦帝國理工學院碩博），領導大規(guī)模機器學習系統(tǒng)研究組。他擔任英國工程與物理研究理事會（EPSRC）機器學習系統(tǒng)博士培訓中心聯合主任，以及英國ARIA項目“Scaling Compute – Charting the Course”的聯合負責人。他的研究涵蓋計算機系統(tǒng)、機器學習和數據管理。他領導的AI系統(tǒng)已被各大科技公司采用，并以開源軟件的形式廣泛發(fā)布，并獲得了廣泛的認可。他是谷歌博士生獎學金和微軟亞洲研究院StarTrack獎的獲得者，并入圍了校長新星研究獎的最終角逐。

拉里·保爾森（Larry Paulson）

亞馬遜學者、劍橋大學計算邏輯榮譽教授，也是形式邏輯和證明助手領域的知名專家。他領導了廣泛使用的Isabelle證明助手的開發(fā)，并率先推出了Sledgehammer，這項突破性的創(chuàng)新已被幾乎所有主流證明助手所采用。為了表彰他對證明助手和自動推理的杰出貢獻，他被選為ACM院士、皇家學會院士，并獲得了Herbrand獎。

辛華劍

愛丁堡大學的博士生（本科畢業(yè)于中山大學邏輯學專業(yè)，目前是字節(jié)跳動倫敦Seed實習生），與Jacques Fleuriot和Wenda Li合作。他的研究重點是使用大語言模型進行自動定理證明，尤其關注能夠自動形式化和知識庫學習的自主智能體。他的代表作包括：最先進的開源定理證明模型DeepSeek Prover系列；以任務分解和知識積累為特色的LEGO-Prover；以及用于庫級證明工程評估的基準數據集APE-Bench。

27、邁向自動化數學發(fā)現

項目簡介

該項目探索了一個多智能體猜想器-證明器框架，該框架利用大語言模型(LLM) 在Lean定理證明器中生成并證明新穎的數學猜想。該框架從實用性和新穎性的角度量化和形式化“趣味性”的概念，旨在簡化開放式數學探索和發(fā)現。通過對猜想器和證明器進行迭代改進，這種創(chuàng)新方法旨在推進自動化定理證明，并為新的數學見解的發(fā)展做出貢獻。

團隊簡介

亞倫·庫維爾（Aaron Courville）

蒙特利爾大學計算機科學與運籌學系(DIRO)的教授，也是IVADO的科學主任。他擁有卡內基梅隆大學機器人研究所的博士學位。Courville是深度學習的早期貢獻者：他是Mila——魁北克AI研究所的創(chuàng)始成員之一。他與Ian Goodfellow和Yoshua Bengio共同編寫了深度學習的開創(chuàng)性教科書。他目前的研究重點是深度學習模型和方法的開發(fā)。他對強化學習、多智能體強化學習、深度生成模型和推理尤其感興趣。

納文·戈亞爾（Navin Goyal）

1998年在孟買印度理工學院獲得理學學士學位，并于2005年在羅格斯大學獲得博士學位。在麥吉爾大學和佐治亞理工學院從事博士后研究后，他于2009年加入微軟印度研究院。他的研究始于理論計算機科學，研究范圍涵蓋算法設計和分析以及計算復雜性等諸多問題。逐漸地，他的工作轉向學習理論。他的理論研究有時涉及應用數學各個領域的技術（例如組合學、信息論、傅里葉分析）。這使他對數學和理論計算機科學的多樣性和統(tǒng)一性產生了濃厚的興趣。最近，他一直在進行實證研究，從多個角度理解神經網絡，包括其歸納偏差和對其內部工作原理的解釋，以及其解決數學問題的能力。他對數學和其他領域的人們如何取得新發(fā)現非常感興趣。

28、犢皮紙（Vellum）——AI輔助形式推理的可擴展框架

項目簡介

Vellum項目構建了一個開源框架，其中大語言模型 (LLM) 充當規(guī)劃器，并與多個交互式定理證明器 (ITP) 和自動求解器交互，旨在簡化數學探索和證明過程。通過與不同類型的求解器和工具交互，Vellum促進了大規(guī)模的AI輔助形式推理，從而簡化了自然語言陳述的自動形式化，并顯著降低了數學推理研究的門檻。

團隊簡介

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

德克薩斯大學奧斯汀分校計算機科學教授，同時也是谷歌Deepmind的研究科學家。他的研究融合了自動推理、機器學習和編程語言的理念，旨在創(chuàng)建功能強大、可靠、透明且安全的AI系統(tǒng)。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杰出創(chuàng)新獎，以及十余項計算機安全和深度學習領域頂級會議的“經得起時間考驗”獎和最佳論文獎。她是計算機安全領域被引用次數最多的學者，被評為最具影響力學者（AMiner獎）。她是ACM會士和IEEE會士，也是美國藝術與科學學院當選院士。她在加州大學伯克利分校獲得博士學位。她還是一位連續(xù)創(chuàng)業(yè)者，并被《Inc.》雜志評選為百強女性創(chuàng)始人，并被《Wired25》評選為創(chuàng)新者。

何靜軒

加州大學伯克利分校的博士后研究員。他的研究領域廣泛，涵蓋計算機安全、機器學習和編程語言，近期專注于提升AI軟件程序的安全性和可靠性。他于蘇黎世聯邦理工學院獲得博士學位，并榮獲蘇黎世聯邦理工學院杰出博士論文獎章。他還曾榮獲ACM CCS 2023杰出論文獎。

Zhe Ye（葉哲——音譯）

加州大學伯克利分校和伯克利研發(fā)中心的博士生（上?？萍即髮W信息科學與技術學院計算機科學學士）。他的研究方向包括大語言模型輔助形式化驗證、形式化規(guī)范合成和計算機安全。他在相關領域發(fā)表了多篇論文，其中一些已被IEEE S&P和ISSTA等頂級會議錄用。

阿米塔尤什·塔庫爾（Amitayush Thakur）

德克薩斯大學奧斯汀分校的博士生，致力于“數學AI”和“代碼AI”的交叉研究。他的興趣在于通過大語言模型進行自動化數學推理，以及其在完全驗證的程序合成中的意義，這對于從AI生成工業(yè)級代碼至關重要。他是Copra（一個用于形式化定理證明的智能體框架）的首席開發(fā)者。加入德克薩斯大學之前，他曾在微軟擔任軟件工程師，此前曾在微軟研究院擔任研究實習生。

喬治·蘇卡拉斯（George Tsoukalas）

德克薩斯大學奧斯汀分校的博士生，致力于研究用于自動數學推理和程序合成的神經符號技術。他領導創(chuàng)建了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小樂

公眾號主頁

加星★

數學科普不迷路！