AI顛覆數(shù)學(xué)研究！陶哲軒借AI數(shù)學(xué)猜想，形式化成功驚呆數(shù)學(xué)圈

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

原標(biāo)題：AI顛覆數(shù)學(xué)研究！陶哲軒借AI數(shù)學(xué)猜想，形式化成功驚呆數(shù)學(xué)圈

關(guān)鍵字：報告,目標(biāo),數(shù)學(xué),氣泡,人類

文章來源：新智元

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

內(nèi)容摘要：新智元報道編輯：編輯部【新智元導(dǎo)讀】歷時三周，陶哲軒成功地用AI工具完成了形式化多項式Freiman-Ruzsa猜想證明過程的工作。他再次呼吁數(shù)學(xué)研究者學(xué)會正確利用AI工具，網(wǎng)友驚呼：以后的數(shù)學(xué)論文不需要人類可讀了？用AI工具輔助研究數(shù)學(xué)的項目，再一次被陶哲軒跑通！三周前，他曾發(fā)布一篇博文，記錄下自己使用Blueprint在Lean4中形式化多項式Freiman-Ruzsa猜想的證明過程。就在昨天，他激動宣布：將多項式Freiman-Ruzsa猜想的證明形式化的Lean4項目，在三周后取得了成功！現(xiàn)在，依賴關(guān)系圖已經(jīng)完全被綠色所覆蓋，Lean編譯器也報告說，這個猜想完全遵循標(biāo)準(zhǔn)公理。陶哲軒表示，在整個團(tuán)隊中，自己貢獻(xiàn)的代碼大概只有5%。這個結(jié)果很鼓舞人心，因為這意味著數(shù)學(xué)家即使不具備Lean編程技能，也能領(lǐng)導(dǎo)Lean的形式化項目。他發(fā)現(xiàn)，項目中在數(shù)學(xué)上最有趣的部分，形式化起來比較容易，而技…

原文鏈接：點此閱讀原文：AI顛覆數(shù)學(xué)研究！陶哲軒借AI數(shù)學(xué)猜想，形式化成功驚呆數(shù)學(xué)圈

聯(lián)系作者

文章來源：新智元

作者微信：AI_era

作者簡介：智能+中國主平臺，致力于推動中國從互聯(lián)網(wǎng)+邁向智能+新紀(jì)元。重點關(guān)注人工智能、機(jī)器人等前沿領(lǐng)域發(fā)展，關(guān)注人機(jī)融合、人工智能和機(jī)器人對人類社會與文明進(jìn)化的影響，領(lǐng)航中國新智能時代。