新智元报道  

编辑：好困 桃子
【新智元导读】陶哲轩转发的这份「数学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



内容中包含的图片若涉及版权问题，请及时与我们联系删除