陶哲軒青睞的證明助手Lean，用上了大模型

AIGC動態歡迎閱讀

原標題：陶哲軒青睞的證明助手Lean，用上了大模型

關鍵字：報告,數學,模型,策略,定理

文章來源：機器之心

內容字數：4657字

內容摘要：機器之心報道編輯：陳萍現在，數學輔助證明工具都用上了大模型。「我預計，如果使用得當，到 2026 年，AI 將成為數學研究和許多其他領域值得信賴的合著者。」數學家陶哲軒在之前的一篇博客中說道。陶哲軒這樣說了，也這樣做了。他最近一直在用 GPT-4、Copilot、Lean 等工具進行數學研究，并且還在 AI 的幫助下發現了自己論文中的一處隱藏 bug。不僅如此，前幾天，陶哲軒表示：對多項式 Freiman-Ruzsa 猜想（PFR）的證明進行形式化的 Lean4 項目成功完成，并且耗時僅三周時間。Lean 編譯器也報告該猜想符合標準公理，可以說這是計算機和 AI 輔助證明的一項巨大成功。關于上述研究的更多內容，感興趣的讀者可以參考《》。看到這，細心的讀者可能已經發現了端倪，陶大神在進行數學研究時，多次都提到過 Lean。簡單來講，Lean 是一種可幫助數學家驗證定理的編程語言，用戶可以在其…

原文鏈接：點此閱讀原文：陶哲軒青睞的證明助手Lean，用上了大模型

聯系作者

文章來源：機器之心

作者微信：almosthuman2014

作者簡介：專業的人工智能媒體和產業服務平臺