★加星zzllrr小樂公眾號數學科普不迷路!
2025年9月17日——文藝復興慈善基金會和XTX Markets宣布從AI for Math Fund(數學AI基金)獲得1800 萬美元的資助,這是有史以來最大的慈善投入之一,旨在支持開發基于AI人工智能和機器學習的工具來推動數學發展。
該基金首批29個獲獎項目涵蓋大學和機構的數學家和研究人員,他們致力于開發有助于推進多項關鍵任務的數學發現和研究的系統。這些項目包括前沿形式化數學數據集、促進人工智能與數學協同作用的軟件工具,以及一些將人工智能應用于基礎數學和應用的高風險、高回報的構想。資助金額最高可達100萬美元。
![]()
作者:文藝復興慈善基金官網(Renaissance Philanthropy)2025-9-17
譯者:zzllrr小樂(數學科普公眾號)2025-9-24
該基金于2024年12月啟動(參見),XTX Markets承諾注資900萬美元,收到了來自世界各地研究人員和數學家團隊的280份申請。由于申請質量高,XTX Markets的資金規模翻了一番,達到1800萬美元。
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。
![]()
韓衍雋
紐約大學柯朗數學科學研究所和數據科學中心的數學與數據科學助理教授。他于2021年獲得斯坦福大學電氣工程博士學位(之前系2011年安徽省高考理科狀元——705分,保送清華大學電子工程系),并在加州大學伯克利分校西蒙斯計算理論研究所和麻省理工學院統計與數據科學中心工作多年。他對數據科學的數學有著廣泛的興趣,包括統計學、學習理論、強盜算法和信息論。
![]()
鄧準
北卡羅來納大學教堂山分校計算機科學系的助理教授。他于浙江大學竺可楨學院獲得數學學士學位,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)
AI安全研究員。在獲得數學集合論博士學位后,他在牛津大學計算機科學系從事博士后研究,專注于圖神經網絡的理論研究。目前,他正在進行一個機器學習與博弈論交叉領域的獨立研究項目。他即將在非營利性AI安全研究機構 FAR.AI 擔任研究科學家。
![]()
約書亞·翁(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最佳論文獎,以及由亞馬遜、彭博和高通資助的博士生獎學金。
——(未完待續)——
參考資料
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小樂
公眾號主頁
加星★
數學科普不迷路!
特別聲明:以上內容(如有圖片或視頻亦包括在內)為自媒體平臺“網易號”用戶上傳并發布,本平臺僅提供信息存儲服務。
Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.