要點(diǎn):

益美檔案文件銷(xiāo)毀公司12月6日 音訊:近期，陶哲軒成功利用AI工具形式化了多項(xiàng)式Freiman-Ruzsa推想的證明，這一成果引發(fā)了數(shù)學(xué)界的廣泛關(guān)注。他在博文中詳細(xì)記錄了使用Blueprint在Lean4中形式化講明的工序。這一項(xiàng)目歷時(shí)三周，成功兌現(xiàn)了多項(xiàng)式Freiman-Ruzsa揣測(cè)的標(biāo)明形式化，讓人驚嘆于人工智能在數(shù)學(xué)斟酌中的威力。

陶哲軒對(duì)這一成果的解讀強(qiáng)調(diào)了切實(shí)使用AI工具的首要性。他認(rèn)為，形式化說(shuō)明的主流化有望創(chuàng)造出既人類(lèi)可讀又機(jī)器可解的說(shuō)明，從而將數(shù)學(xué)變成一種更加高效的編程。他非常推崇了Blueprint工具，該工具使團(tuán)隊(duì)沒(méi)準(zhǔn)編寫(xiě)與Lean形式化相關(guān)的、人類(lèi)可讀的標(biāo)明「藍(lán)圖」。在這個(gè)項(xiàng)目中，綠色的氣泡或矩形表態(tài)曾經(jīng)被完全形式化的引理或定義，而藍(lán)色的表示準(zhǔn)備好進(jìn)行形式化的引理或定義，顯示了項(xiàng)目形式化進(jìn)展的大致快照。

他強(qiáng)調(diào)了使用Blueprint將項(xiàng)目分解成易于處理的部分的效果，使大批并行工作成為也許。這也讓不具備Lean編程技能的數(shù)學(xué)家或者率領(lǐng)形式化項(xiàng)目。陶哲軒團(tuán)隊(duì)的目標(biāo)是將所有通向「pfr」氣泡的底部氣泡變成綠色，最終Lean成功說(shuō)明了PFR猜測(cè)，圓滿(mǎn)兌現(xiàn)了項(xiàng)目的首要目標(biāo)。

他的成果引起了關(guān)于數(shù)學(xué)探討將來(lái)的討論。一些人認(rèn)為，形式化將成為主流數(shù)學(xué)中的關(guān)鍵趨勢(shì)，大部分證明或者只在類(lèi)似系統(tǒng)中實(shí)行，不再需要費(fèi)心寫(xiě)人類(lèi)可讀的論文。然而，陶哲軒提醒不要混淆「計(jì)算機(jī)輔助表明」和「不能提供理解/偶然成立的闡揚(yáng)」，強(qiáng)調(diào)形式化并不削弱理解講明的重要性。這一成果展現(xiàn)了形式化在主流數(shù)學(xué)中的受關(guān)注程度，為將來(lái)的數(shù)學(xué)研究指明了或者的方向。

（投訴）