闻乐 发自 凹非寺 量子位 | 公众号 QbitAI 陶哲轩转发，AI搞数学证明的标准习题集来了！ DeepMind最新开源 形式化数学猜想库 —— 猜想库收录了经典的形式化表述的数学猜想集合，例如，解析数论中的四个朗道问题。 不仅如此，资源库中还提供了各种代码函数，以方便用户对自然语言的数学猜想进行形式化的表述。 DeepMind的形式化数学猜想库一经建成，团队就表示所有人都可以将数学猜想添加到资源库中，呼吁大家积极参与。 感兴趣的数学家们可以行动起来了。 陶哲轩曾用Lean形式化证明了PFR猜想（多项式Freiman-Ruzsa猜想），这项成就的第一步就是将猜想的核心概念转化为计算机可验证的形 式化版本。 目前，这位"数学界的计算机推广大神"已转发此项目，并表示： "如果希望利用自动化工具帮助开放性问题，那么对这些问题进行形式化表述是重要的第一步。" 形式化数学猜想库有什么用 虽然带证明的形式化定理语料库不断扩充，但仅陈述开放式猜想的形式化资源却十分稀缺。 这类资源有望成为自动定理证明或形式化工具的测试基准，来帮助AI模型提升数学推理及证明能力。 DeepMind此次开源的猜想库在一定程度上缓解了这个问题 ...