陶哲軒力薦！史上最全「數學AI資源」清單出爐

新智元報道

編輯：好睏 桃子

【新智元導讀】陶哲軒轉發的這份「數學AI資源清單」，乾貨滿滿，全到讓你震撼。

史上最全的「數學人工智能資源」清單出爐了。

陶哲軒，信奉AI將在2026年成爲人類數學家的重要合著者，一早便轉發了這份清單。

文檔地址：

https://docs.google.com/document/d/1kD7H4E28656ua8jOGZ934nbH2HcBLyxcRgFDduH5iQ0/edit

正如文檔所介紹，「這是爲那些希望涉足數學AI領域的人士準備的初步資源列表」。

去年，美國國家科學院「AI輔助數學推理」研討會期間發起了這份清單行動。

它是由UIUC的助理教授Talia Ringer進行了整理。

據介紹，這份清單還不是最終版。每個人都可以針對文檔內容進行編輯和評論。

從修改批註中可以看出，陶哲軒本人貢獻了自己的一份力量。

有網友表示，「不僅我需要這個，我的學生們也會失去理智」。

目錄

這份長達12頁的文檔，可謂是乾貨滿滿，從自學材料、論壇、工具，到研究平臺的各種資源應有盡有。

先來直觀看一看這份文檔的目錄。

教育

這部分提供了一些教育資源。

教科書和調查論文

- 形式化證明

- 機器學習

維基和詞彙表

- 編程語言

- 數學

教程

- 形式化證明

- 形式化證明的機器學習

- 機器學習

課程資料

- 「自動化證明」，Talia Ringer

- 「形式化數學」，Kevin Buzzard

- 「機器學習」，吳恩達

- 面相職業數學家的機器學習

- 賓夕法尼亞大學軟件基礎課程

- Lean教學和課程網頁

- 「實分析」，Patrick Massot

- 「邏輯驗證指南」，Anne Baanen

合作

這是多個領域高度融合的一個交叉點，因此，知道如何與具有互補專業知識、經驗或興趣的人建立聯繫非常重要。

工具和資源庫

這個列表包括了一些對於初入此領域的人可能有用的工具。

機器學習框架

- PyTorch

- Tensorflow

- JAX

證明助手

AI在數學領域的一個研究方向是結合AI自動化技術和機器可驗證的證明。以下是一些可以用於編寫的工具列表：

- Lean

- Coq

- Isabelle

- HOL4

- HOL Light

- Agda

- Cubical Agda

約束求解器

計算數學工具

數學數據庫

集成AI數學工具

數據集和基準測試

下述資源可以作爲訓練數據或用於評估性能。部分資源提供了標準的訓練/測試劃分，而部分則沒有。

在構建任何工具時，務必注意避免讓測試數據污染訓練集，以保證結果的有效性。

另外，HuggingFace提供了衆多公共數據集和基準測試套件，是一個值得查看的好資源。

語言模型和聊天機器人

AI工具若能被託管機構之外的人下載，通常會被標爲「開源」。然而，這些工具往往伴隨着嚴格的使用和分發限制。

以下內容將會按照OSI的 定義，使用「自由和開源」這個術語。

對於那些標爲「公開可用」的模型，使用前務必仔細閱讀其許可協議，以避免對使用權限的誤解。

通用模型

數學模型

形式化證明模型

聊天機器人

研究

以下是關於這個領域的研究成果及其查找途徑。

參考

活動

激勵

某些領域特有的激勵結構對於大規模合作、開發實用工具和形式化證明等工作很有幫助。

參考資料：

https://docs.google.com/document/d/1kD7H4E28656ua8jOGZ934nbH2HcBLyxcRgFDduH5iQ0/edit