刚刚，谷歌DeepMind开源形式化数学猜想库，陶哲轩也转发！ 尽管包含证明的形式化定理库正在不断扩充，但仅陈述猜想本身的形式化资源却依然十分匮乏。 DeepMind此次开源的资源库，收录了使用Lean形式化表述的数学猜想集合。例如，解析数论中的四个朗道问题已在其中完成形式化。【图2】 这类资源的丰富，不仅能通过形式化澄清猜想的精确含义，更是有望成为自动化定理证明工具和形式化工具的基准测试集。 正如陶哲轩所强调的： “提出一个开放性问题远比证明它简单，但若希望借助自动化工具推动这些问题的发展，建立标准化的表述形式是至关重要的第一步。”【图1】 他指出，如果AI工具直接去解决非形式化描述的问题，它更可能通过技术性漏洞“成功”。 例如，证明一个包含非预期边缘情况的命题（比如某个关键参数本应非零，但形式化表述中允许其为零），而非真正解决原问题。 目前这个数据库才刚刚起步，只收录了文献中极小一部分的猜想，团队正公开征集更多贡献，所有想为这个项目贡献一份力量的人，可以通过下面几种方式参与其中： 添加新的问题形式化：猜想可以来自各种地方，包括数学教科书、研究论文、专用问题列表等 提出你希望形式化的问题：建议包含参考文献链接和精确的非正式表述 改进问题的引用和标记：为现有命题添加参考文献或补充AMS学科分类标签 修复错误的形式化：鼓励通过提交PR修复不准确的表述，或提交issue反馈潜在缺陷 感兴趣的朋友可以点开资源库链接：-deepmind/formal-conjectures
