導語

在2023年，由集智俱樂部聯(lián)合同濟大學特聘研究員陳小楊、清華大學交叉信息學院助理教授袁洋、南洋理工大學副教授夏克林三位老師共同發(fā)起“”讀書會，希望從 AI for Math，Math for AI 兩個方面深入探討人工智能與數(shù)學的密切聯(lián)系。我們也在持續(xù)關(guān)注這個領(lǐng)域的發(fā)展。

形式化數(shù)學推理代表了AI for Math的新前沿，它結(jié)合了數(shù)學的嚴謹性與AI的創(chuàng)造力。這種結(jié)合有希望開發(fā)出能夠可靠地進行復雜數(shù)學推理的AI系統(tǒng)，這不僅會推動數(shù)學本身的發(fā)展，還會為科學、工程和技術(shù)領(lǐng)域帶來變革性影響。我們特別邀請到北京國際數(shù)學研究中心徐天一研究員在本周三（3月12日）晚在讀書會上做加餐分享，關(guān)于AI+形式化數(shù)學的話題，是什么、為什么以及怎么做。

AI for formalized math: What, why, and how?

分享流程

19:00-20:30 主題分享，主講人：徐天一

20:30-21:00 圓桌討論，嘉賓：陳小楊

分享簡介

形式化數(shù)學，將數(shù)學證明轉(zhuǎn)化為計算機可驗證的語言，長期以來一直是少數(shù)專家的領(lǐng)域。它要求將每一步推理都精確到機器可驗證的程度，沒有跳躍，沒有“顯然”，只有嚴格的邏輯鏈條。這種嚴謹性使得形式化證明在傳統(tǒng)上需要耗費大量時間和專業(yè)知識，限制了其廣泛應用。

Lean語言的形式化表述

隨著生成式AI的崛起，這個領(lǐng)域也迎來了新的發(fā)展機遇。大語言模型有很強的推理能力，但是在準確性和可靠性方面面臨挑戰(zhàn)，形式化數(shù)學剛好可以彌補這一短板，為AI在數(shù)學推理上提供嚴格的驗證框架。反過來，AI也有潛力來幫助自動形式化，完成從自然語言到形式化語言的轉(zhuǎn)換，降低領(lǐng)域門檻，加速證明過程。

在本次分享中，將介紹形式化數(shù)學的發(fā)展現(xiàn)狀，以及和生成式AI交叉的前沿進展。

分享大綱

1. 形式化數(shù)學簡介

2. 形式化數(shù)學與生成式 AI：互補短長

3. 目前的進展

主講嘉賓簡介

徐天一，北京國際數(shù)學研究中心研究員。研究方向為自動化定理證明及 Lean 語言元編程。開發(fā)了多種用于操作 Lean 語言代碼的工具，涵蓋數(shù)據(jù)提取、依賴關(guān)系分析和動態(tài)交互等功能。同時負責 LeanSearch 的維護。

圓桌嘉賓簡介

陳小楊，同濟大學特聘研究員。2014年5月獲得美國圣母大學數(shù)學博士學位，2014-2016年在澳門大學從事博士后研究，并于2016年底入職同濟大學。陳小楊的主要研究方向為黎曼幾何，在 Geometry and Topology, Advances in Mathematics等期刊發(fā)表了多篇研究論文。近期，陳小楊與研究團隊開展了大模型在基礎(chǔ)數(shù)學的應用研究，并計劃開發(fā)機器學習算法用于發(fā)現(xiàn)數(shù)學規(guī)律，構(gòu)造數(shù)學猜想反例等。

同時陳小楊團隊發(fā)起了“ ”，旨在訓練一個開源數(shù)學大模型，將其數(shù)學推理能力提升至數(shù)學專業(yè)博士生水平，同時探索大模型是否具有數(shù)學創(chuàng)造能力，以及大模型在前沿數(shù)學研究中的潛在能力。邀請數(shù)學愛好者和智能探索者共同創(chuàng)建數(shù)學大模型。

推薦閱讀論文：

1. Yang, Kaiyu, et al. "Leandojo: Theorem proving with retrieval-augmented language models." Advances in Neural Information Processing Systems 36 (2023): 21573-21612. https://proceedings.neurips.cc/paper_files/paper/2023/file/4441469427094f8873d0fecb0c4e1cee-Paper-Datasets_and_Benchmarks.pdf

2. Gao, Guoxiong, et al. "A semantic search engine for Mathlib4." arXiv preprint arXiv:2403.13310 (2024). https://arxiv.org/abs/2403.13310v2

3. Gao, Guoxiong, et al. "Herald: A natural language annotated Lean 4 dataset." arXiv preprint arXiv:2410.10878 (2024). https://arxiv.org/abs/2410.10878

4. Lin, Yong, et al. "Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving." arXiv preprint arXiv:2502.07640 (2025). https://arxiv.org/abs/2502.07640

5. Ying, Huaiyuan, et al. "Lean workbook: A large-scale lean problem set formalized from natural language math problems." arXiv preprint arXiv:2406.03847 (2024). https://arxiv.org/abs/2406.03847

6. Xin, Huajian, et al. "Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data." arXiv preprint arXiv:2405.14333 (2024). https://arxiv.org/abs/2405.14333

直播信息

2025年3月12日 19:00-21:00

報名加入社群（可開發(fā)票）

集智斑圖鏈接：https://pattern.swarma.org/study_group/32?from=wechat

掃 碼參與 ，加入群聊，獲取系列讀書會回看權(quán)限，共建共享 AI for Math 科學社區(qū)，與一線科研工 作者溝通交流，共同推動這一前沿領(lǐng)域的發(fā)展。

人工智能與數(shù)學讀書會啟動

數(shù)十年來，人工智能的理論發(fā)展和技術(shù)實踐一直與科學探索相伴而生，尤其在以大模型為代表的人工智能技術(shù)應用集中爆發(fā)的當下，人工智能正在加速物理、化學、生物等基礎(chǔ)科學的革新，而這些學科也在反過來啟發(fā)人工智能技術(shù)創(chuàng)新。在此過程中，數(shù)學作為兼具理論屬性與工具屬性的重要基礎(chǔ)學科，與人工智能關(guān)系甚密，相輔相成。一方面，人工智能在解決數(shù)學領(lǐng)域的諸多工程問題、理論問題乃至圣杯難題上屢創(chuàng)紀錄。另一方面，數(shù)學持續(xù)為人工智能構(gòu)筑理論基石并拓展其未來空間。這兩個關(guān)鍵領(lǐng)域的交叉融合，正在揭開下個時代的科學之幕。

為了探索數(shù)學與人工智能深度融合的可能性，集智俱樂部聯(lián)合同濟大學特聘研究員陳小楊、清華大學交叉信息學院助理教授袁洋、南洋理工大學副教授夏克林三位老師，共同發(fā)起“人工智能與數(shù)學”讀書會，希望從 AI　for　Math，Math　for　AI 兩個方面深入探討人工智能與數(shù)學的密切聯(lián)系。讀書會已完結(jié)，現(xiàn)在報名可加入社群并解鎖回放視頻權(quán)限。

詳情請見：