AI時(shí)代，證明只需一頁(yè)紙，人類何需苦戰(zhàn)？
天才數(shù)學(xué)家陶哲軒，以他的卓越才華和敏銳洞察力，再次引領(lǐng)了數(shù)學(xué)界的潮流。這次，他將人工智能（AI）引入了數(shù)學(xué)證明領(lǐng)域，將人類對(duì)數(shù)學(xué)的探索推向了一個(gè)新的高度。
陶哲軒的這次視頻博主之旅，可謂是一鳴驚人。他選取了一個(gè)泛代數(shù)的命題，即證明Magma方程E1689蘊(yùn)含E2。即使是方程理論項(xiàng)目的合作者Bruno Le Floch，也足足人工花了一頁(yè)紙才完成證明。然而，借助AI，整個(gè)證明過(guò)程僅用時(shí)33分鐘。
AI在此過(guò)程中的角色，可謂神奇。陶哲軒將草稿拆分為微小邏輯單元，交由GitHub Copilot生成代碼骨架，再以Lean的canonical策略匹配填補(bǔ)細(xì)節(jié)。過(guò)程中也涉及部分手動(dòng)補(bǔ)全，最終，整個(gè)形式化證明能夠在Lean中通過(guò)驗(yàn)證。
這樣的操作不僅大大縮短了時(shí)間，更重要的是滿足了“人類可讀性”。Bruno Le Floch最初挑戰(zhàn)該問(wèn)題時(shí)，曾在論文中宣稱E1689-E2的所有已知證明都依賴計(jì)算機(jī)輔助。然而，經(jīng)過(guò)AI的助力，研究者成功地將證明轉(zhuǎn)化為一個(gè)人類可讀的證明。這無(wú)疑為AI在數(shù)學(xué)領(lǐng)域的角色提供了新的解讀。
陶哲軒此次嘗試并非一次成功即止。據(jù)他在視頻中透露，前兩次的證明過(guò)程都出現(xiàn)了一些“bug”。第一次拿到的代碼才到第5行他就有點(diǎn)看不懂了，所以選擇了重開；第二次雖然完成了所有證明（用時(shí)48分鐘），但由于是新人博主不太熟悉錄屏設(shè)備，導(dǎo)致屏幕分享失敗，因此又只能重來(lái)。但他并未因此氣餒，而是以積極的態(tài)度面對(duì)挑戰(zhàn)，繼續(xù)探索AI在數(shù)學(xué)證明中的應(yīng)用。
與此同時(shí)，陶哲軒開發(fā)的數(shù)學(xué)證明助手也迎來(lái)了2.0版本升級(jí)。這個(gè)輕量級(jí)證明助手的功能遠(yuǎn)遜于Lean、Isabelle或Rocq等完整證明助手，但希望它能夠輕松用于證明一些簡(jiǎn)短而繁瑣的任務(wù)。這個(gè)工具的兩個(gè)具體目標(biāo)是：為漸近分析提供支持，以及根據(jù)反饋進(jìn)行靈活的擴(kuò)展。目前這個(gè)助手有兩種模式：假設(shè)模式和策略模式。其中策略模式作為默認(rèn)模式，有點(diǎn)類似于Lean、Isabelle或Rocq里面那樣式兒的策略模式。
陶哲軒對(duì)這個(gè)證明助手的改進(jìn)感到非常滿意，并愿意接受進(jìn)一步的建議或貢獻(xiàn)新的功能。他表示這個(gè)工具足夠靈活，可以為解決一些看似棘手的問(wèn)題提供幫助。他還計(jì)劃引入新的數(shù)據(jù)類型、公例和策略，或者貢獻(xiàn)一些有難度的例子。此外，他還計(jì)劃開發(fā)用于估算符號(hào)函數(shù)的函數(shù)空間規(guī)范的工具。
天才數(shù)學(xué)家陶哲軒的這次嘗試，讓我們看到了AI在數(shù)學(xué)領(lǐng)域的無(wú)限可能。他以自己的實(shí)際行動(dòng)證明了AI在數(shù)學(xué)證明中的強(qiáng)大作用，將人類對(duì)數(shù)學(xué)的探索推向了一個(gè)新的高度。在這個(gè)AI時(shí)代，我們看到了證明只需一頁(yè)紙的可能，也看到了人類在數(shù)學(xué)領(lǐng)域探索的新方向。
總的來(lái)說(shuō)，陶哲軒的這次嘗試給我們提供了一個(gè)全新的視角來(lái)看待AI與數(shù)學(xué)的關(guān)系。我們期待在未來(lái)的日子里，會(huì)有更多的數(shù)學(xué)家和科學(xué)家投身于此，共同探索AI在數(shù)學(xué)領(lǐng)域的無(wú)限可能。在這個(gè)過(guò)程中，我們也將更深入地理解數(shù)學(xué)的本質(zhì)，以及它在人類文明中的重要地位。
（免責(zé)聲明：本網(wǎng)站內(nèi)容主要來(lái)自原創(chuàng)、合作伙伴供稿和第三方自媒體作者投稿，凡在本網(wǎng)站出現(xiàn)的信息，均僅供參考。本網(wǎng)站將盡力確保所提供信息的準(zhǔn)確性及可靠性，但不保證有關(guān)資料的準(zhǔn)確性及可靠性，讀者在使用前請(qǐng)進(jìn)一步核實(shí)，并對(duì)任何自主決定的行為負(fù)責(zé)。本網(wǎng)站對(duì)有關(guān)資料所引致的錯(cuò)誤、不確或遺漏，概不負(fù)任何法律責(zé)任。
任何單位或個(gè)人認(rèn)為本網(wǎng)站中的網(wǎng)頁(yè)或鏈接內(nèi)容可能涉嫌侵犯其知識(shí)產(chǎn)權(quán)或存在不實(shí)內(nèi)容時(shí)，應(yīng)及時(shí)向本網(wǎng)站提出書面權(quán)利通知或不實(shí)情況說(shuō)明，并提供身份證明、權(quán)屬證明及詳細(xì)侵權(quán)或不實(shí)情況證明。本網(wǎng)站在收到上述法律文件后，將會(huì)依法盡快聯(lián)系相關(guān)文章源頭核實(shí)，溝通刪除相關(guān)內(nèi)容或斷開相關(guān)鏈接。 ）
