陶哲轩力荐，史上最全「数学AI资源」清单出炉
陶哲轩力荐，史上最全「数学AI资源」清单出炉
数学与人工智能的结合是当前科技领域的热门话题。近日，一份由UIUC助理教授Talia Ringer整理的「数学人工智能资源」清单在网络上广为流传，这份清单得到了著名数学家陶哲轩的认可。
这份长达12页的文档，可谓是干货满满，从自学材料、论坛、工具，到研究平台的各种资源应有尽有。
教育
这部分提供了一些教育资源。
教科书和调查论文
形式化证明
机器学习
维基和词汇表
编程语言
数学
教程
形式化证明
形式化证明的机器学习
机器学习
课程资料
「自动化证明」，Talia Ringer
「形式化数学」，Kevin Buzzard
「机器学习」，吴恩达
面相职业数学家的机器学习
宾夕法尼亚大学软件基础课程
Lean教学和课程网页
「实分析」，Patrick Massot
「逻辑验证指南」，Anne Baanen
合作
这是多个领域高度融合的一个交叉点，因此，知道如何与具有互补专业知识、经验或兴趣的人建立联系非常重要。
工具和资源库
这个列表包括了一些对于初入此领域的人可能有用的工具。
机器学习框架
PyTorch
Tensorflow
JAX
证明助手
Lean
Coq
Isabelle
HOL4
HOL Light
Agda
Cubical Agda
约束求解器
计算数学工具
数学数据库
集成AI数学工具
数据集和基准测试
下述资源可以作为训练数据或用于评估性能。部分资源提供了标准的训练/测试划分，而部分则没有。在构建任何工具时，务必注意避免让测试数据污染训练集，以保证结果的有效性。另外，HuggingFace提供了众多公共数据集和基准测试套件，是一个值得查看的好资源。
语言模型和聊天机器人
AI工具若能被托管机构之外的人下载，通常会被标为「开源」。然而，这些工具往往伴随着严格的使用和分发限制。以下内容将会按照OSI的定义，使用「自由和开源」这个术语。对于那些标为「公开可用」的模型，使用前务必仔细阅读其许可协议，以避免对使用权限的误解。
- 通用模型
- 数学模型
- 形式化证明模型
- 聊天机器人
研究
以下是关于这个领域的研究成果及其查找途径。
参考
活动
激励
某些领域特有的激励结构对于大规模合作、开发实用工具和形式化证明等工作很有帮助。
参考资料：
https://docs.google.com/document/d/1kD7H4E28656ua8jOGZ934nbH2HcBLyxcRgFDduH5iQ0/edit