A 4-hour Interview with Carina Hong: AI for Math, Lean, Proofs from The Book, and Intuition

AI for Math 致力於透過 AI 與形式化語言（Lean）結合，實現數學證明與自動化推理的革命。數學作為介於藝術與科學間的文明體系，AI 透過邏輯驗證與蠻力運算，能有效輔助人類突破發現瓶頸。Axiom 創辦人洪樂潼強調，AI 數學家不僅能解決複雜難題，更具備泛化潛力，作為科學探索的驗證工具，能有效解決大語言模型常見的幻覺問題。核心在於將數學轉化為可驗證的代碼，透過自動化推理與知識庫建設，推動科學發現的指數級增長。這場「登月」式的技術探索，旨在建立一個具自我驗證能力的推理系統，讓數學與編碼成為推動未來智能發展的核心引擎。