Building an AI Mathematician with Carina Hong - #754

摘要

訪談 Axiom 執行長 Karina Hong，探討結合大語言模型、形式化證明語言 Lean 與程式碼生成技術，打造能自主推導數學定理的「AI 數學家」。內容涵蓋自動形式化挑戰、資料匱乏問題及未來應用，適合對 AI 與數學交叉領域感興趣的開發者與研究者。

Interview with Karina Hong on building an AI mathematician by combining LLMs, formal proof languages, and code generation.

摘要、重點與章節標題由語言模型整理，細節（誰說的、數字、先後）可能有誤；要引用請以原始內容為準。

重點

• 結合 LLM、Lean 與程式碼生成技術打造 AI 數學家
• 解決自然語言證明轉形式化驗證的資料與技術難題
• 探討數學驗證在軟體硬體高風險領域的應用前景

章節

依話題轉折切分，標題由 AI 產生

1. 00:00數學與程式碼是數位世界核心
2. 03:58為何現在是數學與 AI 結合契機
3. 07:08Lean 如何讓數學證明像程式碼般嚴謹
4. 11:45自動形式化與證明應整合於單一模型
5. 17:39如何設計課程讓模型跨越不同數學層級
6. 20:37建構能自我改進的數學證明系統
7. 23:55數學作為測試自我改進 AI 的實驗室
8. 26:34數學資料稀缺與自監督學習機會
9. 29:04跨領域人才招募與數學發現策略
10. 34:49自動形式化技術現狀與挑戰
11. 42:04幾何領域特殊性及定義學習難題
12. 46:18數學商業化價值與形式驗證市場
13. 50:27產品公司路線與自然語言介面設計
14. 53:09深科技研發優先與里程碑達成

提到的工具與公司

• Lean
• Axiom

適合誰看

對 AI 數學應用、形式化驗證或深度技術研發感興趣的開發者與研究者。

摘要依據

講者

Sam Charrington

依據

語音轉文字

為什麼排在這裡

人氣

0.50

新鮮

0.28

在主題頁與搜尋結果裡，名次由相關、人氣、新鮮三個分數決定；這一頁沒有搜尋的關鍵字，所以沒有相關分數。排序怎麼算

相關內容

• Carina Hong: Can AI Do Math? Lean Proofs, Ancient Intuition & the Mystery of Mathematics影片 ・ Zhang Xiaojun Podcast ・ 4 小時 23 分（在新分頁開啟原站）
• AI That Can Prove It’s Right: Verification as the Missing Layer in AI — Carina HongPodcast ・ The MAD Podcast ・ 1 小時 4 分
• 🔬Scaling Past Informal AI - Carina Hong, Axiom MathPodcast ・ Latent Space ・ 1 小時 33 分
• The $64M Bet on an AI That Has to Be Right | Carina Hong, CEO of AxiomPodcast ・ Gradient Dissent ・ 51 分鐘
• When you keep AI Lean, you keep AI correctPodcast ・ The Stack Overflow Podcast ・ 25 分鐘
• Erdős问题为何会成为AI的新竞技场 | AI数学证明 | OpenAI | 保罗·埃尔德什 | 大语言模型 | 人工智能 | 陶哲轩 | 菲尔兹奖 | 数论 | Astra模型影片 ・ Best Partners TV ・ 17 分鐘（在新分頁開啟原站）