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

接上文

本文介紹文藝復(fù)興慈善基金會(huì)揭曉首批1800萬美元AI數(shù)學(xué)基金資助的29個(gè)項(xiàng)目（二）[11 ~ 20]

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

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

11、結(jié)構(gòu)化動(dòng)機(jī)證明數(shù)據(jù)庫

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

該項(xiàng)目旨在通過開發(fā)一個(gè)全面的動(dòng)機(jī)證明數(shù)據(jù)庫，清晰記錄每個(gè)想法的起源，從而顯著增強(qiáng)AI驅(qū)動(dòng)的數(shù)學(xué)研究。通過實(shí)施“證明-發(fā)現(xiàn)步驟”作為Lean策略，團(tuán)隊(duì)將促進(jìn)這些證明的形式化和識(shí)別，從而創(chuàng)建一個(gè)以Lean方式表達(dá)的并行數(shù)據(jù)庫。這種創(chuàng)新方法有望促進(jìn)數(shù)學(xué)領(lǐng)域AI模型的訓(xùn)練、評(píng)估和解釋，為傳統(tǒng)的定理-證明配對(duì)提供一種更適合實(shí)際數(shù)學(xué)任務(wù)的替代方案。該項(xiàng)目有望通過提供一個(gè)透明且結(jié)構(gòu)化的框架來理解數(shù)學(xué)家的推理方式，從而顯著提高AI在數(shù)學(xué)任務(wù)中的表現(xiàn)。

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

蒂莫西·高爾斯（Timothy Gowers）

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

阿南德·拉奧·塔迪帕特里（Anand Rao Tadipatri）

劍橋大學(xué)Timothy Gowers以人為本（中心）的自動(dòng)定理證明研究小組的二年級(jí)博士生。他與研究小組的其他成員合作，開發(fā)了一個(gè)自動(dòng)推廣證明的程序，并在Lean上設(shè)計(jì)了一個(gè)適合證明發(fā)現(xiàn)的環(huán)境。他是Lean社區(qū)的成員，期待有一天交互式定理證明器能夠成為數(shù)學(xué)家的主流，并積極協(xié)助證明發(fā)現(xiàn)過程。

安舒拉·甘地（Anshula Gandhi）

劍橋大學(xué)數(shù)學(xué)專業(yè)的博士生，專攻自動(dòng)定理證明以及失敗和泛化（推廣）在數(shù)學(xué)研究中的作用。她的研究背景還涵蓋結(jié)理論、機(jī)器人技術(shù)和計(jì)算天體物理學(xué)。

雅各布·洛德（Jacob Loader）

Jacob Loader在悉尼大學(xué)完成了數(shù)學(xué)和計(jì)算機(jī)科學(xué)的本科學(xué)位，隨后在劍橋大學(xué)獲得了數(shù)學(xué)碩士學(xué)位。他的研究涵蓋了純數(shù)學(xué)的多個(gè)領(lǐng)域，包括概率論、表示論和解析數(shù)論。他目前的研究方向是利用反例引導(dǎo)迭代法解決存在性問題，并通過Lean 4中的元編程來實(shí)現(xiàn)這些想法。

約萬·格布沙伊德（Jovan Gerbscheid）

Jovan Gerbscheid完成了劍橋數(shù)學(xué)tripos學(xué)位考試，并在國際數(shù)學(xué)奧林匹克競(jìng)賽中獲得了一枚金牌和兩枚銅牌。他目前正在完成自動(dòng)定理證明博士學(xué)位的第一年學(xué)習(xí)。他是Lean社區(qū)的活躍成員，專注于Lean元編程，最近還擔(dān)任了mathlib的官方審閱者。

喬納斯·拜耳（Jonas Bayer）

Jonas Bayer在不來梅雅各布大學(xué)獲得數(shù)學(xué)學(xué)士學(xué)位。他目前是劍橋大學(xué)的博士生，研究自動(dòng)定理證明。他因與馬可·大衛(wèi)（Marco David）合作在Isabelle中成功形式化戴維斯、普特南、羅賓遜和馬蒂亞塞維奇提出的希爾伯特第十問題的解而聞名。

12、DEEPER——用于精確專家推理的深度探索引擎

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

“DEEPER”（Deep Exploratory Engine for Precise Expert Reasoning）項(xiàng)目旨在通過整合先進(jìn)的機(jī)器學(xué)習(xí)技術(shù)，為最先進(jìn)的自動(dòng)定理證明器 (ATP，automatic theorem provers) 提供指導(dǎo)，從而徹底革新自動(dòng)定理證明。通過結(jié)合神經(jīng)學(xué)習(xí)和符號(hào)學(xué)習(xí)方法，該團(tuán)隊(duì)致力于增強(qiáng)證明指導(dǎo)，特別是針對(duì)高階和依賴類型演算的證明指導(dǎo)，這些演算對(duì)于形式化復(fù)雜數(shù)學(xué)問題至關(guān)重要。該項(xiàng)目專注于開發(fā)基于AI的自動(dòng)推理系統(tǒng)指導(dǎo)，設(shè)計(jì)高效的證明自動(dòng)化，并將這些進(jìn)步融入現(xiàn)代證明助手中。

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

切扎里·卡利齊克（Cezary Kaliszyk）

墨爾本大學(xué)的教授，專攻自動(dòng)推理、證明輔助自動(dòng)化和交互式定理證明。在荷蘭拉德堡德大學(xué)獲得博士學(xué)位后，他擔(dān)任因斯布魯克大學(xué)的終身副教授。他的研究領(lǐng)域包括學(xué)習(xí)引導(dǎo)式證明搜索、名義邏輯以及Coq和形式集合論的錘子系統(tǒng)開發(fā)。

馬丁·蘇達(dá)（Martin Suda）

Martin Suda領(lǐng)導(dǎo)著捷克信息學(xué)、機(jī)器人學(xué)和控制論研究所（CIIRC）的自動(dòng)推理小組，該研究所隸屬于布拉格捷克技術(shù)大學(xué)。他的研究探索了機(jī)器學(xué)習(xí)與自動(dòng)定理證明的交叉領(lǐng)域，重點(diǎn)是增強(qiáng)像“吸血鬼證明器”（Vampire prover）這樣的系統(tǒng)。他擁有薩爾大學(xué)博士學(xué)位，并在曼徹斯特和維也納擔(dān)任過博士后。

揚(yáng)·雅庫布夫（Jan Jakub?v）

捷克布拉格技術(shù)大學(xué)CIIRC的高級(jí)研究員，專攻自動(dòng)推理和形式驗(yàn)證。他于赫瑞瓦特大學(xué)獲得博士學(xué)位，研究方向?yàn)檫^程演算和類型系統(tǒng)。他近期的研究重點(diǎn)是機(jī)器學(xué)習(xí)技術(shù)在定理證明中的應(yīng)用，同時(shí)也是ENIGMA的主要開發(fā)者。

13、文檔級(jí)自動(dòng)形式化

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

該項(xiàng)目將開發(fā)開源工具，實(shí)現(xiàn)數(shù)學(xué)文檔形式化的自動(dòng)化，并利用Lean證明助手對(duì)研究級(jí)數(shù)學(xué)進(jìn)行算法驗(yàn)證。項(xiàng)目團(tuán)隊(duì)將充分利用其在數(shù)論和幾何優(yōu)化領(lǐng)域高等數(shù)學(xué)形式化的經(jīng)驗(yàn)，以及在自然語言處理和形式驗(yàn)證方面的專業(yè)知識(shí)。通過將大語言模型與自動(dòng)符號(hào)推理相結(jié)合，該項(xiàng)目將創(chuàng)建一個(gè)基于Lean藍(lán)圖的模塊化形式化框架，從而推動(dòng)數(shù)學(xué)結(jié)果形式化驗(yàn)證的民主化。

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

安托萬·博塞呂（Antoine Bosselut）

瑞士洛桑聯(lián)邦理工學(xué)院（EPFL）計(jì)算機(jī)與通信科學(xué)學(xué)院的助理教授。此前，他曾在斯坦福大學(xué)擔(dān)任博士后研究員，并在艾倫AI研究所（AI2）擔(dān)任青年研究員。他于2020年獲得華盛頓大學(xué)博士學(xué)位。他的研究重點(diǎn)是開發(fā)能夠有效轉(zhuǎn)化為解決醫(yī)療、教育和弱勢(shì)群體等重要社會(huì)問題的AI推理方法。他于2021年入選《福布斯》雜志30位30歲以下科學(xué)與醫(yī)療保健領(lǐng)域杰出人物榜單，并擔(dān)任瑞士AI計(jì)劃指導(dǎo)委員會(huì)成員。

維克托·昆恰克（Viktor Kun?ak）

洛桑聯(lián)邦理工學(xué)院 (EPFL) 計(jì)算機(jī)與通信科學(xué)學(xué)院的副教授，他于2007年獲得麻省理工學(xué)院 (MIT) 博士學(xué)位后加入該學(xué)院。此后，他一直領(lǐng)導(dǎo)洛桑聯(lián)邦理工學(xué)院自動(dòng)推理與分析實(shí)驗(yàn)室，指導(dǎo)了16篇已完成的博士論文。他的團(tuán)隊(duì)開發(fā)了Stainless軟件驗(yàn)證器和Lisa形式化證明助手。Viktor曾是歐洲自動(dòng)推理、驗(yàn)證和綜合網(wǎng)絡(luò)（COST 行動(dòng)）的發(fā)起人和協(xié)調(diào)員之一，并獲得了歐洲研究理事會(huì) (ERC) 為期5年、金額為150萬歐元的程序綜合研究經(jīng)費(fèi)。

瑪麗娜·維亞佐夫斯卡（Maryna Viazovska）

1984年出生于烏克蘭基輔。她于2005年獲得基輔國立大學(xué)數(shù)學(xué)學(xué)士學(xué)位，并于2007年獲得凱澤斯勞滕大學(xué)碩士學(xué)位。她曾是馬克斯·普朗克數(shù)學(xué)研究所Don Zagier教授的博士生，并于波恩大學(xué)獲得博士學(xué)位。在柏林洪堡大學(xué)完成博士后研究后，她于2017年加入洛桑聯(lián)邦理工學(xué)院（EPFL），并于2018年成為該學(xué)院的全職教授。2022年，她因解決八維球體堆積問題而榮獲菲爾茲獎(jiǎng)。

參閱

14、特定領(lǐng)域Mathlib文檔

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

該項(xiàng)目旨在通過創(chuàng)建易于理解、針對(duì)特定領(lǐng)域的Lean定理證明指南，為對(duì)形式化感興趣的數(shù)學(xué)家們搭建橋梁。該項(xiàng)目面向研究生及以上水平的數(shù)學(xué)家，重點(diǎn)關(guān)注代數(shù)數(shù)論和圖論等領(lǐng)域。在這些領(lǐng)域，現(xiàn)有的Mathlib API雖然已經(jīng)非常成熟，但對(duì)于非專業(yè)人士來說仍然頗具挑戰(zhàn)性。通過提供參考成功資源的概述、示例和練習(xí)，該項(xiàng)目旨在增強(qiáng)對(duì)形式化的理解和參與，最終擴(kuò)展可用于AI模型訓(xùn)練的高質(zhì)量Lean代碼。

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

約翰·塔爾博特（John Talbot）

曾任牛津大學(xué)政府通信總部 (GCHQ) 研究員，后獲倫敦大學(xué)學(xué)院皇家學(xué)會(huì)大學(xué)研究員稱號(hào)。他目前是倫敦大學(xué)學(xué)院純數(shù)學(xué)副教授，研究極值和概率組合學(xué)。他最近對(duì)Lean證明形式化產(chǎn)生了興趣。

理查德·M·希爾（Richard M. Hill）

曾在哥廷根和馬克斯普朗克研究所（波恩）擔(dān)任研究職務(wù)，現(xiàn)任倫敦大學(xué)學(xué)院純數(shù)學(xué)教授。

15、游戲結(jié)束還是QED？——將Lean游戲服務(wù)器提升到新的水平

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

Lean游戲服務(wù)器項(xiàng)目旨在通過提供易于理解的數(shù)學(xué)形式化和驗(yàn)證入門，拓展計(jì)算機(jī)輔助定理證明的覆蓋范圍和影響力。該服務(wù)器將進(jìn)行擴(kuò)展，以吸引多元化的學(xué)生和研究人員群體，鼓勵(lì)他們參與形式化數(shù)學(xué)，提升其教育價(jià)值，并在數(shù)學(xué)AI領(lǐng)域培育更龐大的貢獻(xiàn)者社區(qū)。

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

馬庫斯·齊布羅維斯（Marcus Zibrowius）

Marcus Zibrowius是杜塞爾多夫海因里?！ずＤ髮W(xué)的拓?fù)鋵W(xué)和幾何學(xué)教授。他的博士論文在劍橋大學(xué)Burt Totaro的指導(dǎo)下完成。他的核心研究領(lǐng)域是K-理論，但最近他也領(lǐng)導(dǎo)了使用拓?fù)鋽?shù)據(jù)分析方法研究大語言模型的研究。

16、GNN-SMT——基于聯(lián)盟的Lean 4證明自動(dòng)化

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

斯坦福Centaur實(shí)驗(yàn)室在Lean 4中采用雙管齊下的方法實(shí)現(xiàn)證明自動(dòng)化：Lean-SMT和通用定理證明智能體。Lean-SMT集成了SMT（可滿足性模理論）求解器，以擴(kuò)展Lean的功能并提供一種新的證明策略。通用定理證明智能體的靈感源自真正的數(shù)學(xué)家進(jìn)行數(shù)學(xué)運(yùn)算的方式，并使用機(jī)器學(xué)習(xí)輔助的蒙特卡洛樹搜索（AlphaGo等AI突破背后的技術(shù)）基于啟發(fā)式過程探索大量的證明狀態(tài)空間。

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

克拉克·巴雷特（Clark Barrett）

斯坦福大學(xué)計(jì)算機(jī)科學(xué)（研究）教授。他的專長是自動(dòng)推理及其應(yīng)用。他是可滿足性模理論（SMT）和形式化硬件驗(yàn)證的早期先驅(qū)。近年來，他還開創(chuàng)了將形式化方法應(yīng)用于AI系統(tǒng)的技術(shù)。他是斯坦福自動(dòng)推理中心（Centaur，Center for Automated Reasoning）主任和斯坦福AI安全中心聯(lián)合主任。他是ACM會(huì)士，并兩度榮獲計(jì)算機(jī)輔助驗(yàn)證（CAV）獎(jiǎng)。

萊尼·阿尼瓦（Leni Aniva）

斯坦福大學(xué)計(jì)算機(jī)科學(xué)博士生。她是Pantograph工具的主要作者，該工具被學(xué)術(shù)界和工業(yè)界的眾多機(jī)器輔助定理證明項(xiàng)目廣泛使用。她擁有多年的軟件工程經(jīng)驗(yàn)，曾參與SMT求解器、證明助手和機(jī)器學(xué)習(xí)智能體的開發(fā)，尤其注重可診斷性和效率。

阿卜杜勒曼·穆罕默德（Abdalrhman Mohamed）

斯坦福大學(xué)的博士生，研究方向?yàn)槎ɡ碜C明和模型檢查的交叉領(lǐng)域。他是cvc5和Lean-SMT（一種將cvc5集成到Lean中的策略）的核心開發(fā)人員。他的研究重點(diǎn)是SMT求解及其在形式驗(yàn)證中的應(yīng)用。

哈倫·可汗（Harun Khan）

斯坦福大學(xué)計(jì)算機(jī)科學(xué)專業(yè)的博士生。他的研究重點(diǎn)是形式化驗(yàn)證、定理證明和自動(dòng)推理。他致力于Lean定理證明器中的數(shù)學(xué)形式化，包括“所有方法的穩(wěn)健均值估計(jì)”，以及形式化證明規(guī)則，以實(shí)現(xiàn)SMT求解器與Lean的集成。

17、LeanAide——通過自動(dòng)形式化連接AI和數(shù)學(xué)

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

該項(xiàng)目旨在通過開發(fā)一套無縫集成自然語言處理、大語言模型 (LLM) 和Lean的工具，重新審視數(shù)學(xué)概念的形式化和發(fā)現(xiàn)方式。通過創(chuàng)建一個(gè)易于訪問的無代碼AI+Lean環(huán)境，該項(xiàng)目旨在簡(jiǎn)化Lean用戶的形式化流程，并為數(shù)學(xué)家提供包括智能體解決方案在內(nèi)的全新創(chuàng)新研究工具。

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

悉達(dá)多·加吉爾（Siddhartha Gadgil）

印度科學(xué)研究所的數(shù)學(xué)教授。他擁有加州理工學(xué)院幾何拓?fù)鋵W(xué)博士學(xué)位，并在相關(guān)領(lǐng)域工作多年。近十年來，他主要致力于自動(dòng)定理證明的研究。在過去三年左右的時(shí)間里，他致力于開發(fā)Lean Prover，尤其致力于構(gòu)建與AI集成的工具。他的主要研究目標(biāo)是使AI和Lean能夠應(yīng)用于數(shù)學(xué)發(fā)現(xiàn)，而無需任何特殊的（非數(shù)學(xué)）專業(yè)知識(shí)。

維拉杰·庫馬爾（Viraj Kumar）

Kotak-IISc AI-ML中心的客座教授。他的研究重點(diǎn)是計(jì)算機(jī)教育，尤其關(guān)注如何重新思考生成式AI時(shí)代的教學(xué)法和評(píng)估方法。他擁有伊利諾伊大學(xué)厄巴納-香檳分校計(jì)算機(jī)科學(xué)博士學(xué)位（2007年），并且是ACM印度理事會(huì)的當(dāng)選成員，并擔(dān)任其教育項(xiàng)目的聯(lián)合主席。

阿尼魯?shù)隆す牌账ˋnirudh Gupta）

目前正在班加羅爾印度科學(xué)技術(shù)學(xué)院 (IISc Bengaluru) 攻讀理學(xué)學(xué)士學(xué)位。他的興趣包括數(shù)學(xué)、計(jì)算機(jī)科學(xué)和印度古典長笛演奏。他是一位敬業(yè)且充滿熱情的人，喜歡與團(tuán)隊(duì)合作，并盡其所能地投入工作。對(duì)他來說，從事研究工作不僅僅是一種職業(yè)追求，更是一份激發(fā)他求知欲的真摯熱情。他渴望做出有意義的貢獻(xiàn)，在學(xué)術(shù)環(huán)境中茁壯成長，不斷尋求探索和發(fā)現(xiàn)的機(jī)會(huì)。

姆里甘克（Mrigank）

印度科學(xué)研究所的一名即將升入大四的學(xué)生，正在攻讀數(shù)學(xué)和計(jì)算機(jī)專業(yè)的理學(xué)學(xué)士學(xué)位。他的研究重點(diǎn)是開發(fā)用于提升軟件質(zhì)量和自動(dòng)化軟件工程流程的工具。他尤其感興趣的是探索如何將傳統(tǒng)的軟件測(cè)試和分析技術(shù)與日益強(qiáng)大的大語言模型相結(jié)合，以大規(guī)模地解決此類問題。Mrigank希望通過模糊數(shù)學(xué)與軟件界限的定理證明器，將軟件工程的進(jìn)步帶入日益發(fā)展的形式化和自動(dòng)化數(shù)學(xué)領(lǐng)域。

斯瓦爾納瓦·查克拉博蒂（Swarnava Chakraborty）

目前正在印度理工學(xué)院攻讀數(shù)學(xué)與計(jì)算機(jī)學(xué)士學(xué)位，已完成二年級(jí)學(xué)業(yè)。他一直對(duì)自動(dòng)定理證明領(lǐng)域充滿興趣。他的主要研究興趣在于利用Lean方法實(shí)現(xiàn)自動(dòng)形式化，以及將AI融入這一廣闊領(lǐng)域。

舒巴姆·庫馬爾（Shubham Kumar）

專攻使用OCaml進(jìn)行函數(shù)式編程以及使用Coq進(jìn)行形式化驗(yàn)證。他對(duì)形式化方法的興趣始于學(xué)習(xí)期間，并通過在多核OCaml上的工作得以鞏固。這段經(jīng)歷促使他開始使用OCaml開發(fā)系統(tǒng)，并使用Coq和coq-of-ocaml應(yīng)用形式化驗(yàn)證技術(shù)。

18、LeanTutor——本科數(shù)學(xué)證明輔導(dǎo)

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

LeanTutor借助交互式定理證明器 (ITP) 和大語言模型 (LLM)，重新審視了本科生學(xué)習(xí)數(shù)學(xué)證明的方式。LeanTutor旨在自動(dòng)形式化學(xué)生（本科生）的自然語言證明，使用ITP評(píng)估證明的正確性，利用ITP的反饋生成后續(xù)步驟，并為學(xué)生提供個(gè)性化指導(dǎo)。LeanTutor的設(shè)計(jì)借鑒了教育研究、機(jī)器學(xué)習(xí)和形式化方法的洞見，旨在開發(fā)一個(gè)系統(tǒng)，讓學(xué)生和AI智能體能夠一起進(jìn)行有意義的數(shù)學(xué)學(xué)習(xí)。

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

吉雷賈·拉納德（Gireeja Ranade）

加州大學(xué)伯克利分校電氣工程與計(jì)算機(jī)科學(xué) (EECS) 系的副教授。在此之前，她曾在華盛頓州雷德蒙德市的微軟研究院擔(dān)任研究員。她在加州大學(xué)伯克利分校獲得電氣工程與計(jì)算機(jī)科學(xué)博士學(xué)位，并在馬薩諸塞州劍橋市的麻省理工學(xué)院獲得本科學(xué)位。她因其研究和教學(xué)成果榮獲多項(xiàng)獎(jiǎng)項(xiàng)，例如美國國家科學(xué)基金會(huì)杰出人才獎(jiǎng) (NSF CAREER Award)、加州大學(xué)伯克利分校電氣工程杰出教學(xué)獎(jiǎng)、加州大學(xué)伯克利分校杰出GSI指導(dǎo)獎(jiǎng)等。

19、大語言模型——用于反應(yīng)式程序的格論推理

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

該項(xiàng)目旨在通過開發(fā)一種新穎的方法，利用基于合成的精化命題數(shù)據(jù)集進(jìn)行微調(diào)的大語言模型 (LLM) 來證明精化定律，從而推動(dòng)數(shù)學(xué)推理AI的發(fā)展。團(tuán)隊(duì)致力于創(chuàng)建包含證明和反例的綜合數(shù)據(jù)集，以提高訓(xùn)練數(shù)據(jù)集的多樣性和質(zhì)量，從而彌補(bǔ)數(shù)學(xué)AI領(lǐng)域的重大差距。該項(xiàng)目將LLM與最先進(jìn)的精化檢查技術(shù)相結(jié)合，以提高精化證明的準(zhǔn)確性和效率。這項(xiàng)工作不僅有望超越現(xiàn)有方法，還將為未來數(shù)學(xué)推理AI模型訓(xùn)練提供寶貴的基準(zhǔn)數(shù)據(jù)集。

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

佩德羅·里貝羅（Pedro Ribeiro）

英國約克大學(xué)計(jì)算機(jī)科學(xué)講師（助理教授）。此前，他曾擔(dān)任約克大學(xué)物理工程與技術(shù)學(xué)院的研究員，更早之前擔(dān)任計(jì)算機(jī)科學(xué)的助理研究員。他在約克大學(xué)獲得了博士學(xué)位，研究方向?yàn)橥ㄟ^統(tǒng)一程序設(shè)計(jì)理論中的完整格理論處理過程演算中的非確定性問題。他在機(jī)器人技術(shù)和信息物理系統(tǒng)相關(guān)的軟件工程形式化方法方面擁有十多年的經(jīng)驗(yàn)。他的研究興趣涵蓋了整個(gè)工程生命周期，從領(lǐng)域特定符號(hào)及其語義的設(shè)計(jì)和開發(fā)，到使用自動(dòng)化數(shù)學(xué)證明技術(shù)（例如模型檢查和定理證明）進(jìn)行測(cè)試和形式化推理。他是約克大學(xué)RoboStar機(jī)器人軟件工程卓越中心的成員，也是歐洲形式化方法協(xié)會(huì)傳播委員會(huì)的創(chuàng)始成員。

弗蘭克·索博岑斯基（Frank Soboczenski）

約克大學(xué)計(jì)算機(jī)科學(xué) (AI/ML) 助理教授，并在倫敦國王學(xué)院擔(dān)任副科學(xué)家。他的研究重點(diǎn)是深度學(xué)習(xí)和Transformer模型、可解釋機(jī)器學(xué)習(xí)和量子機(jī)器學(xué)習(xí)，主要側(cè)重于太空和醫(yī)療保健領(lǐng)域的應(yīng)用。Frank是NASA和NOAA的GLOBE計(jì)劃的STEM科學(xué)家、NASA GeneLab AI重點(diǎn)工作組成員（負(fù)責(zé)載人航天數(shù)據(jù)）、IBM量子研究人員計(jì)劃科學(xué)家、NASA Nancy Grace Roman航天器工作組成員、激光干涉儀空間天線 (LISA) 工作組成員、歐洲學(xué)習(xí)和智能系統(tǒng)實(shí)驗(yàn)室 (ELLIS) 學(xué)者、國際天文學(xué)聯(lián)合會(huì)(IAU) 成員。Frank經(jīng)常與NASA中心合作，包括領(lǐng)導(dǎo)肯尼迪航天中心過去的機(jī)器學(xué)習(xí)研討會(huì)并擔(dān)任NASA生物醫(yī)學(xué)研討會(huì)的發(fā)言人。他的工作獲得了多項(xiàng)榮譽(yù)，例如NASA TechLeap獎(jiǎng)；NASA/NOAA/美國國務(wù)院對(duì)杰出指導(dǎo)的認(rèn)可；以及多個(gè)前沿發(fā)展實(shí)驗(yàn)室的榮譽(yù)。

20、Leaning and Rocq'ing（Lean和Rocq Prover）

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

該項(xiàng)目利用大語言模型 (LLM) 的強(qiáng)大功能，促進(jìn)不同交互式定理證明器 (ITP)（例如Lean和Rocq Prover）之間以及同一證明器不同版本（例如Lean 3與Lean 4）之間陳述和證明的轉(zhuǎn)換。通過實(shí)現(xiàn)跨平臺(tái)證明和庫的轉(zhuǎn)換，該項(xiàng)目旨在創(chuàng)建一個(gè)統(tǒng)一的形式化知識(shí)庫，增強(qiáng)形式化方法社區(qū)內(nèi)的協(xié)作和資源共享。這項(xiàng)工作不僅可以連接MathLib和Mathematical Components等重要資源，還能在未來的重大更新（例如Lean 5）期間支持更順暢的過渡。

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

紀(jì)堯姆·鮑達(dá)特（Guillaume Baudart）

Inria IRIF實(shí)驗(yàn)室PICUBE團(tuán)隊(duì)的研究員。2017年至2020年，他曾擔(dān)任IBM TJ Watson研究中心AI編程模型團(tuán)隊(duì)的研究員。他的研究重點(diǎn)是概率編程，最近又轉(zhuǎn)向了用于交互式定理證明的生成式AI。

西里爾·科恩（Cyril Cohen）

Inria里昂高等師范學(xué)院LIP CASH團(tuán)隊(duì)的研究員。他的主要研究方向是利用數(shù)學(xué)知識(shí)豐富Rocq證明器。他也是數(shù)學(xué)組件庫的主要架構(gòu)師之一。

尼古拉斯·塔巴羅（Nicolas Tabareau）

Inria高級(jí)研究員，領(lǐng)導(dǎo)著位于南特的Gallinette團(tuán)隊(duì)。他專注于交互式定理證明器 (ITP) 的開發(fā)和實(shí)現(xiàn)，并在Rocq Prover的持續(xù)開發(fā)中發(fā)揮著積極作用。

馬克·勒拉奇（Marc Lelarge）

Inria高級(jí)研究員，也是巴黎高等師范學(xué)院計(jì)算機(jī)科學(xué)系的講師。他的研究涵蓋機(jī)器學(xué)習(xí)、深度學(xué)習(xí)和圖論，近期專注于用于交互式定理證明的生成式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

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

出版社和作家自薦通道

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

·開放 · 友好 · 多元 · 普適 · 守拙·

讓數(shù)學(xué)

更加

易學(xué)易練

易教易研

易賞易玩

易見易得

易傳易及

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

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

查看原始文章出處

點(diǎn)擊zzllrr小樂

公眾號(hào)主頁

加星★

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