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

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)

粵公網(wǎng)安備 44011502001135號(hào)