AIGC動(dòng)態(tài)歡迎閱讀

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

關(guān)鍵字：報(bào)告,數(shù)學(xué),模型,策略,定理

文章來源：機(jī)器之心

內(nèi)容字?jǐn)?shù)：4657字

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

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

聯(lián)系作者

文章來源：機(jī)器之心

作者微信：almosthuman2014

作者簡(jiǎn)介：專業(yè)的人工智能媒體和產(chǎn)業(yè)服務(wù)平臺(tái)