陶哲軒最新采訪:AI將顛覆數(shù)學(xué)界!用Lean規(guī)模化,成百上千條定理一次秒殺

AIGC動(dòng)態(tài)歡迎閱讀
原標(biāo)題:陶哲軒最新采訪:AI將顛覆數(shù)學(xué)界!用Lean規(guī)模化,成百上千條定理一次秒殺
關(guān)鍵字:數(shù)學(xué),人工智能,數(shù)學(xué)家,人類,領(lǐng)域
文章來源:新智元
內(nèi)容字?jǐn)?shù):0字
內(nèi)容摘要:
新智元報(bào)道編輯:庸庸 喬楊
【新智元導(dǎo)讀】陶哲軒在最新的采訪中,系統(tǒng)地談到了AI可能會(huì)對(duì)數(shù)學(xué)領(lǐng)域產(chǎn)生的影響。他樂觀地認(rèn)為,使用Lean等工具「形式化」數(shù)學(xué),在AI的輔助下實(shí)現(xiàn)規(guī)模化生產(chǎn)——一次證明數(shù)百或數(shù)千條定理。但他也審慎地預(yù)測(cè),數(shù)學(xué)問題在短期內(nèi)不會(huì)像國(guó)際象棋一樣被「解決」,但有可能會(huì)提高人類科學(xué)家的洞察力。數(shù)學(xué)歷來是一門孤獨(dú)的科學(xué)。
1986 年,安德魯·懷爾斯(Andrew Wiles)為了證明費(fèi)馬大定理,遁入書齋長(zhǎng)達(dá)七年之久。
數(shù)學(xué)家苦心孤詣得到的證明往往讓同行難以理解,有些證明至今仍有爭(zhēng)議。
但近年來,越來越多的數(shù)學(xué)領(lǐng)域被嚴(yán)格分解成各個(gè)組成部分,我們稱之為「形式化」(formalized),這就可以讓計(jì)算機(jī)來檢查和驗(yàn)證數(shù)學(xué)證明。
菲爾茲獎(jiǎng)得主、加州大學(xué)洛杉磯分校教授陶哲軒堅(jiān)信,這些方法為數(shù)學(xué)領(lǐng)域的合作開辟了全新的可能性。
如果再加上人工智能的最新進(jìn)展,在未來幾年里,數(shù)學(xué)領(lǐng)域可能會(huì)出現(xiàn)全新的工作方式。
在計(jì)算機(jī)的幫助下,一些重大問題可能會(huì)被更快解決。
陶哲軒在接受《科學(xué)美國(guó)人》的德語(yǔ)姊妹刊物Spektrum der Wissenschaft的采訪時(shí)闡述了他對(duì)未來的看法。
以下
原文鏈接:陶哲軒最新采訪:AI將顛覆數(shù)學(xué)界!用Lean規(guī)模化,成百上千條定理一次秒殺
聯(lián)系作者
文章來源:新智元
作者微信:AI_era
作者簡(jiǎn)介:智能+中國(guó)主平臺(tái),致力于推動(dòng)中國(guó)從互聯(lián)網(wǎng)+邁向智能+新紀(jì)元。重點(diǎn)關(guān)注人工智能、機(jī)器人等前沿領(lǐng)域發(fā)展,關(guān)注人機(jī)融合、人工智能和機(jī)器人對(duì)人類社會(huì)與文明進(jìn)化的影響,領(lǐng)航中國(guó)新智能時(shí)代。

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