arXiv cs.AI· Moritz Firsching, Paul Lezeau, Salvatore Mercuri, Mikl\'os Z. Horv\'ath, Ya\"el Dillies, Calle S\"onne, Eric Wieser, Fred Zhang, Thomas Hubert, Blaise Ag\"uera y Arcas, Pushmeet Kohli·· 3 小时前AI 评分50
Formal Conjectures：面向数学验证式发现的开源演进型基准
Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics
AI 导读
Formal Conjectures 是一个用 Lean 4 形式化的数学基准，目前包含 7559 条数学问题陈述，其中 1642 条无已知解的开放研究猜想、2923 道已解决问题和 2994 条辅助命题，已收录于 NeurIPS 2026 Datasets and Benchmarks Track。
正文 · 原文
Authors:Moritz Firsching, Paul Lezeau, Salvatore Mercuri, Miklós Z. Horváth, Yaël Dillies, Calle Sönne, Eric Wieser, Fred Zhang, Thomas Hubert, Blaise Agüera y Arcas, Pushmeet Kohli
Abstract: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 (this https URL), 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.
| Comments: | 24 pages, 4 figures, 5 tables, Accepted at NeurIPS 2026 Datasets and Benchmarks Track |
| Subjects: | Artificial Intelligence (cs.AI) |
| MSC classes: | 68V15, 03B35, 68T05 |
| ACM classes: | I.2.3; F.4.3; I.2.6 |
| Cite as: | arXiv:2605.13171 [cs.AI] |
| (or arXiv:2605.13171v2 [cs.AI] for this version) | |
| https://doi.org/10.48550/arXiv.2605.13171 arXiv-issued DOI via DataCite |
Submission history
From: Moritz Firsching [view email]
[v1]
Wed, 13 May 2026 08:33:15 UTC (5,817 KB)
[v2]
Wed, 11 Nov 2026 13:54:44 UTC (5,824 KB)
来源：arXiv cs.AI · arxiv.org