北京
林樾 發自 凹非寺
量子位｜公眾號 QbitAI
就在5月，前有DeepSeek Prover V2發布，后有陶哲軒的AI數學直播，還有谷歌最新發布的AlphaEvolve。
大模型“解數學題”的能力已經是衡量AI「智能天花板」的一種方式，正吸引著無數團隊爭相挑戰。
為了更好地評估AI完成數學推理的能力，近期發布的FormalMATH基準測試也備受關注。
現在，AI完成自動定理證明的表現與挑戰究竟如何？主流的技術路徑是什么？AI完成形式化證明的能力，又將對大模型應用帶來怎樣的影響？
為了回答這些問題，5月29日20:00，我們與2077AI開源基金會共同邀請到了來自DeepSeek Prover、FormalMath、Kinima等項目團隊的成員，一同來討論大語言模型形式化證明前沿探索。
歡迎在量子位視頻號預約直播：形式化證明、大模型與AI數學未來
直播嘉賓
辛華劍，愛丁堡大學博士生，DeepSeek Prover 項目第一作者
劉威揚，香港中文大學博士生導師，資深學者
付杰，上海人工智能實驗室研究員，人工智能領域專家
郁晝亮，香港中文大學博士生，FormalMath 項目第一作者
王海明，月之暗面（Moonshot AI）技術負責人，Kinima 項目技術領銜人
劉征瀛，月之暗面（Moonshot AI）技術負責人，資深技術專家
李祎哲，浙江大學博士生，數學領域青年研究者
劉明皓，資深算法工程師，2077AI核心發起人、貢獻者
直播議程
本周四晚20:00，一起來聊聊AI數學吧～
特別聲明：以上內容(如有圖片或視頻亦包括在內)為自媒體平臺“網易號”用戶上傳并發布，本平臺僅提供信息存儲服務。
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.
