陶哲軒轉發！DeepMind開源「AI數學證明標準習題集」
陶哲軒轉發，AI搞數學證明的標準習題集來了！
DeepMind最新開源形式化數學猜想庫——
猜想庫收錄了經典的形式化表述的數學猜想集合，例如，解析數論中的四個朗道問題。
不僅如此，資源庫中還提供了各種代碼函數，以方便用戶對自然語言的數學猜想進行形式化的表述。
陶哲軒曾用Lean形式化證明了PFR猜想（多項式Freiman-Ruzsa猜想），這項成就的第一步就是將猜想的核心概念轉化為計算機可驗證的形式化版本。
目前，這位“數學界的計算機推廣大神”已轉發此項目，并表示：
“如果希望利用自動化工具幫助開放性問題，那么對這些問題進行形式化表述是重要的第一步。”
DeepMind的形式化數學猜想庫一經建成，團隊就表示所有人都可以將數學猜想添加到資源庫中，呼吁大家積極參與。
感興趣的數學家們可以行動起來了。
形式化數學猜想庫有什么用
雖然帶證明的形式化定理語料庫不斷擴充，但僅陳述開放式猜想的形式化資源卻十分稀缺。
這類資源有望成為自動定理證明或形式化工具的測試基準，來幫助AI模型提升數學推理及證明能力。
DeepMind此次開源的猜想庫在一定程度上緩解了這個問題。
它收錄了使用Lean形式化表述的數學猜想集合，這些猜想來源于各個途徑，并且類型多樣。
下圖展示了題目類別統計。
這個猜想庫相當于為計算機寫了一套形式化的“習題集”，還是能夠隨時擴充并且自帶審核的那種！
有了這個“習題集”，傳統ATP（自動推理證明）就可以直接基于里面的命題進行證明搜索，比如使用歸結法嘗試推導矛盾或驗證等。
除此之外，將猜想庫作為訓練數據，就能讓模型學習數學猜想的模式，AI就有可能提出新猜想。
例如，AlphaGeometry（DeepMind開發的專門用于自動解決奧林匹克幾何題的AI系統）就能夠依賴合成幾何猜想訓練模型。
可以說，形式化數學猜想庫是AI+ATP范式的關鍵前置步驟。
目前，該猜想庫剛剛起步，團隊希望更多人能參與其中，豐富猜想庫的內容。
所有感興趣的用戶都可以通過以下這幾種方式參與其中：
1. 添加新的問題形式化：猜想可以來自各種地方，包括數學教科書、研究論文、專用問題列表等。
2. 提出你希望的形式化問題：建議包含參考文獻鏈接和精確的非正式表述。
3. 改進問題的引用和標記：為現有命題添加參考文獻或補充AMS學科分類標簽。
4. 修復錯誤的形式化：鼓勵通過提交PR修復不準確的表述，或提交issue反饋潛在缺陷。
那么如何操作呢？
接下來，讓我們給大家解答。
流程大致分為這樣幾個步驟：
首先，你要在在GitHub上創建問題，清晰描述計劃貢獻的內容，包括對要添加的數學猜想的概述、相關背景信息以及自己對該猜想的初步理解等，然后將問題分配給自己，以便跟蹤和管理貢獻進度。
并且，可以從官方倉庫Fork一份到自己的GitHub賬戶下進行修改。
然后，按照倉庫的目錄結構和組織方式，確定猜想應該放置的具體的位置，再將你的形式化猜想添加到適當的文件/目錄結構中。
下一步就是在本地運行lake build命令，避免出現語法錯誤或其他導致系統無法正常運行的問題，確保添加或修改后的代碼能夠成功構建。
完成上述步驟就可以向官方倉庫提交拉取請求了，隨后等待即可～
并且，由于無證明的數學猜想的形式化過程中可能出現細微錯誤，猜想庫將通過人工審核和AlphaProof（通用數學自動證明系統，結合了LLM和符號推理引擎）輔助識別。
DeepMind與陶哲軒
說來，陶哲軒與DeepMind也是互動頗多。
早在2023年，DeepMind提出FunSearch——一種能夠為數學和計算機科學問題搜索解決方案的方法。
陶哲軒就曾稱贊FunSearch是“利用LLM進行數學發現的有前途的范式” 。
該方法首次證明LLMs可以生成用計算機代碼編寫的函數，相關工作發表在《Nature》雜志上。
就在前不久，谷歌DeepMind與陶哲軒等一眾頂尖科學家一起共同打造了AlphaEvolve——一個LLM驅動的進化編碼Agent，用于通用算法的發現與優化。
幾百年未曾解決的幾何挑戰接吻數（Kissing Number）問題，也都因為它的出現前進了一大步。
它發現了一個由593個外球體組成的結構，直接刷新了11維空間中的下限。
AlphaEvolve團隊將其應用于數學分析、幾何學、組合學和數論等多個領域。
在大約75%的案例中，它能夠重新發現最先進的解決方案。
在20%的案例中，它改進了之前已知的最佳解決方案。
可以說，這是AI與數學的一次里程碑式碰撞。
陶哲軒表示AlphaEvolve的數學潛力仍在開發之中，讓我們一起期待更多進展吧。
形式化數學猜想庫：https://google-deepmind.github.io/formal-conjectures/項目地址：https://github.com/google-deepmind/formal-conjectures
