要點：
陶哲軒成功利用 AI 工具形式化多項式 Freiman-Ruzsa 猜想的證明，標誌著數學研究中人工智能的廣泛應用，引發數學界的震動。
他強調數學研究者應學會正確使用 AI 工具，認為形式化證明的主流化有望創造出既人類可讀又機器可解的證明，將數學變成一種編程。
陶哲軒團隊利用 Blueprint 工具，將證明過程分解成易於處理的部分，通過眾多貢獻者並行工作，成功形式化了 PFR 猜想。
站長之家（ChinaZ.com）12 月 6 日消息：近期，陶哲軒成功利用 AI 工具形式化了多項式 Freiman-Ruzsa 猜想的證明，這一成果引起了數學界的廣泛關注。他在博文中詳細記錄了使用 Blueprint 在 Lean4 中形式化證明的過程。這一項目歷時三周，成功實現了多項式 Freiman-Ruzsa 猜想的證明形式化，讓人驚嘆於人工智能在數學研究中的威力。
陶哲軒對這一成果的解讀強調了正確使用 AI 工具的重要性。他認為，形式化證明的主流化有望創造出既人類可讀又機器可解的證明，從而將數學變成一種更加高效的編程。他特別推崇了 Blueprint 工具，該工具使團隊能夠編寫與 Lean 形式化相關的、人類可讀的證明「藍圖」。在這個項目中，綠色的氣泡或矩形表示已經被完全形式化的引理或定義，而藍色的表示準備好進行形式化的引理或定義，展示了項目形式化進展的大致快照。
© 由 站長之家 提供
他強調了使用 Blueprint 將項目分解成易於處理的部分的效果，使大量並行工作成為可能。這也讓不具備 Lean 編程技能的數學家能夠領導形式化項目。陶哲軒團隊的目標是將所有通向「pfr」氣泡的底部氣泡變成綠色，最終 Lean 成功證明了 PFR 猜想，圓滿完成了項目的主要目標。
Fullscreen button
image.png
image.png
© 由 站長之家 提供
他的成果引發了關於數學研究未來的討論。一些人認為，形式化將成為主流數學中的關鍵趨勢，大多數證明可能只在類似系統中完成，不再需要費心寫人類可讀的論文。然而，陶哲軒提醒不要混淆「計算機輔助證明」和「不能提供理解 / 偶然成立的證明」，強調形式化並不削弱理解證明的重要性。這一成果展示了形式化在主流數學中的受關注程度，為未來的數學研究指明了可能的方向。
Fullscreen button
image.png