IXThinker·2025-05-15 20:40

陶哲軒測試AI形式化證明 Claude勝出

數學家陶哲軒在YouTube發布第二輪AI形式化實驗，讓AI在Lean證明輔助工具中形式化同一代數蘊含證明，結果Claude約20分鐘完成，o4-mini則中途放棄。

兩模型同場較量

今次任務是基於先前的非形式化與形式化證明，生成Lean形式化代碼。Claude表現穩定，約20分鐘完成整個證明；o4-mini則因過於謹慎，遲遲不敢下手，最終「棄賽」。