Formal Conjectures 形式数学基准
blaiseaguera · x · 2026-07-14
作者宣布与 **Google DeepMind** 合作推出 **Formal Conjectures**：一个用于评估 AI 形式化数学能力的、持续演进的 **Lean 4 benchmark**。 ### 核心特点 - 以 **1,029 个开放猜想** 作为“零污染”推理测试集，尽量避免训练集泄漏带来的干扰。 - 另外提供 **836 个已解决问题**，用于自动形式化（auto-formalization）任务。 - 设计目标要求 **kernel-level correctness**，也就是最终证明必须在 Lean 内核层面严格成立。 作者补充说，这项工作已经开始促进新的发现，并帮助形式化数学社区与自动化求解器之间建立更紧密的联系。帖文还提到开源代码已经放出。