要點:

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

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

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

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

（投訴）