形式化数学猜想库 - DeepMind最新开源形式化数学猜想库，收录经典数学猜想的形式化表述，如解析数论中的四个朗道问题 [1] - 资源库提供代码函数，方便用户将自然语言数学猜想转化为计算机可验证的形式化版本 [2] - 陶哲轩转发并强调形式化表述是利用自动化工具解决开放性问题的关键第一步 [3] - 猜想库开放共建，鼓励数学家添加新猜想 [4] 猜想库的用途与结构 - 填补开放式猜想形式化资源的空白，可作为自动定理证明或形式化工具的测试基准 [6][7] - 收录使用Lean形式化表述的数学猜想，来源多样，类型丰富 [9] - 题目类别统计：数论（262个）、组合数学（99个）、特殊函数（28个）、域论与多项式（17个）等 [11] - 相当于为计算机提供可扩充的“习题集”，支持ATP直接进行证明搜索或作为训练数据让AI学习猜想模式 [11][13] 参与方式与流程 - 用户可通过四种方式参与：添加新问题形式化、提出形式化需求、改进引用标记、修复错误表述 [16][17][18] - 操作流程：GitHub创建问题→Fork仓库→本地构建验证→提交PR→等待审核 [20][21][22][23][24] - 审核机制结合人工与AlphaProof（通用数学自动证明系统）确保准确性 [26] DeepMind与陶哲轩的合作 - 陶哲轩曾称赞DeepMind的FunSearch是利用LLM进行数学发现的有前途范式 [28] - 双方合作开发AlphaEvolve（LLM驱动的进化编码Agent），在数学分析、几何学等领域取得突破 [33][38] - AlphaEvolve在75%案例中复现最优解，20%案例改进已知方案 [39][40] - 解决11维空间接吻数问题，发现593个外球体结构刷新下限 [36][37] 资源链接 - 形式化数学猜想库官网与项目地址 [42]