國內首次實現AI自主解決數學開放問題

??6日，記者從北京大學北京國際數學研究中心了解到，該中心董彬教授課題組與合作者組建的AI4Math團隊用自主構建的自動化AI框架解決了交換代數中一個開放問題——安德森猜想，并在用于形式化驗證數學定理正確性的編程語言和定理證明器——Lean中完成了約19000行的形式化驗證。這是國內首次以AI框架攻克交換代數開放問題并實現大規模形式化驗證，開辟了數學與AI深度融合的更多可能。

??安德森猜想由美國數學家安德森于2014年提出，它關注的是“準完備局部環”的一類性質——這類環旨在用代數工具刻畫幾何對象局部（如某點附近）的無窮小結構與變形。該猜想提出后十余年始終無人突破。

??此次解決安德森猜想，北京大學AI4Math團隊搭建的雙智能體協作框架功不可沒。該框架由自然語言推理智能體Rethlas和形式化驗證智能體Archon組成。

??研究中，Rethlas通過團隊自研的Matlas自然語言語義檢索系統，從上千萬條數學陳述中精準定位到與猜想看似無關的整環完備化理論成果，以此構造反例。隨后，Archon將證明轉化為約19000行Lean代碼，并在過程中自主發現初始方案存在隱含的邏輯漏洞，重新設計了形式化證明的整體技術路線，還在所需數學概念于Lean形式化數學庫中尚未收錄時，自主找到等價替代路徑，最終完成的代碼覆蓋6篇外部論文關鍵結果，完成同等規模形式化工作的效率較經驗豐富的Lean專家提升至少10倍。

??該成果的背后是團隊三年的技術積累與跨學科協作。2023年，北京大學AI4Math團隊正式組建，它由一群對這個方向有共同判斷的人逐步自然匯聚而成，團隊成員來自代數與數論、優化、機器學習與人工智能等方向。

??董彬告訴科技日報記者，團隊認為，讓AI做嚴肅數學推理，檢索最為關鍵。他們打造了雙引擎檢索架構——LeanSearch和Matlas。LeanSearch用自然語言描述需求即可語義檢索出相關定理，現已被Lean官方社區廣泛使用。Matlas則覆蓋上千萬條數學陳述，支持命題級語義檢索。在這些基礎設施之上，他們搭建了前述兩個AI智能體。

??北京大學數學科學學院院長、中國科學院院士劉若川指出，此次探索不僅解決了具體數學問題，更驗證了AI與數學融合的新研究范式。中國科學院院士田剛由此呼吁，應鼓勵和支持青年學者大膽創新，進一步推動AI與數學的深度融合，并在國家急需解決的重大科技問題中發揮關鍵作用。（記者張蓋倫）

【責任編輯:周靖杰】