← 研踪 PaperTrailarXiv:2605.13171 · v2
Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics
首次提交 2026-05-13 16:33
版本更新 2026-11-11 21:54
雷达观测 2026-11-13 14:16
摘要
As automated reasoning systems advance rapidly, there is a growing need for research-level formal mathematical problems to accurately evaluate their capabilities. To address this, we present Formal Conjectures (https://github.com/google-deepmind/formal-conjectures), an evolving benchmark of currently 7559 mathematical problem statements formalized in Lean 4. Sourced from areas of active mathematical research, the dataset features 1642 open research conjectures without known solutions for mathematical proof discovery, 2923 solved problems for proof auto-formalization, and 2994 supporting statements. Notably, the repository provides a structured interface connecting mathematicians who formalize and clarify problems with the AI systems and humans attempting to solve them. Demonstrating its immediate utility, the benchmark has already been leveraged for new mathematical discoveries, including the resolution of open research conjectures, and for the formal confirmation of major newly announced results. We describe our approach to ensuring the correctness of these formalizations in a collaborative open-source project where contributions stem from an active community. In this framework, AI-generated proofs and disproofs serve as a valuable auditing mechanism to iteratively improve the fidelity of the benchmark. Finally, we provide a standardized evaluation setup and report baseline results on frozen evaluation subsets, demonstrating a climbable signal that measures the current frontier of automated reasoning on research-level mathematics.
作者备注：24 pages, 4 figures, 5 tables, Accepted at NeurIPS 2026 Datasets and Benchmarks Track
观测到的版本
相邻记录可能跳过中间版本；首次发现 v2 及以上也会标为版本更新。
v2 · 2026-11-11 21:54 · 最新观测版本
Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics
As automated reasoning systems advance rapidly, there is a growing need for research-level formal mathematical problems to accurately evaluate their capabilities. To address this, we present Formal Conjectures (https://github.com/google-deepmind/formal-conjectures), an evolving benchmark of currently 7559 mathematical problem statements formalized in Lean 4. Sourced from areas of active mathematical research, the dataset features 1642 open research conjectures without known solutions for mathematical proof discovery, 2923 solved problems for proof auto-formalization, and 2994 supporting statements. Notably, the repository provides a structured interface connecting mathematicians who formalize and clarify problems with the AI systems and humans attempting to solve them. Demonstrating its immediate utility, the benchmark has already been leveraged for new mathematical discoveries, including the resolution of open research conjectures, and for the formal confirmation of major newly announced results. We describe our approach to ensuring the correctness of these formalizations in a collaborative open-source project where contributions stem from an active community. In this framework, AI-generated proofs and disproofs serve as a valuable auditing mechanism to iteratively improve the fidelity of the benchmark. Finally, we provide a standardized evaluation setup and report baseline results on frozen evaluation subsets, demonstrating a climbable signal that measures the current frontier of automated reasoning on research-level mathematics.
查看此版本解读 →查看此版本原文 ↗