形式化證明與大模型：共創可驗證的AI數學未來｜量子位直播
本周四晚20:00，一起來聊聊AI數學吧～
林樾 發自 凹非寺
量子位｜公眾號 QbitAI
就在5月，前有DeepSeek Prover V2發布，后有陶哲軒的AI數學直播，還有谷歌最新發布的AlphaEvolve。
大模型“解數學題”的能力已經是衡量AI「智能天花板」的一種方式，正吸引著無數團隊爭相挑戰。
為了更好地評估AI完成數學推理的能力，近期發布的FormalMATH基準測試也備受關注。
現在，AI完成自動定理證明的表現與挑戰究竟如何？主流的技術路徑是什么？AI完成形式化證明的能力，又將對大模型應用帶來怎樣的影響？
為了回答這些問題，5月29日20:00，我們與2077AI開源基金會共同邀請到了來自FormalMath、Kimina等項目團隊的成員，一同來討論大語言模型形式化證明前沿探索。
歡迎在量子位視頻號預約直播：形式化證明、大模型與AI數學未來
直播嘉賓
付杰，上海人工智能實驗室青年科學家，上海創智學院博士導師
李祎哲，浙江大學博士生，數學領域青年研究者
劉明皓，資深算法工程師，2077AI核心發起人、貢獻者
劉威楊，香港中文大學博士生導師，助理教授
劉征瀛，月之暗面（Moonshot AI）研究員，Kimina Co-author
王海明，月之暗面（Moonshot AI）研究員，Kimina Co-author
辛華劍，愛丁堡大學博士生，字節跳動Seed實習生
郁晝亮，香港中文大學博士生
* 順序按首字母音序排列。
直播議程
本周四晚20:00，一起來聊聊AI數學吧～
版權所有，未經授權不得以任何形式轉載及使用，違者必究。
- 嘉賓全陣容揭曉！張亞勤孫茂松，百度小米商湯谷歌都要來MEET20262025-12-04
- 下周三！量子位的這件大事就要來了｜MEET20262025-12-04
- 第三波嘉賓來襲！等你一起MEET2026，速戳報名2025-11-28
- 搶先報名！第二波嘉賓亮相，百度京東高通亞馬遜都來了｜MEET20262025-11-20
相關閱讀
