OpenFrontiers：开放研究问题集与科学再发现基准

# A Collection of Open Research Problemsand a Benchmark for Scientific Rediscovery
Source: [https://arxiv.org/html/2610.37739](https://arxiv.org/html/2610.37739)
## OpenFrontiers: A Collection of Open Research Problems and a Benchmark for Scientific Rediscovery

###### Abstract

Large language models \(LLMs\) have shown increasing promise in research\-level problem solving, yet a comprehensive collection of such problems is still missing, and evaluating them on research\-level problems remains challenging\. We introduceOpenFrontiers, a cross\-disciplinary resource that combines a structured corpus of open research problems with a retrospective benchmark of recently resolved problems in mathematics\. The corpus records problem statements, context, progress, and other information for 12,151 problems\. The benchmark contains 200 problems, 110 resolved in 2026 and 90 still open, each with a Lean 4 statement checked by automated probes and two independent reviews; a subset HQ\-50 further filters based on quality score, etc\. Our evaluation protocol grades formal proofs with two independent checkers in an isolated sandbox under closed\-book, frozen\-retrieval, and live\-web conditions\. Evaluating seven LLM agents on the HQ\-50 subset under a standardized budget, we find that closed\-book rediscovery is rare, at most 7 of 40 resolved problems, whereas live\-web success mostly reflects retrieval of published solutions\. By linking a broad research\-problem corpus to a formally graded evaluation subset with documented solutions, OpenFrontiers provides a foundation for measuring research\-level rediscovery and studying progress toward solving currently open scientific problems\. The dataset and benchmark could be found in[https://huggingface\.co/collections/FlippyDora/openfrontiers](https://huggingface.co/collections/FlippyDora/openfrontiers)\.

## 1Introduction

Large language models \(LLMs\) have achieved perfect performance in extremely hard theoretical science tests, like IMO, and are now increasingly directed at problems that nobody has solved yet: systems built around them have produced formally checked proofs of olympiad problems\([Hubert et al\., 2026](https://arxiv.org/html/2610.37739#bib.bib22)\)and new constructions or improved bounds for research questions\([Romera\-Paredes et al\., 2024](https://arxiv.org/html/2610.37739#bib.bib23);[Novikov et al\., 2025](https://arxiv.org/html/2610.37739#bib.bib24);[Georgiev et al\., 2025b](https://arxiv.org/html/2610.37739#bib.bib25)\), and they appear in the solution materials of many problems examined below\. Measuring the ability to resolve open problems is harder than measuring exam performance: expert\-written suites such as FrontierMath\([Glazer et al\., 2024](https://arxiv.org/html/2610.37739#bib.bib1)\), Humanity’s Last Exam\([Phan et al\., 2025](https://arxiv.org/html/2610.37739#bib.bib2)\)and GPQA\([Rein et al\., 2023](https://arxiv.org/html/2610.37739#bib.bib3)\)grade against a reference answer their authors already knew; competition sets saturate quickly and appear in training data\([Balunović et al\., 2025](https://arxiv.org/html/2610.37739#bib.bib9);[Sainz et al\., 2023](https://arxiv.org/html/2610.37739#bib.bib46);[Roberts et al\., 2024](https://arxiv.org/html/2610.37739#bib.bib48)\); and proof\-level grading shows that final\-answer accuracy overstates what a model has established\([Petrov et al\., 2025](https://arxiv.org/html/2610.37739#bib.bib10)\)\. A research problem, by contrast, is defined by the absence of a reference answer\.

Measuring research\-level ability therefore needs two things: a map of what is open, and tasks that can be graded at all\. Open problems are scattered across problem lists, workshop reports, survey sections, prize pages, blogs and many other platforms\([Bloom, 2023](https://arxiv.org/html/2610.37739#bib.bib32);[The Formal Conjectures Authors, 2025](https://arxiv.org/html/2610.37739#bib.bib31);[TheoremDB, 2026](https://arxiv.org/html/2610.37739#bib.bib35);[Ju et al\., 2026](https://arxiv.org/html/2610.37739#bib.bib36)\)with differing conventions for wording, status and licensing, and assembling them without rewording statements or overstating status is itself a curation problem\. A formerly open problem can be graded only against a solution that appeared after the evaluated model was frozen, so tasks must be time\-anchored\([White et al\., 2025](https://arxiv.org/html/2610.37739#bib.bib18)\): the model receives the formulation that was public before resolution, and the located solution is evaluator\-only\.

Figure 1:Overview of OpenFrontiers: registered sources are fetched and normalized into a provenance\-first corpus \(Section[3](https://arxiv.org/html/2610.37739#S3)\); curation yields the 200 Lean\-stated items of OpenFrontiers\-Bench \(Section[4](https://arxiv.org/html/2610.37739#S4)\); models are evaluated under three access conditions and graded by two Lean checkers \(Section[5](https://arxiv.org/html/2610.37739#S5)\)\.We introduce OpenFrontiers, which has three coupled parts \(Figure[1](https://arxiv.org/html/2610.37739#S1.F1)\)\. The OpenFrontiers corpus \(Section[3](https://arxiv.org/html/2610.37739#S3)\) is a large corpus of 12,151 problem records from 62 source collections across 10 top\-level fields and 32 sub\-fields, with MSC 2020 codes on 65\.9% of records and Lean 4 statements attached to 1,946\. Uncertain status is labeled*unassessed*\(46\.0% of records\) rather than promoted to*open*\(50\.7%\)\.

Based on the open problems collection, we build a benchmark including problems that are still open and those resolved recently\. OpenFrontiers\-Bench holds 200 research\-level mathematics problems, each with a Lean 4 statement that compiles in a pinned environment and has passed automated verifications and two independent reviews\. Rediscovery\-110 has 110 documented research questions that remained open into 2026 and now have a located solution, 85 with an independently checked Lean proof or exact certificate \(an explicit finite object, such as a counterexample, recomputed with exact arithmetic\), and Open\-90 has 90 problems still open\. Constructing Rediscovery\-110 yielded an observation: for 55 of the 110 the solution materials credit an AI system with the key mathematics, and most checked solutions have a public Lean proof\. A model whose lineage produced a solution cannot be said to rediscover it, so post\-cutoff dating alone does not control contamination, and the protocol \(Section[5](https://arxiv.org/html/2610.37739#S5)\) excludes such items per model and makes closed\-book the main condition\.

We evaluate seven LLM agents on HQ\-50, a high\-quality 50\-item subset of OpenFrontiers\-Bench, under closed\-book, frozen\-retrieval and live\-web conditions, grading only Lean proofs accepted by two independent checkers\. Closed\-book, the agents solve 0–7 of 40 solved items, mostly three human\-solved items with short constructions; with live web they solve up to 27, nearly always after fetching the published solution, and no open problem was solved without one\. Frontier agents also tend to give up easily without reaching the time budget if the problem is too hard\. To summarize, our contributions are:

- •Open problems corpus\.A cross\-disciplinary, diverse 12,151 open\-problem records with verbatim statements, resolve status, Lean 4 attachments, source, and other information etc\.
- •Benchmark\.OpenFrontiers\-Bench: 200 items with checked Lean 4 statements, evidence tiers and per\-item date and AI\-disclosure audits, and the HQ\-50 subset\.
- •Evaluation protocol\.We evaluate the models’ open problem solving ability under three access conditions in an isolated sandbox, grading by two independent Lean checkers, and per\-model lineage and cutoff exclusion\.
- •Experiment results\.We conduct different evaluations on our benchmark with seven LLM agents, showing that closed\-book rediscovery is rare and that live\-web success reflects retrieval of published solutions\.

## 2Related Work

#### Benchmarks for mathematical and scientific reasoning\.

LLM reasoning has been tracked with competition datasets such as GSM8K\([Cobbe et al\., 2021](https://arxiv.org/html/2610.37739#bib.bib5)\), MATH\([Hendrycks et al\., 2021](https://arxiv.org/html/2610.37739#bib.bib4)\), OlympiadBench\([He et al\., 2024](https://arxiv.org/html/2610.37739#bib.bib12)\)and Omni\-MATH\([Gao et al\., 2025](https://arxiv.org/html/2610.37739#bib.bib13)\), and with expert\-written science questions in GPQA\([Rein et al\., 2023](https://arxiv.org/html/2610.37739#bib.bib3)\), TPBench\([Chung et al\., 2025](https://arxiv.org/html/2610.37739#bib.bib14)\), SciCode\([Tian et al\., 2024](https://arxiv.org/html/2610.37739#bib.bib15)\)and LAB\-Bench\([Laurent et al\., 2024](https://arxiv.org/html/2610.37739#bib.bib16)\)\. Against contamination of static benchmarks\([Sainz et al\., 2023](https://arxiv.org/html/2610.37739#bib.bib46);[Deng et al\., 2024](https://arxiv.org/html/2610.37739#bib.bib47)\)and performance drops on post\-cutoff material\([Roberts et al\., 2024](https://arxiv.org/html/2610.37739#bib.bib48)\), FrontierMath\([Glazer et al\., 2024](https://arxiv.org/html/2610.37739#bib.bib1)\)and Humanity’s Last Exam\([Phan et al\., 2025](https://arxiv.org/html/2610.37739#bib.bib2)\)hold out expert questions, while MathArena\([Balunović et al\., 2025](https://arxiv.org/html/2610.37739#bib.bib9)\), RealMath\([Zhang et al\., 2025](https://arxiv.org/html/2610.37739#bib.bib17)\)and LiveBench\([White et al\., 2025](https://arxiv.org/html/2610.37739#bib.bib18)\)refresh items from new competitions and papers\. Most grade a final answer or a unit\-tested program on items written for the benchmark; FrontierMath: Open Problems\([Epoch AI, 2026](https://arxiv.org/html/2610.37739#bib.bib50)\)and OEIS Open\([Adamczewski, 2026](https://arxiv.org/html/2610.37739#bib.bib53)\)pose actually open questions but accept only machine\-checked answers\. OpenFrontiers also uses questions that were actually open, dates them by located solution evidence and admits expert\-reviewed proofs\.

#### Proof\-level and formal evaluation\.

Graded as full proofs, recent olympiad problems yield few complete and rigorous arguments even from models that lead final\-answer competitions\([Petrov et al\., 2025](https://arxiv.org/html/2610.37739#bib.bib10)\), motivating proof\-graded sets such as IMO\-ProofBench\([Luong et al\., 2025](https://arxiv.org/html/2610.37739#bib.bib11)\)\. Formal benchmarks such as miniF2F\([Zheng et al\., 2022](https://arxiv.org/html/2610.37739#bib.bib6)\), ProofNet\([Azerbayev et al\., 2023](https://arxiv.org/html/2610.37739#bib.bib8)\)and PutnamBench\([Tsoukalas et al\., 2024](https://arxiv.org/html/2610.37739#bib.bib7)\)replace the grader with a proof assistant, most often Lean 4\([de Moura and Ullrich, 2021](https://arxiv.org/html/2610.37739#bib.bib19)\)with mathlib\([The mathlib Community, 2020](https://arxiv.org/html/2610.37739#bib.bib20)\), and dedicated provers followed: AlphaGeometry\([Trinh et al\., 2024](https://arxiv.org/html/2610.37739#bib.bib21)\), AlphaProof\([Hubert et al\., 2026](https://arxiv.org/html/2610.37739#bib.bib22)\), DeepSeek\-Prover\-V2\([Ren et al\., 2025](https://arxiv.org/html/2610.37739#bib.bib26)\), Kimina\-Prover\([Wang et al\., 2025](https://arxiv.org/html/2610.37739#bib.bib27)\), Goedel\-Prover\([Lin et al\., 2025](https://arxiv.org/html/2610.37739#bib.bib28)\), Seed\-Prover\([Chen et al\., 2025](https://arxiv.org/html/2610.37739#bib.bib29)\)and Aristotle\([Achim et al\., 2025](https://arxiv.org/html/2610.37739#bib.bib30)\); agentic systems such as Danus\([Liu et al\., 2026](https://arxiv.org/html/2610.37739#bib.bib49)\)go further and coordinate prover agents with an independent verifier around a memory of verified facts to attack research\-level problems directly\. Since only 16\.0% of corpus records carry a Lean 4 statement, OpenFrontiers\-Bench writes and reviews a pinned statement for each of its items, and our protocol grades solutions with two independent Lean checkers \(Section[5\.2](https://arxiv.org/html/2610.37739#S5.SS2)\)\.

#### Open\-problem collections\.

Curated problem lists \(the Kourovka Notebook\([Khukhro and Mazurov, 2026](https://arxiv.org/html/2610.37739#bib.bib33)\), Kirby’s list\([Kirby, 1997](https://arxiv.org/html/2610.37739#bib.bib41)\), Smale’s problems\([Smale, 1998](https://arxiv.org/html/2610.37739#bib.bib40)\), the Clay Millennium Prize Problems\([Clay Mathematics Institute, 2000](https://arxiv.org/html/2610.37739#bib.bib42)\), The Open Problems Project\([Demaine et al\., 2001](https://arxiv.org/html/2610.37739#bib.bib39)\), Ben Green’s list\([Green, 2025](https://arxiv.org/html/2610.37739#bib.bib34)\), the AIM workshop lists\([American Institute of Mathematics, 2026](https://arxiv.org/html/2610.37739#bib.bib38)\)\), community venues \(the Erdős Problems site\([Bloom, 2023](https://arxiv.org/html/2610.37739#bib.bib32)\), the Open Problem Garden\([Open Problem Garden contributors, 2026](https://arxiv.org/html/2610.37739#bib.bib43)\), Wikipedia’s subject lists\([Wikipedia contributors, 2026](https://arxiv.org/html/2610.37739#bib.bib44)\), the COLT open\-problem track\([Conference on Learning Theory, 2026](https://arxiv.org/html/2610.37739#bib.bib45)\)\) and structured databases \(TheoremDB\([TheoremDB, 2026](https://arxiv.org/html/2610.37739#bib.bib35)\), ICM Conjectures\([Ju et al\., 2026](https://arxiv.org/html/2610.37739#bib.bib36)\), Open Quantum Problems\([Bruneton, 2026](https://arxiv.org/html/2610.37739#bib.bib37)\), Formal Conjectures\([The Formal Conjectures Authors, 2025](https://arxiv.org/html/2610.37739#bib.bib31)\), the Optimization Constants\([Davis et al\., 2026](https://arxiv.org/html/2610.37739#bib.bib51)\)and AlphaEvolve\([Georgiev et al\., 2025a](https://arxiv.org/html/2610.37739#bib.bib52)\)repositories\) are each bound to one community, one format and one notion of “open”, and their statuses drift as problems are solved\. OpenFrontiers registers 71 such sources under one schema with verbatim statements, per\-record provenance and license text, and a status policy that labels uncertain itemsunassessedrather than open \(Section[3](https://arxiv.org/html/2610.37739#S3)\); Erdős Problems and Formal Conjectures also feed OpenFrontiers\-Bench \(Section[4](https://arxiv.org/html/2610.37739#S4)\)\.

## 3The OpenFrontiers Corpus

Open problems may be gradually solved over time; therefore, we cut off the status filtering to a particular date\. The corpus snapshot used here holds 12,151 problem records from 62 source collections in 10 top\-level fields, plus 4,751 catalogue items \(source indices and pointers without statements\)\. We did not perform deduplication based on statements in order to preserve the original problems\.

### 3\.1Sources and acquisition

#### Source registry\.

To increase the diversity of the open\-problems collection, we search as many sources as possible\. The registry lists 71 sources \(problem lists, workshop lists, preprints and surveys with open\-question sections, prize lists, blogs and Wikipedia subject lists\), of which 62 contribute problem records; the rest, such as the Kourovka Notebook\([Khukhro and Mazurov, 2026](https://arxiv.org/html/2610.37739#bib.bib33)\)and Ben Green’s 100 problems\([Green, 2025](https://arxiv.org/html/2610.37739#bib.bib34)\), are catalogue\-only, with bibliographic pointers and indices collected but no statements\. Seven collections have at least 100 records: TheoremDB \(3,909\)\([TheoremDB, 2026](https://arxiv.org/html/2610.37739#bib.bib35)\), the AIM Problem Lists \(3,470\)\([American Institute of Mathematics, 2026](https://arxiv.org/html/2610.37739#bib.bib38)\), ICM Conjectures \(2,898\)\([Ju et al\., 2026](https://arxiv.org/html/2610.37739#bib.bib36)\), Erdős Problems \(634\)\([Bloom, 2023](https://arxiv.org/html/2610.37739#bib.bib32)\), Formal Conjectures \(459\)\([The Formal Conjectures Authors, 2025](https://arxiv.org/html/2610.37739#bib.bib31)\), Optimization Constants \(115\) and Open Quantum Problems \(114\)\([Bruneton, 2026](https://arxiv.org/html/2610.37739#bib.bib37)\); eight more, including The Open Problems Project\([Demaine et al\., 2001](https://arxiv.org/html/2610.37739#bib.bib39)\), have between 22 and 59, and the remaining 47 \(including 13 Wikipedia lists\([Wikipedia contributors, 2026](https://arxiv.org/html/2610.37739#bib.bib44)\)\) have at most 20 records each; all 62 are listed with license notes in Table[B](https://arxiv.org/html/2610.37739#A2)\(Appendix[B](https://arxiv.org/html/2610.37739#A2)\)\. Theverified\-coltcollection \(30 records: 14 open, 16 partially solved\) comes from a two\-reviewer fidelity audit of the 118 COLT open\-problem papers of 2003–2026\([Conference on Learning Theory, 2026](https://arxiv.org/html/2610.37739#bib.bib45)\)\.

#### Acquisition and formulation\.

To collect the data from various websites, we developed several tools as deterministic fetchers and record checksums of retrieved files\. Besides, we use a unified format to store the problems\. One schema covers all problem kinds; a problem item stores the verbatim statement \(Markdown with LaTeX\), field, MSC 2020 codes with their mapping basis, status, source and license wording, references, provenance \(import and status\-as\-of dates\), quality flags, Lean 4 attachments and partial\-progress context \(94\.9% of records; Appendix[F](https://arxiv.org/html/2610.37739#A6)\)\.

#### Status policy\.

Status is one ofopen,unassessed,partially\-solved,solved,disputedorwithdrawn\. Historical workshop lists \(AIMPL\) and backlog items default tounassessedbecause their sources assert no current status; the corpus does not claim that they are still open\. Every label records the source’s status claim as of the stored status\-as\-of date, not a local check: anopenrecord has not been verified to be open, and source\-side “solved” or “verified” labels are kept as*claims*insource\_status\_json, keeping the original statement\.

#### Field classification and Lean 4 statement\.

To facilitate the fine\-grained evaluation of models on the open problems corpus, we classify the problems according to the MSC 2020 code\. Each MSC 2020 code assignment records its basis and an evidence string:source\-map\(2,665 assignments, from the source’s own subject category\),community\-map\(5,241, from the record’s field label\) oreditorial\(297, curator\-assigned\)\. Lean 4 statements\([de Moura and Ullrich, 2021](https://arxiv.org/html/2610.37739#bib.bib19);[The mathlib Community, 2020](https://arxiv.org/html/2610.37739#bib.bib20)\)are attached from TheoremDB, the Formal Conjectures repository \(pinned commitb82b08f, Lean 4\.33\.1\) and the Erdős\-problem files\. They are display\-only: no Lean is executed at export time, lexicalsorry/admit/axiomflags are recorded instead, and formal checking happens only in the platform sandbox \(Appendix[D](https://arxiv.org/html/2610.37739#A4)\) and the benchmark grader \(Section[5\.2](https://arxiv.org/html/2610.37739#S5.SS2)\)\.

### 3\.2Corpus statistics

Table 1:Key figures of the corpus \(problem partition unless stated; snapshot 2026\-10\-10; source records, not deduplicated conjectures\)\.withdrawndisputedsolvedpartially\-solvedunassessedopen12413545,5916,162\(a\)Status of the 12,151 records53 Diff\. geometry03 Logic37 Dynamical sys\.20 Group theory35 PDE68 Computer sci\.60 Probability14 Algebraic geom\.05 Combinatorics11 Number theory1661772422612873105026142,0072,862\(b\)Top\-10 MSC 2020 classes1950s1960s1970s1980s1990s2000s2010s2020s9260260245428466869878\(c\)Records by posed decade
Figure 2:Corpus statistics for the 12,151 problem records: \(a\) status; \(b\) top\-10 MSC 2020 top\-level classes by records with at least one code in the class \(8,011 records carry a code\); \(c\) posed decade for the 3,389 records with a known posed year \(91 records before 1950 omitted\)\.#### Coverage\.

Table[1](https://arxiv.org/html/2610.37739#S3.T1)and Figure[2](https://arxiv.org/html/2610.37739#S3.F2)summarize the status of OpenFrontiers\. Mathematics accounts for 11,349 records \(93\.4%\); the 802 others are mostly physics \(339\), computer science \(285\) and machine learning \(70\), with at most 36 records in each remaining field, so mathematics still accounts for the most formalized open problems\. Within mathematics, number theory \(2,867 records\) and geometry and topology \(2,371\) lead the 32 sub\-fields, and the MSC view \(Figure[2](https://arxiv.org/html/2610.37739#S3.F2)b\) is led by 11 Number theory and 05 Combinatorics\.

#### Status\.

Half of the records areopen\(50\.7%\) and nearly as many areunassessed\(46\.0%\); the latter reflects the status policy rather than the problems, since AIMPL \(3,465\), TheoremDB \(1,243, largely backlog candidates\) and Formal Conjectures \(459\) account for 5,167 of them\. Theopenrecords come mainly from TheoremDB \(2,644\), ICM Conjectures \(2,594\) and Erdős Problems \(633\); 304 of the 354partially\-solvedrecords come from ICM Conjectures, and only 41 aresolved, since resolved material lives mostly in the catalogue partition \(1,042 of its 4,751 items are labeled solved by their source\)\.

#### Formal material, text and time\.

Of the 1,946 records with a Lean 4 statement, almost all from TheoremDB \(1,109\), Formal Conjectures \(459\) and Erdős Problems \(374\), 1,562 are flaggedformalization\-contains\-placeholder\(a lexicalsorryoradmit\), and no record carries a canonical accepted proof or a locally verified Lean proof \(Appendix[D](https://arxiv.org/html/2610.37739#A4)\)\. Statements are short and most are summaries or excerpts: only 1,507 records carry the full source text\. References are nearly universal \(1\.79 per record\)\. Among the 3,389 records with a known posed year, the count per decade \(Figure[2](https://arxiv.org/html/2610.37739#S3.F2)c\) rises from 260 in the 1970s to 869 in the 2010s, with 878 already in the 2020s\.

## 4OpenFrontiers\-Bench: A Retrospective Rediscovery Benchmark

OpenFrontiers\-Bench is the evaluation subset of OpenFrontiers: 200 research\-level mathematics problems, each with a checked Lean 4 statement\. Rediscovery\-110 holds 110 publicly posed research questions that remained open into 2026 and now have a located solution \(ID prefixes R, E and N mark three curation rounds\); Open\-90 holds 90 problems still open at the status of check\. HQ\-50, a high\-quality 50\-item subset selected for reference reliability and diversity \(Section[4\.3](https://arxiv.org/html/2610.37739#S4.SS3)\), is evaluated in Section[5](https://arxiv.org/html/2610.37739#S5)\. All 200 items could be found in Appendix[A](https://arxiv.org/html/2610.37739#A1)\.

### 4\.1Construction

#### Candidates\.

Solved candidates came from status changes between successive versions of the corpus’s source lists \(e\.g\., problems newly marked solved in a later Kourovka edition, Erdős Problems threads, Formal Conjectures\([The Formal Conjectures Authors, 2025](https://arxiv.org/html/2610.37739#bib.bib31)\)\), from 2026 arXiv preprints and from public releases of AI\-produced solutions; open candidates came from corpus records with an upstream Lean statement\. Nine search sweeps gave 291 unique solved leads \(257 verified, 230 eligible after a first pass\), and 1,061 Formal Conjectures declarations were screened for the open track \(152 verified, 136 kept\)\. A second reviewer then tried to overturn each new item and rejected 5 \(Appendix[G](https://arxiv.org/html/2610.37739#A7)\)\. Re\-reviewing an earlier 90\-item version removed two solved items \(an answer already in the literature; a refuted solution claim\) and moved four open items resolved in 2026, among them the irrationality ofζ⁡\(5\)\\zeta\(5\), into Rediscovery\-110\.

#### Admission and evidence tiers\.

An item enters Rediscovery\-110 only if it was demonstrably a public research question before its resolution, the located solution settles it with the same quantifiers and scope as posed, no earlier solution was located, and it is not a restatement of an old theorem, a withdrawn paper or an announcement without proof; same\-paper and same\-release items share a split group \(Appendix[C](https://arxiv.org/html/2610.37739#A3)\)\.Tier A\(85 items\): an exact finite certificate was independently recomputed, or a complete Lean proof was compiled locally \(mostly AI\-assisted formalizations\)\.Tier B\(21\): a complete solution corroborated by the source list, a publication or an independent proof, but not re\-verified by us\.Tier C\(4\): a solution claim pending verification\. All located solution\-evidence dates run after 2026\-01\-05\.

#### Lean statements\.

Each item states its target as one theoremmainin a pinned environment \(Lean 4\.33\.1, Mathlib0df444a, Formal Conjectures89294ea;[de Moura and Ullrich, 2021](https://arxiv.org/html/2610.37739#bib.bib19);[The mathlib Community, 2020](https://arxiv.org/html/2610.37739#bib.bib20)\); a yes/no question is writtenanswer\(sorry\)↔\\leftrightarrowP, so a solution must fill in the answer*and*provemain\. 93 statements were taken verbatim from Formal Conjectures, 47 adapted \(e\.g\., an upstream constant stronger than the posed problem\) and 60 newly written; upstream problem files stay out of the build, since at least 35 of them record a solved item’s answer\. A checker requires every file to compile withautoImplicitoff, without axioms ornative\_decide, and with standard axioms only; the statement with the reference answer filled in compiles for all 110 solved items, leakage patterns \(answers, upstream identifiers, live status links\) are absent, and automation \(decide,simp,omega,aesop\) proves or refutes none of the 200 \(Appendix[D](https://arxiv.org/html/2610.37739#A4)\)\.

#### Lean 4 statements review\.

Two independent reviewers checked each statement, one for fidelity to the original source and one attacking its Lean semantics, with up to two repair rounds: 139 items ended ok\+ok, 38 minor\+ok and 23 minor\+minor, with no must\-fix issue\. A further pass rewrote solved\-item comments that hinted at the answer \(47 files\), keeping the comment\-stripped code unchanged\. These reviews were run by AI agents\.

More curation criteria such as importance scores could be found in Appendix[C](https://arxiv.org/html/2610.37739#A3)\.

Table 2:Composition of OpenFrontiers\-Bench\. Rediscovery\-110 columns split by the located solution\-evidence month of 2026\. AI classes classify disclosures in the solution materials; “none disclosed” does not imply that no AI was used\.JanFebMarAprMayJunJulAugSep00101020203030404036241656105262026\-06\-30located solution\-evidence month \(2026\)itemsAI producedAI assistancenone disclosedFigure 3:Located solution\-evidence month of the 110 Rediscovery\-110 items, by disclosed AI involvement \(monthly totals above the bars\)\.

### 4\.2Rediscovery\-110 and Open\-90

#### Rediscovery\-110\.

Rediscovery\-110 spans nine areas, led by group theory and number theory \(19 each\), graph theory \(14\), analysis and PDE \(13\) and geometry and topology \(12\), and includes long\-standing conjectures such as Beck–Fiala, Sendov’s conjecture and the cycle double cover conjecture \(Table[2](https://arxiv.org/html/2610.37739#S4.T2)\)\. 76 items have located solution evidence after 2026\-06\-30, so a model frozen before July can meet them unseen\. Tier A items mostly rest on a full Lean proof of the answered statement \(75 of 85\); the other 10 rest on an exact certificate\.

#### AI involvement\.

For 55 of the 110 items the solution materials credit an AI system with the key mathematics \(OpenAI models 46, Anthropic 5, Google 4, Harmonic 3; several items name more than one\), concentrated after June \(41 of 76; Figure[3](https://arxiv.org/html/2610.37739#S4.F3)\); 36 disclose assistance with a human\-attributed solution, and 19 disclose none\. A model whose lineage produced a solution has in effect seen it, and most Tier A items have a public Lean proof, so a post\-cutoff date is necessary but not sufficient: the protocol excludes such items per model and makes closed\-book the main condition \(Section[5\.1](https://arxiv.org/html/2610.37739#S5.SS1)\)\.

#### Open\-90\.

Open\-90 keeps 26 problems of the earlier open split and adds 64; number theory \(25\) and graph theory \(20\) lead, and statements come verbatim \(69\) or adapted \(21\) from Formal Conjectures\. For 38 items one direction is settled by a single finite object \(a counterexample or construction\), so search plus reasoning could succeed\. We recently checked the status to keep it relatively reliable\. A kernel\-accepted solution would be new mathematics, but a statement error is the likelier explanation, so any acceptance triggers review before a claim \(Section[5\.2](https://arxiv.org/html/2610.37739#S5.SS2)\)\.

### 4\.3HQ\-50

HQ\-50 \(40 solved and 10 open items\) is chosen by a reproducible script in three layers\. Hard filters keep statements with high formalization confidence and a clean review, solved items of unconditional Tier A \(excluding B, C and four conditional A items\) with importance≥4\\geq 4\(human\-solved post\-cutoff exceptions at 3\), and open items with importance≥4\\geq 4, clarity 5, an unrepaired statement and an answer that is not easy to guess; 55 solved and 48 open items qualify\. A score then ranks them \(review outcome, importance, proof type, recency\), and greedy selection enforces caps: one item per paper or problem family, two per public release, at most 16 Erdős and 6 Kourovka items and 8 per area among solved items, and at most 21 items whose key mathematics came from OpenAI models\. The 40 solved items have 34 Lean\-proof and 6 certificate references, 32 post\-cutoff dates, and 21 OpenAI\-, 2 Anthropic\-, 2 Google\-, and 2 other AI\-produced solutions \(13 human\); 8 of the 10 open items have a finite\-certificate direction\. We rechecked all 50 statements to confirm their open status during the LLM agent evaluation\.

## 5Evaluation Protocol and Results

A: closed\-bookB: frozen retrievalC: live webModellineage, cutoffallcleanallcleanallclean*Native protocol \(the agent ends the session\)*Claude Sonnet 5\.5Anthropic, 2026\-0600/3011/3063/30GPT\-6\.1\-solOpenAI, 2026\-0622/1522/15156/15GPT\-6\-lunaOpenAI, 2026\-0600/1500/1543/15Kimi\-K3–, 2026\-0622/3322/331512/33GLM\-5\.3–, 2026\-0822/1622/16158/16DeepSeek\-V4\.1\-Flash–, 2026\-0931/531/5130/5Qwen3\.8\-27B–, 2026\-0800/1900/1910/19†*Continuation protocol \(resumed until the budget is spent\)*Claude Sonnet 5\.5Anthropic, 2026\-0643/3033/302418/30GPT\-6\.1\-solOpenAI, 2026\-0674/1553/152712/15GPT\-6\-lunaOpenAI, 2026\-0622/1500/15166/15Kimi\-K3–, 2026\-0633/3322/331513/33GLM\-5\.3–, 2026\-0800/1622/16135/16DeepSeek\-V4\.1\-Flash–, 2026\-0931/531/5152/5Qwen3\.8\-27B–, 2026\-0800/1900/1920/19Table 3:Results on the 40 solved items of HQ\-50 \(pass@1, 3 h per attempt\)\.*all*: items solved, i\.e\. a Lean proof with the reference answer accepted by both checkers, out of 40;*clean*: solved / eligible after removing items whose key mathematics came from the model’s lineage and items with solution evidence on or before the model’s cutoff \(release date where none is published; – means no lineage exclusion\)\. C mostly measures retrieval of known solutions \(Section[5\.4](https://arxiv.org/html/2610.37739#S5.SS4)\)\. Open items are reported separately\.### 5\.1Access conditions and environment

Each attempt runs one problem in a fresh sandbox holding only that problem’s Lean workspace \(with prebuilt Mathlib, so the model can compile and test its own files\) and Python with numpy, sympy and mpmath\. Answers, the evaluator\-only package and the grading workspace are not visible; every command runs without network under an unprivileged user with private namespaces, seccomp and cgroup limits; and the problem file carries an opaque ID with status\-revealing source lines removed\. The three conditions differ only in retrieval, which the harness performs outside the sandbox and logs: \(A\)*closed\-book*, no retrieval, the main condition; \(B\)*frozen retrieval*, search and fetch over arXiv, Wikipedia, OpenAlex and MathOverflow limited to content public before 2026\-01\-06, one week before the earliest solution evidence, with each hit re\-checked against the historical version it displays; \(C\)*live web*, all URLs logged, a leakage reference rather than a rediscovery measure, since 34 of the 40 solved items have public Lean proofs; this mainly reveals the information retrieval ability of models\.

### 5\.2Grading

A submission is a Lean file; natural\-language proofs and certificates may accompany it but are reported separately, and the main metric counts formal solutions only\. Static rules admit only Mathlib imports and rejectsorry, axioms,native\_decide, metaprogramming and syntax extensions; a yes/no answer must be the literalTrueorFalse\. The grader compiles the reference statement with the submitted answer and the submission in separate jails, replays the submission in the kernel, compares the elaborated definitions and the statement ofmainwith the reference, and allows onlypropext,Classical\.choiceandQuot\.sound\. A second, independent checker, leanprover/comparator, compares every constant the statement uses and replays the whole exported environment in the kernel without loading files the submission may have written\. An item is*solved*only if both checkers accept with the reference answer; a proof of the opposite answer or an accepted open item freezes the item for statement review, and a checker disagreement counts as unsolved\. There is no model\-as\-judge\. A grader self\-test \(accept and reject cases, including a compile\-time file write that passes keyword bans\) and comparator’s 16 official regression attacks pass\. The*clean*subset removes, per model, items whose key mathematics came from its lineage and items with solution evidence on or before its cutoff; at a 2026\-06\-30 cutoff it holds 15 items for OpenAI models, 30 for Anthropic and 32 for unrelated models\. We report counts with their denominators, never answer accuracy \(a yes/no guess scores 50%\)\.

### 5\.3Models and harness

We evaluate seven models through vendor agent CLIs that run inside the sandbox behind a gateway, which pins the model and strips server\-side tools in A and B: Claude Code for Claude Sonnet 5\.5, Kimi\-K3, GLM\-5\.3, DeepSeek\-V4\.1\-Flash and Qwen3\.8\-27B \(128k\-token output limit\), and Codex for GPT\-6\.1\-sol and GPT\-6\-luna\. Each attempt has 3 hours of wall\-clock time, 5 CPU cores and 24 GB of memory, with one attempt per item and condition\. Under the*native*protocol the session ends when the agent stops\. Because frontier agents often stop within minutes, the*continuation*protocol resumes the same session, stating the remaining budget, until a submission passes the pre\-submission check or the budget is spent; an attempt ends as stalled after 20 consecutive \(or 30 of 40\) rounds without tool use \(Appendix[E](https://arxiv.org/html/2610.37739#A5)\)\.

### 5\.4Results

#### Closed\-book rediscovery is rare\.

Models solve 0–3 of the 40 items in A under the native protocol and 0–7 under continuation \(Table[3](https://arxiv.org/html/2610.37739#S5.T3)\)\. Continuation helps most the agents that stop earliest: Claude Sonnet 5\.5 rises from 0 to 4, GPT\-6\.1\-sol from 2 to 7 and GPT\-6\-luna from 0 to 2 \(clean 3/30, 4/15 and 2/15\), while the open\-weight models change by at most two items\. Across the 14 runs \(7 models×\\times2 running protocols\), the 53 A and B solves fall on eight items, and the three importance\-3 items of HQ\-50, all solved by humans through short constructions \(R01, R04, R29\), account for 44 of them; of the 21 importance\-5 items only one \(N28, settled by a finite certificate\) was solved, once\. Frozen retrieval did not help systematically: B exceeds A in two runs \(by one and two items\) and trails it in three, consistent with a snapshot that predates every solution\.

#### Live web measures retrieval\.

In C models solve 1–27 items, but 167 of the 181 C solves came from attempts that fetched a located solution source \(preprint, repository or problem page\), often with a public Lean proof to adapt; the C–A gap thus estimates how retrievable the answers are\. For example, Erdős Problem \#152 \(E03\), solved by a DeepMind prover agent with a public Lean proof since 2026\-04\-03, was solved in none of the 28 A and B attempts but in 11 of the 14 C runs, each after fetching the problem page or its forum thread, which links to that proof\. This becomes pure solution\-seeking rather than scientific rediscovery\. However, even in the live web setting, none of the models can solve all 40 already solved problems perfectly, showing that there is still room to improve models’ information search and retrieval ability\.

#### Agents stop early\.

Natively, Claude Sonnet 5\.5 and the GPT models end most attempts within minutes \(median 0\.3–4\.1 of 180 minutes\), whereas the open\-weight models run longer, Qwen3\.8\-27B mostly until the limit\. Under continuation most agents use nearly the full budget, but most Claude Sonnet 5\.5 attempts stall, repeating that no progress is possible\. By Table[3](https://arxiv.org/html/2610.37739#S5.T3), under the continuation evaluation protocol, agents turn out to solve more problems compared to the native one\. Therefore even models are equipped with the intrinsic ability to solve some open problems, it should be explicitly induced by appropriate prompting and harness design\.

## 6Conclusion

We presented OpenFrontiers, a systematic collection of 12,151 research\-level open\-problem records from 62 source collections across 10 fields, and OpenFrontiers\-Bench, 200 mathematics problems with checked Lean 4 statements, graded by two independent Lean checkers under three access conditions\. Upon our evaluation, seven LLM agents rarely rediscover recent solutions under the closed\-book setting, and their live\-web successes mostly retrieve published solutions\. Even with access to the whole Internet, models do not correctly resolve all already solved problems, revealing room for better information search and retrieval ability\. Moreover, although models can solve some open problems within a fixed budget, they tend to give up early before making substantive progress, highlighting the need to develop more advanced harnesses that keep the model thinking deeper and longer rather than failing to explore the open problem thoroughly\.

## References

- Achimet al\.\(2025\)T\. Achim, A\. Best, A\. Bietti, K\. Der, M\. Fédérico, S\. Gukov, D\. Halpern\-Leistner, K\. Henningsgard, Y\. Kudryashov, A\. Meiburg, M\. Michelsen, R\. Patterson, E\. Rodriguez, L\. Scharff, V\. Shanker, V\. Sicca, H\. Sowrirajan, A\. Swope, M\. Tamas, V\. Tenev, J\. Thomm, H\. Williams, and L\. WuAristotle: IMO\-level automated theorem proving\.arXiv preprint arXiv:2510\.01346\.Note:Developed by HarmonicExternal Links:[Link](https://arxiv.org/abs/2510.01346)Cited by:[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px2.p1.1)\.
- Adamczewski \(2026\)T\. AdamczewskiOEIS Open: how many conjectures can language models turn into theorems?\.arXiv preprint arXiv:2608\.11941\.External Links:[Link](https://arxiv.org/abs/2608.11941)Cited by:[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px1.p1.1)\.
- American Institute of Mathematics \(2026\)American Institute of MathematicsAIM problem lists\.Note:[https://aimath\.org/problemlists/](https://aimath.org/problemlists/)Workshop problem lists hosted on AimPL \([http://aimpl\.org](http://aimpl.org/)\)\. Accessed September 2026Cited by:[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px3.p1.1),[§3\.1](https://arxiv.org/html/2610.37739#S3.SS1.SSS0.Px1.p1.1)\.
- Azerbayevet al\.\(2023\)Z\. Azerbayev, B\. Piotrowski, H\. Schoelkopf, E\. W\. Ayers, D\. Radev, and J\. AvigadProofNet: autoformalizing and formally proving undergraduate\-level mathematics\.arXiv preprint arXiv:2302\.12433\.External Links:[Link](https://arxiv.org/abs/2302.12433)Cited by:[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px2.p1.1)\.
- Balunovićet al\.\(2025\)M\. Balunović, J\. Dekoninck, I\. Petrov, N\. Jovanović, and M\. VechevMathArena: evaluating LLMs on uncontaminated math competitions\.InAdvances in Neural Information Processing Systems 38 \(NeurIPS 2025\), Datasets and Benchmarks Track,Note:arXiv:2505\.23281Cited by:[§1](https://arxiv.org/html/2610.37739#S1.p1.1),[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px1.p1.1)\.
- Bloom \(2023\)T\. F\. BloomErdős problems\.Note:[https://www\.erdosproblems\.com/](https://www.erdosproblems.com/)Online database of problems posed by Paul Erdős, with status tracking and discussion forum\. Accessed September 2026Cited by:[§1](https://arxiv.org/html/2610.37739#S1.p2.1),[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px3.p1.1),[§3\.1](https://arxiv.org/html/2610.37739#S3.SS1.SSS0.Px1.p1.1)\.
- Bruneton \(2026\)J\. BrunetonOpen problems in quantum mechanics for AI agents\.Note:[https://openquantumproblems\.com/](https://openquantumproblems.com/)Open Quantum Problems catalogue; literature\-reviewed entries in ten research areas; source repository[https://github\.com/jpbruneton/open\_quantum\_problems](https://github.com/jpbruneton/open_quantum_problems)\. Accessed September 2026Cited by:[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px3.p1.1),[§3\.1](https://arxiv.org/html/2610.37739#S3.SS1.SSS0.Px1.p1.1)\.
- Chenet al\.\(2025\)L\. Chen, J\. Gu, L\. Huang, W\. Huang, Z\. Jiang, A\. Jie, X\. Jin, X\. Jin, C\. Li, K\. Ma, C\. Ren, J\. Shen, W\. Shi, T\. Sun, H\. Sun, J\. Wang, S\. Wang, Z\. Wang, C\. Wei, S\. Wei, Y\. Wu, Y\. Wu, Y\. Xia, H\. Xin, F\. Yang, H\. Ying, H\. Yuan, Z\. Yuan, T\. Zhan, C\. Zhang, Y\. Zhang, G\. Zhang, T\. Zhao, J\. Zhao, Y\. Zhou, and T\. H\. ZhuSeed\-Prover: deep and broad reasoning for automated theorem proving\.arXiv preprint arXiv:2507\.23726\.External Links:[Link](https://arxiv.org/abs/2507.23726)Cited by:[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px2.p1.1)\.
- Chunget al\.\(2025\)D\. J\. H\. Chung, Z\. Gao, Y\. Kvasiuk, T\. Li, M\. Münchmeyer, M\. Rudolph, F\. Sala, and S\. C\. TadepalliTheoretical physics benchmark \(TPBench\)—a dataset and study of AI reasoning capabilities in theoretical physics\.Machine Learning: Science and Technology6\(3\),pp\. 030505\.Note:arXiv:2502\.15815External Links:[Document](https://dx.doi.org/10.1088/2632-2153/adfcb0)Cited by:[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px1.p1.1)\.
- Clay Mathematics Institute \(2000\)Clay Mathematics InstituteThe Millennium Prize Problems\.Note:[https://www\.claymath\.org/millennium\-problems/](https://www.claymath.org/millennium-problems/)Announced 24 May 2000, Collège de France, Paris\. Accessed September 2026Cited by:[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px3.p1.1)\.
- Cobbeet al\.\(2021\)K\. Cobbe, V\. Kosaraju, M\. Bavarian, M\. Chen, H\. Jun, L\. Kaiser, M\. Plappert, J\. Tworek, J\. Hilton, R\. Nakano,et al\.Training verifiers to solve math word problems\.arXiv preprint arXiv:2110\.14168\.Cited by:[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px1.p1.1)\.
- Conference on Learning Theory \(2026\)Conference on Learning TheoryOpen problems track of the Conference on Learning Theory \(COLT\)\.Note:[https://proceedings\.mlr\.press/](https://proceedings.mlr.press/)Open\-problem papers appear in the annual COLT proceedings volumes \(Proceedings of Machine Learning Research\)\. Accessed September 2026Cited by:[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px3.p1.1),[§3\.1](https://arxiv.org/html/2610.37739#S3.SS1.SSS0.Px1.p1.1)\.
- Daviset al\.\(2026\)D\. Davis, P\. Ivanisvili, and T\. TaoOptimization constants in mathematics\.Note:[https://github\.com/teorth/optimizationproblems](https://github.com/teorth/optimizationproblems)Repository at commit 2c1968c \(26 September 2026\); accessed October 2026Cited by:[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px3.p1.1)\.
- de Moura and Ullrich \(2021\)L\. de Moura and S\. UllrichThe Lean 4 theorem prover and programming language\.InAutomated Deduction – CADE 28,A\. Platzer and G\. Sutcliffe \(Eds\.\),Lecture Notes in Computer Science, Vol\.12699,Cham,pp\. 625–635\.External Links:[Document](https://dx.doi.org/10.1007/978-3-030-79876-5%5F37)Cited by:[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px2.p1.1),[§3\.1](https://arxiv.org/html/2610.37739#S3.SS1.SSS0.Px4.p1.1),[§4\.1](https://arxiv.org/html/2610.37739#S4.SS1.SSS0.Px3.p1.1)\.
- Demaineet al\.\(2001\)E\. D\. Demaine, J\. S\. B\. Mitchell, and J\. O’RourkeThe Open Problems Project\.Note:[https://topp\.openproblem\.net/](https://topp.openproblem.net/)Online compilation of open problems in computational geometry, 2001–present; originating from Mitchell and O’Rourke, Computational Geometry Column 42, Internat\. J\. Comput\. Geom\. Appl\. 11\(5\):573–582, 2001\. Accessed September 2026Cited by:[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px3.p1.1),[§3\.1](https://arxiv.org/html/2610.37739#S3.SS1.SSS0.Px1.p1.1)\.
- Denget al\.\(2024\)C\. Deng, Y\. Zhao, X\. Tang, M\. Gerstein, and A\. CohanInvestigating data contamination in modern benchmarks for large language models\.InProceedings of the 2024 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies \(Volume 1: Long Papers\),Mexico City, Mexico,pp\. 8706–8719\.Cited by:[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px1.p1.1)\.
- Epoch AI \(2026\)Epoch AIFrontierMath: open problems\.Note:[https://epoch\.ai/frontiermath/open\-problems](https://epoch.ai/frontiermath/open-problems)CC BY 4\.0\. Data archive updated 7 October 2026; accessed October 2026Cited by:[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px1.p1.1)\.
- Gaoet al\.\(2025\)B\. Gao, F\. Song, Z\. Yang, Z\. Cai, Y\. Miao, Q\. Dong, L\. Li, C\. Ma, L\. Chen, R\. Xu, Z\. Tang, B\. Wang, D\. Zan, S\. Quan, G\. Zhang, L\. Sha, Y\. Zhang, X\. Ren, T\. Liu, and B\. ChangOmni\-MATH: a universal Olympiad level mathematic benchmark for large language models\.InInternational Conference on Learning Representations \(ICLR\),Note:arXiv:2410\.07985Cited by:[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px1.p1.1)\.
- Georgievet al\.\(2025a\)B\. Georgiev, J\. Gómez\-Serrano, T\. Tao, and A\. Z\. WagnerAlphaEvolve repository of problems\.Note:[https://github\.com/google\-deepmind/alphaevolve\_repository\_of\_problems](https://github.com/google-deepmind/alphaevolve_repository_of_problems)Accompanies arXiv:2511\.02864; repository at commit 8f44745 \(11 July 2026\); accessed October 2026Cited by:[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px3.p1.1)\.
- Georgievet al\.\(2025b\)B\. Georgiev, J\. Gómez\-Serrano, T\. Tao, and A\. Z\. WagnerMathematical exploration and discovery at scale\.arXiv preprint arXiv:2511\.02864\.External Links:[Link](https://arxiv.org/abs/2511.02864)Cited by:[§1](https://arxiv.org/html/2610.37739#S1.p1.1)\.
- Glazeret al\.\(2024\)E\. Glazer, E\. Erdil, T\. Besiroglu, D\. Chicharro, E\. Chen, A\. Gunning, C\. F\. Olsson, J\. Denain, A\. Ho, E\. d\. O\. Santos,et al\.FrontierMath: a benchmark for evaluating advanced mathematical reasoning in AI\.arXiv preprint arXiv:2411\.04872\.Cited by:[§1](https://arxiv.org/html/2610.37739#S1.p1.1),[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px1.p1.1)\.
- Green \(2025\)B\. Green100 open problems\.Note:[https://people\.maths\.ox\.ac\.uk/greenbj/papers/open\-problems\.pdf](https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf)Manuscript, circulated since 2018; version of December 2025\. Accessed September 2026Cited by:[Appendix B](https://arxiv.org/html/2610.37739#A2.p1.1),[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px3.p1.1),[§3\.1](https://arxiv.org/html/2610.37739#S3.SS1.SSS0.Px1.p1.1)\.
- Heet al\.\(2024\)C\. He, R\. Luo, Y\. Bai, S\. Hu, Z\. Thai, J\. Shen, J\. Hu, X\. Han, Y\. Huang, Y\. Zhang, J\. Liu, L\. Qi, Z\. Liu, and M\. SunOlympiadBench: a challenging benchmark for promoting AGI with Olympiad\-level bilingual multimodal scientific problems\.InProceedings of the 62nd Annual Meeting of the Association for Computational Linguistics \(Volume 1: Long Papers\),Bangkok, Thailand,pp\. 3828–3850\.Cited by:[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px1.p1.1)\.
- Hendryckset al\.\(2021\)D\. Hendrycks, C\. Burns, S\. Kadavath, A\. Arora, S\. Basart, E\. Tang, D\. Song, and J\. SteinhardtMeasuring mathematical problem solving with the MATH dataset\.InProceedings of the Neural Information Processing Systems Track on Datasets and Benchmarks \(NeurIPS 2021\),Note:arXiv:2103\.03874Cited by:[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px1.p1.1)\.
- Hubertet al\.\(2026\)T\. Hubert, R\. Mehta, L\. Sartran, M\. Z\. Horváth, G\. Žužić, E\. Wieser, A\. Huang, J\. Schrittwieser, Y\. Schroecker, H\. Masoom, O\. Bertolli, T\. Zahavy, A\. Mandhane, J\. Yung, I\. Beloshapka, B\. Ibarz, V\. Veeriah, L\. Yu, O\. Nash, P\. Lezeau, S\. Mercuri, C\. Sönne, B\. Mehta, A\. Davies, D\. Zheng, F\. Pedregosa, Y\. Li, I\. von Glehn, M\. Rowland, S\. Albanie, A\. Velingker, S\. Schmitt, E\. Lockhart, E\. Hughes, H\. Michalewski, N\. Sonnerat, D\. Hassabis, P\. Kohli, and D\. SilverOlympiad\-level formal mathematical reasoning with reinforcement learning\.Nature651\(8106\),pp\. 607–613\.Note:AlphaProof\. Published online 12 November 2025External Links:[Document](https://dx.doi.org/10.1038/s41586-025-09833-y)Cited by:[§1](https://arxiv.org/html/2610.37739#S1.p1.1),[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px2.p1.1)\.
- Juet al\.\(2026\)H\. Ju, B\. Dong, and G\. BércziICMConjectures: a collection of open conjectures from the ICM proceedings\.Note:[https://www\.icmconjectures\.com/](https://www.icmconjectures.com/)Announced 28 August 2026 at[https://frenzymath\.com/blog/icmconjectures/](https://frenzymath.com/blog/icmconjectures/)\. Accessed September 2026Cited by:[§1](https://arxiv.org/html/2610.37739#S1.p2.1),[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px3.p1.1),[§3\.1](https://arxiv.org/html/2610.37739#S3.SS1.SSS0.Px1.p1.1)\.
- Khukhro and Mazurov \(2026\)E\. I\. Khukhro and V\. D\. MazurovUnsolved problems in group theory\. The Kourovka Notebook\.Note:[https://arxiv\.org/abs/1401\.0300](https://arxiv.org/abs/1401.0300)21st edition \(arXiv:1401\.0300v46\)\. Accessed September 2026Cited by:[Appendix B](https://arxiv.org/html/2610.37739#A2.p1.1),[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px3.p1.1),[§3\.1](https://arxiv.org/html/2610.37739#S3.SS1.SSS0.Px1.p1.1)\.
- Kirby \(1997\)R\. KirbyProblems in low\-dimensional topology\.InGeometric Topology \(Athens, GA, 1993\),W\. H\. Kazez \(Ed\.\),AMS/IP Studies in Advanced Mathematics, Vol\.2\.2,pp\. 35–473\.Cited by:[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px3.p1.1)\.
- Laurentet al\.\(2024\)J\. M\. Laurent, J\. D\. Janizek, M\. Ruzo, M\. M\. Hinks, M\. J\. Hammerling, S\. Narayanan, M\. Ponnapati, A\. D\. White, and S\. G\. RodriquesLAB\-Bench: measuring capabilities of language models for biology research\.arXiv preprint arXiv:2407\.10362\.External Links:[Link](https://arxiv.org/abs/2407.10362)Cited by:[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px1.p1.1)\.
- Linet al\.\(2025\)Y\. Lin, S\. Tang, B\. Lyu, J\. Wu, H\. Lin, K\. Yang, J\. Li, M\. Xia, D\. Chen, S\. Arora, and C\. JinGoedel\-Prover: a frontier model for open\-source automated theorem proving\.InSecond Conference on Language Modeling \(COLM\),Note:arXiv:2502\.07640Cited by:[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px2.p1.1)\.
- Liuet al\.\(2026\)J\. Liu, G\. Gao, Z\. Sun, B\. Wu, S\. Liu, J\. Jiang, H\. Ju, L\. Chen, R\. Cheng, X\. Zhang,et al\.Danus: orchestrating mathematical reasoning agents with fact\-graph memory\.arXiv preprint arXiv:2607\.06447\.Cited by:[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px2.p1.1)\.
- Luonget al\.\(2025\)T\. Luong, D\. Hwang, H\. H\. Nguyen, G\. Ghiasi, Y\. Chervonyi, I\. Seo, J\. Kim, G\. Bingham, J\. Lee, S\. Mishra, A\. Zhai, H\. Hu, H\. Michalewski, J\. Kim, J\. Ahn, J\. Bae, X\. Song, T\. H\. Trinh, Q\. V\. Le, and J\. JungTowards robust mathematical reasoning\.InProceedings of the 2025 Conference on Empirical Methods in Natural Language Processing \(EMNLP\),Suzhou, China,pp\. 35418–35442\.Note:Introduces IMO\-ProofBench; arXiv:2511\.01846Cited by:[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px2.p1.1)\.
- Novikovet al\.\(2025\)A\. Novikov, N\. Vũ, M\. Eisenberger, E\. Dupont, P\. Huang, A\. Z\. Wagner, S\. Shirobokov, B\. Kozlovskii, F\. J\. R\. Ruiz, A\. Mehrabian, M\. P\. Kumar, A\. See, S\. Chaudhuri, G\. Holland, A\. Davies, S\. Nowozin, P\. Kohli, and M\. BalogAlphaEvolve: a coding agent for scientific and algorithmic discovery\.arXiv preprint arXiv:2506\.13131\.External Links:[Link](https://arxiv.org/abs/2506.13131)Cited by:[§1](https://arxiv.org/html/2610.37739#S1.p1.1)\.
- Open Problem Garden contributors \(2026\)Open Problem Garden contributorsOpen Problem Garden: a collection of unsolved problems in mathematics\.Note:[https://www\.openproblemgarden\.org/](https://www.openproblemgarden.org/)Accessed September 2026Cited by:[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px3.p1.1)\.
- Petrovet al\.\(2025\)I\. Petrov, J\. Dekoninck, L\. Baltadzhiev, M\. Drencheva, K\. Minchev, M\. Balunović, N\. Jovanović, and M\. VechevProof or bluff? Evaluating LLMs on 2025 USA Math Olympiad\.arXiv preprint arXiv:2503\.21934\.External Links:[Link](https://arxiv.org/abs/2503.21934)Cited by:[§1](https://arxiv.org/html/2610.37739#S1.p1.1),[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px2.p1.1)\.
- Phanet al\.\(2025\)L\. Phan, A\. Gatti, Z\. Han, N\. Li, J\. Hu, H\. Zhang, C\. B\. C\. Zhang, M\. Shaaban, J\. Ling, S\. Shi,et al\.Humanity’s Last Exam\.arXiv preprint arXiv:2501\.14249\.Cited by:[§1](https://arxiv.org/html/2610.37739#S1.p1.1),[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px1.p1.1)\.
- Reinet al\.\(2023\)D\. Rein, B\. L\. Hou, A\. C\. Stickland, J\. Petty, R\. Y\. Pang, J\. Dirani, J\. Michael, and S\. R\. BowmanGPQA: a graduate\-level Google\-proof Q&A benchmark\.arXiv preprint arXiv:2311\.12022\.Cited by:[§1](https://arxiv.org/html/2610.37739#S1.p1.1),[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px1.p1.1)\.
- Renet al\.\(2025\)Z\. Z\. Ren, Z\. Shao, J\. Song, H\. Xin, H\. Wang, W\. Zhao, L\. Zhang, Z\. Fu, Q\. Zhu, D\. Yang, Z\. F\. Wu, Z\. Gou, S\. Ma, H\. Tang, Y\. Liu, W\. Gao, D\. Guo, and C\. RuanDeepSeek\-Prover\-V2: advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition\.arXiv preprint arXiv:2504\.21801\.External Links:[Link](https://arxiv.org/abs/2504.21801)Cited by:[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px2.p1.1)\.
- Robertset al\.\(2024\)M\. Roberts, H\. Thakur, C\. Herlihy, C\. White, and S\. DooleyTo the cutoff… and beyond? A longitudinal perspective on LLM data contamination\.InInternational Conference on Learning Representations \(ICLR\),Cited by:[§1](https://arxiv.org/html/2610.37739#S1.p1.1),[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px1.p1.1)\.
- Romera\-Paredeset al\.\(2024\)B\. Romera\-Paredes, M\. Barekatain, A\. Novikov, M\. Balog, M\. P\. Kumar, E\. Dupont, F\. J\. R\. Ruiz, J\. S\. Ellenberg, P\. Wang, O\. Fawzi, P\. Kohli, and A\. FawziMathematical discoveries from program search with large language models\.Nature625\(7995\),pp\. 468–475\.Note:FunSearchExternal Links:[Document](https://dx.doi.org/10.1038/s41586-023-06924-6)Cited by:[§1](https://arxiv.org/html/2610.37739#S1.p1.1)\.
- Sainzet al\.\(2023\)O\. Sainz, J\. A\. Campos, I\. García\-Ferrero, J\. Etxaniz, O\. Lopez de Lacalle, and E\. AgirreNLP evaluation in trouble: on the need to measure LLM data contamination for each benchmark\.InFindings of the Association for Computational Linguistics: EMNLP 2023,Singapore,pp\. 10776–10787\.Cited by:[§1](https://arxiv.org/html/2610.37739#S1.p1.1),[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px1.p1.1)\.
- Smale \(1998\)S\. SmaleMathematical problems for the next century\.The Mathematical Intelligencer20\(2\),pp\. 7–15\.External Links:[Document](https://dx.doi.org/10.1007/BF03025291)Cited by:[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px3.p1.1)\.
- The Formal Conjectures Authors \(2025\)The Formal Conjectures AuthorsThe Formal Conjectures repository\.Note:[https://github\.com/google\-deepmind/formal\-conjectures](https://github.com/google-deepmind/formal-conjectures)Google DeepMind; formal statements of conjectures in Lean 4 / Mathlib\. Accessed September 2026Cited by:[§1](https://arxiv.org/html/2610.37739#S1.p2.1),[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px3.p1.1),[§3\.1](https://arxiv.org/html/2610.37739#S3.SS1.SSS0.Px1.p1.1),[§4\.1](https://arxiv.org/html/2610.37739#S4.SS1.SSS0.Px1.p1.1)\.
- The mathlib Community \(2020\)The mathlib CommunityThe Lean mathematical library\.InProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs \(CPP 2020\),New Orleans, LA, USA,pp\. 367–381\.External Links:[Document](https://dx.doi.org/10.1145/3372885.3373824)Cited by:[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px2.p1.1),[§3\.1](https://arxiv.org/html/2610.37739#S3.SS1.SSS0.Px4.p1.1),[§4\.1](https://arxiv.org/html/2610.37739#S4.SS1.SSS0.Px3.p1.1)\.
- TheoremDB \(2026\)TheoremDBTheoremDB: a public workspace for machine mathematics\.Note:[https://www\.theoremdb\.org/](https://www.theoremdb.org/)Problem packets with explicit statements and dated source\-side status; a subset carries Lean 4 declarations\. Accessed September 2026Cited by:[§1](https://arxiv.org/html/2610.37739#S1.p2.1),[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px3.p1.1),[§3\.1](https://arxiv.org/html/2610.37739#S3.SS1.SSS0.Px1.p1.1)\.
- Tianet al\.\(2024\)M\. Tian, L\. Gao, S\. D\. Zhang, X\. Chen, C\. Fan, X\. Guo, R\. Haas, P\. Ji, K\. Krongchon, Y\. Li, S\. Liu, D\. Luo, Y\. Ma, H\. Tong, K\. Trinh, C\. Tian, Z\. Wang, B\. Wu, Y\. Xiong, S\. Yin, M\. Zhu, K\. Lieret, Y\. Lu, G\. Liu, Y\. Du, T\. Tao, O\. Press, J\. Callan, E\. Huerta, and H\. PengSciCode: a research coding benchmark curated by scientists\.InAdvances in Neural Information Processing Systems 37 \(NeurIPS 2024\), Datasets and Benchmarks Track,Note:arXiv:2407\.13168Cited by:[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px1.p1.1)\.
- Trinhet al\.\(2024\)T\. H\. Trinh, Y\. Wu, Q\. V\. Le, H\. He, and T\. LuongSolving olympiad geometry without human demonstrations\.Nature625\(7995\),pp\. 476–482\.Note:AlphaGeometryExternal Links:[Document](https://dx.doi.org/10.1038/s41586-023-06747-5)Cited by:[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px2.p1.1)\.
- Tsoukalaset al\.\(2024\)G\. Tsoukalas, J\. Lee, J\. Jennings, J\. Xin, M\. Ding, M\. Jennings, A\. Thakur, and S\. ChaudhuriPutnamBench: evaluating neural theorem\-provers on the Putnam mathematical competition\.InAdvances in Neural Information Processing Systems 37 \(NeurIPS 2024\), Datasets and Benchmarks Track,Note:arXiv:2407\.11214Cited by:[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px2.p1.1)\.
- Wanget al\.\(2025\)H\. Wang, M\. Unsal, X\. Lin, M\. Baksys, J\. Liu, M\. Dos Santos, F\. Sung, M\. Vinyes, Z\. Ying, Z\. Zhu, J\. Lu, H\. de Saxcé, B\. Bailey, C\. Song, C\. Xiao, D\. Zhang, E\. Zhang, F\. Pu, H\. Zhu, J\. Liu, J\. Bayer, J\. Michel, L\. Yu, L\. Dreyfus\-Schmidt, L\. Tunstall, L\. Pagani, M\. Machado, P\. Bourigault, R\. Wang, S\. Polu, T\. Barroyer, W\. Li, Y\. Niu, Y\. Fleureau, Y\. Hu, Z\. Yu, Z\. Wang, Z\. Yang, Z\. Liu, and J\. LiKimina\-Prover Preview: towards large formal reasoning models with reinforcement learning\.arXiv preprint arXiv:2504\.11354\.External Links:[Link](https://arxiv.org/abs/2504.11354)Cited by:[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px2.p1.1)\.
- Whiteet al\.\(2025\)C\. White, S\. Dooley, M\. Roberts, A\. Pal, B\. Feuer, S\. Jain, R\. Shwartz\-Ziv, N\. Jain, K\. Saifullah, S\. Dey, Shubh\-Agrawal, S\. S\. Sandha, S\. Naidu, C\. Hegde, Y\. LeCun, T\. Goldstein, W\. Neiswanger, and M\. GoldblumLiveBench: a challenging, contamination\-limited LLM benchmark\.InInternational Conference on Learning Representations \(ICLR\),Note:arXiv:2406\.19314Cited by:[§1](https://arxiv.org/html/2610.37739#S1.p2.1),[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px1.p1.1)\.
- Wikipedia contributors \(2026\)Wikipedia contributorsList of unsolved problems in mathematics\.Note:[https://en\.wikipedia\.org/wiki/List\_of\_unsolved\_problems\_in\_mathematics](https://en.wikipedia.org/wiki/List_of_unsolved_problems_in_mathematics)Wikipedia, The Free Encyclopedia\. Accessed September 2026Cited by:[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px3.p1.1),[§3\.1](https://arxiv.org/html/2610.37739#S3.SS1.SSS0.Px1.p1.1)\.
- Zhanget al\.\(2025\)J\. Zhang, C\. Petrui, K\. Nikolić, and F\. TramèrRealMath: a continuous benchmark for evaluating language models on research\-level mathematics\.InAdvances in Neural Information Processing Systems 38 \(NeurIPS 2025\), Datasets and Benchmarks Track,Note:arXiv:2505\.12575Cited by:[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px1.p1.1)\.
- Zhenget al\.\(2022\)K\. Zheng, J\. M\. Han, and S\. PoluminiF2F: a cross\-system benchmark for formal Olympiad\-level mathematics\.InInternational Conference on Learning Representations \(ICLR\),Note:arXiv:2109\.00110Cited by:[§2](https://arxiv.org/html/2610.37739#S2.SS0.SSS0.Px2.p1.1)\.

## Appendix ABenchmark item lists

Tables[A](https://arxiv.org/html/2610.37739#A1)and[A](https://arxiv.org/html/2610.37739#A1)list all 200 items of OpenFrontiers\-Bench; a bullet after the ID marks the 50 items of HQ\-50\. The problem column is the English item title, truncated where long; it is a curator title, not the text shown to a model, which receives the Lean file of the solver packet \(Appendix[E](https://arxiv.org/html/2610.37739#A5)\)\. Areas are a curator grouping into ten areas\. For Rediscovery\-110,*T*is the evidence tier \(Appendix[C](https://arxiv.org/html/2610.37739#A3)\),*Date*the year and month of the located solution evidence, and*AI*the disclosure class of the solution materials:*AI*, an AI system is credited with the key mathematics;*assist*, assistance is disclosed and the solution is attributed to humans;*none*, no AI use was disclosed in the reviewed materials, which does not imply that none occurred\. For Open\-90,*Prio\.*is the implementation priority \(pilot, core or stretch; not a difficulty estimate\) and*Cert\.*marks items where one direction is settled by a single finite object\. Solution URLs, split groups, Lean declaration names, scope differences, review verdicts and pending gates are kept in the package files\.

IDProblemAreaTDateAIR01∙\\bulletLin–Wimmer rank\-minimization conjecture \(rank\-minimization analogue of Roth’s similarity theorem\)Alg\./matrixA26\-09noneR02Huang’s weak majorization problem for singular values of Hadamard products of nonnegative matricesAlg\./matrixA26\-09noneR03Teschner’s bondage\-number conjectureGraph th\.A26\-09AIR04∙\\bulletGowers Ukuncertainty conjectureAdd\. comb\.A26\-09noneR05Kourovka 21\.137: if the p\-th powers of a finite p\-group form a subgroup, must it be powerful?Group th\.A26\-09AIR06Queens each attacking at most one other queen \(exact extremal value\)Comb\.B26\-08noneR07∙\\bulletGreen problem 3: measure of open product\-free setsAdd\. comb\.A26\-07assistR08Planar Pompeiu / Schiffer conjectureGeom\./top\.A26\-08assistR10Kourovka 6\.30: Is the profinite completion of a residually finite Hopfian group topologically Hopfian?Group th\.B26\-07noneR12Kourovka Notebook Problem 18\.16 \(definable endomorphisms of ordered abelian groups\)Group th\.B26\-08assistR13Kourovka Notebook Problem 21\.87 \(A\. Lucchini\): generating a finite group from d\-generator subgroups of…Group th\.B26\-08AIR14Kourovka Notebook Problem 21\.142 \(embedding into groups invariably generated by a p\-element and a q\-element\)Group th\.B26\-08AIR15Kourovka Notebook Problem 12\.15 \(finite 2\-groups in which equal normal closures force conjugacy\)Group th\.A26\-08AIR16Kourovka Notebook Problem 21\.88 \(D\. MacHale\): odd\-order groups with k\(G\)/\|\|G\|\|= 1/17Group th\.B26\-08noneR17Open Quantum Problems 35 \(seven\-party case\): local dimensions admitting an AME\(7,d\) stateTCS/logicB26\-08assistR18Alfeld’s conjecture on vertex interpolation by C1cubic splinesAnal\./PDEA26\-09noneR19Periodicity conjecture for finite\-dimensional algebras \(Erdmann–Skowroński\)Alg\./matrixA26\-09AIR20Quantum Fourier Entropy–Influence \(QFEI\) conjecture of Bu–Garcia–Jaffe–Koh–LiAnal\./PDEB26\-08assistR21Polujan–Pott conjecture on bent functions whose translation designs have a 2\-transitive automorphism groupGroup th\.A26\-09assistR22Resistance diameter of a graph versus its line graphGraph th\.C26\-09noneR23∙\\bulletGao’s conjectureν\\nu\(G\) = d\(G\)−\-1 for the van Emde Boas zero\-sum invariantAdd\. comb\.A26\-09noneR24BFGS with exact \(first\-local\-minimizer\) strong Wolfe line searches for arbitrary line\-search constants 0 < c1…TCS/logicC26\-09assistR25Friedgut’s conjecture on influential coalitions on the continuous cube \[0,1\]nComb\.C26\-09assistR26Chen–Li gap\-entropy conjecture for best\-arm identification \(order\-oblivious instance\-wise bound\)TCS/logicA26\-09assistR27Horn’s coincidence conjecture for commuting self\-maps of a compact convex setGeom\./top\.B26\-09noneR28Audenaert–Kittaneh: can the Aujla–Bourin subadditivity inequality for concave matrix functions be…Alg\./matrixB26\-09noneR29∙\\bulletBourin–Lee: optimality of the constant k/4 for an odd number of contractionsAlg\./matrixA26\-09assistR30Decidability of reachability for branching vector addition systems \(BVAS\)TCS/logicC26\-07noneE01∙\\bulletErdős Problem \#106: is f\(k2\+1\) = k for the maximal total side length of squares packed in a unit square?Geom\./top\.A26\-07AIE02Erdős Problem \#125: does A \+ B have positive lower density \(A, B = digits \{0,1\} in base 3, 4\)?Add\. comb\.A26\-03AIE03∙\\bulletErdős Problem \#152: isolated elements of the sumset of a finite Sidon setAdd\. comb\.A26\-04AIE04∙\\bulletErdős Problem \#193: must an infinite bounded\-step walk inℤ\\mathbb\{Z\}3contain three collinear points?Geom\./top\.A26\-08assistE05Erdős Problem \#347: is there a sequence with ratio tending to 2 whose cofinite subsequences all have subset…Number th\.A26\-01assistE06∙\\bulletErdős Problem \#358: is there an increasing integer sequence whose consecutive\-block sums represent every…Add\. comb\.A26\-02assistE07Erdős Problem \#387: is there an absolute constant c \> 0 such that every binomial coefficient C\(n, k\) with 1≤\\leq…Number th\.B26\-05assistE08Erdős Problem \#477: is there a polynomial f :ℤ\\mathbb\{Z\}→\\toℤ\\mathbb\{Z\}of degree at least 2 and a set A⊆\\subseteqℤ\\mathbb\{Z\}such that every…Number th\.A26\-06AIE09Erdős Problem \#570: Ramsey number of a cycle Ckversus a graph with m edgesGraph th\.B26\-01noneE10Erdős Problem \#633: triangles that can only be cut into a square number of congruent trianglesNumber th\.B26\-04AIE11Erdős Problem \#650: matching integers to distinct multiples in an interval of length 2NNumber th\.A26\-03assistE12∙\\bulletErdős Problem \#865: does density 5/8 \+ C force three elements with all pairwise sums in the set?Add\. comb\.A26\-06AIE13∙\\bulletErdős Problem \#868: bases of order 2 with many representations and minimal subbasesNumber th\.A26\-01assistE14∙\\bulletErdős Problem \#987 \(second question\): can the exponential\-sum limsups satisfy Ak= o\(k\)?Anal\./PDEA26\-04AIE15Erdős Problem \#990: does the Erdős–Turán angular discrepancy bound hold with the number of non\-zero…Anal\./PDEA26\-04AIE16Erdős Problem \#997: well\-distribution of the fractional parts \{α\\alphapn\} along the primesNumber th\.B26\-03AIE17Erdős Problem \#1044: infimum of the longest boundary of a component of a polynomial lemniscateGeom\./top\.A26\-01assistE18Erdős Problem \#1138: primes in intervals of length C times the maximal prime gapNumber th\.A26\-04assistE19Erdős Problem \#1148: is every large n of the form x2\+ y2−\-z2with max\(x2, y2, z2\)≤\\leqn?Number th\.A26\-03AIE20Erdős Problem \#1153: the Lebesgue function on a fixed subintervalAnal\./PDEA26\-02assistE21∙\\bulletErdős Problem \#1196: reciprocal\-log sums of primitive sets far from the originNumber th\.A26\-04AIE22Erdős Problem \#1197: integer dilates of a set of positive measureNumber th\.A26\-04assistE23Kourovka Notebook Problem 14\.54: number of conjugacy classes versus nilpotent subgroupsGroup th\.A26\-06noneE24Kourovka Notebook Problem 17\.99: faithfulness of a germ representation of the Baumslag groupGroup th\.A26\-06noneE25Kourovka Notebook Problem 21\.8: groups generated by class transpositions of equal modulusGroup th\.A26\-04noneE26Kourovka Notebook Problem 21\.10: just finite presentations of finite groupsGroup th\.B26\-05assistE27Kourovka Notebook Problem 21\.14: endomorphisms that extend along every homomorphismGroup th\.B26\-04noneE28Kourovka Notebook Problem 21\.24: power graphs of finite groups — cograph implies chordal?Group th\.A26\-01AIE29Simple groups of non\-uniform exponential growth \(Kourovka Notebook 21\.117\(a\)\)Group th\.B26\-05assistE30Rank of Z\(⟨\\langlea,B⟩\\rangle\)∩\\cap⟨\\langlea,B⟩′\\rangle^\{\\prime\}in extensions of elementary abelian groups \(Kourovka Notebook 21\.150\)Group th\.A26\-03AIN01∙\\bulletBeck–Fiala conjecture: is the discrepancy of degree\-t set systems O\(√\\surdt\)?Comb\.A26\-09AIN02Kourovka 20\.76: abelian subgroups of finite p\-groups and the bound p\(2k\)Group th\.B26\-09assistN03Tu–Deng conjectureTCS/logicA26\-07assistN04Isζ\\zeta\(5\) irrational?Number th\.A26\-09AIN05∙\\bulletErdős’s unit distance problem \(Erdős Problem \#90\): is u\(n\) < n1\+ε\\varepsilonfor everyε\\varepsilon\> 0 and all large n?Geom\./top\.A26\-05AIN06Multicolour Ramsey numbers for triangles: determine limk→∞\\to\\inftyR\(3;k\)1/k\(Erdős Problem \#183\)Graph th\.A26\-08AI*continued*
\\@makecaption

Rediscovery\-110 \(110 items; R, E, and N stand for three rounds of data selection with different cutoff dates\)\.∙\\bullet= in HQ\-50\. T = tier; Date = located solution evidence \(YY\-MM\); AI = disclosure class\.

IDProblemAreaPrio\.Cert\.O01Erdős Problem \#242 \(Erdős–Straus conjecture\): for every n \> 2, is 4/n a sum of three distinct unit fractions?Number th\.coreyesO02∙\\bulletLehmer’s totient problem: is there a composite n withφ\\varphi\(n\)∣\\midn−\-1?Number th\.coreyesO03Erdős–Moser equation: does 1k\+ 2k\+⋯\\cdots\+ \(m\-1\)k= mkhave any positive integer solution other than \(k, m\)…Number th\.coreyesO04Kurepa’s left factorial conjecture \(prime version\): no odd prime p divides \!p = 0\! \+ 1\! \+ … \+ \(p\-1\)\!Number th\.coreO05Singmaster’s conjecture: bounded multiplicity of entries \(other than 1\) in Pascal’s triangleNumber th\.stretchO06Perfect cuboid existenceNumber th\.coreyesO07Conway’s 99\-graph problemGraph th\.pilotO08Graceful tree conjecture \(Ringel–Kotzig conjecture\)Graph th\.coreO09Sheehan’s conjecture: every 4\-regular Hamiltonian graph has a second Hamiltonian cycleGraph th\.coreO10Reed’s omega, delta, and chi conjectureGraph th\.coreO11Vizing’s domination conjectureGraph th\.coreO12Union\-closed sets conjecture \(Frankl’s conjecture\)Comb\.coreO13The 1/3–2/3 conjectureComb\.coreO14Barker sequences have length at most 13 \(the Barker conjecture\)Comb\.pilotyesO16Hadamard conjecture: a Hadamard matrix of order 4k exists for every positive integer kComb\.coreO17The Gerstenhaber problem for three commuting matricesAlg\./matrixpilotO18Marcus–de Oliveira determinantal conjectureAlg\./matrixcoreO20Kaplansky zero divisor conjectureNumber th\.stretchO21Černý conjectureTCS/logiccoreO22∙\\bulletScholz addition chain conjectureTCS/logiccoreyesO24Rule 30 center column not eventually periodic \(Rule 30 Prize, Problem 1\)TCS/logicstretchO25Rational distance problem \(unit square\)Geom\./top\.coreO26Lonely runner conjectureGeom\./top\.stretchO27Inscribed square problem \(Toeplitz square peg problem\)Geom\./top\.stretchO29Irrationality of the Euler–Mascheroni constantNumber th\.stretchO30Littlewood conjectureAnal\./PDEstretchO31Zariski Cancellation Problem for affine space in characteristic zeroGeom\./top\.stretchyesO32∙\\bulletErdős Matching Conjecture: maximum number of edges of an r\-uniform hypergraph with no k pairwise disjoint…Comb\.stretchyesO33∙\\bulletErdős–Szekeres "Happy Ending" conjecture: f\(n\) = 2\(n\-2\)\+ 1Geom\./top\.stretchyesO34Gallai’s path decomposition conjecture \(Erdős Problem \#583\)Graph th\.stretchyesO35Erdős–Selfridge odd covering problem: is there a covering system with distinct odd moduli \> 1?Number th\.stretchyesO36∙\\bulletPrime power conjecture for finite projective planes \(Erdős Problem \#723\)Comb\.stretchyesO37Maximum number of mutually unbiased bases in C6Comb\.stretchO38∙\\bulletBorsuk’s partition problem in dimensions 4≤\\leqn≤\\leq62 \(prove or disprove\)Geom\./top\.pilotyesO39Ryser’s conjecture: every Latin square of odd order has a transversalComb\.stretchyesO40Kummer–Vandiver conjecture: p does not divide the class number ofℚ\\mathbb\{Q\}\(ζ\\zetap\)\+Number th\.stretchyesO41∙\\bulletSidorenko’s conjecture: t\(H, G\)≥\\geqt\(K2, G\)e\(H\)for every bipartite graph HGraph th\.stretchyesO42Mazur rotations problem \(Banach–Mazur rotation problem\): is every separable infinite\-dimensional Banach space…Anal\./PDEstretchO43Erdős Problem \#159: R\(C4, Kn\)≪\\lln2−\-cfor some c \> 0Graph th\.stretchO44Erdős Problem \#20 \(Erdős–Rado sunflower conjecture\): is f\(n,k\) < ckn?Comb\.stretchO45Erdős Problem \#39: an infinite Sidon set with counting function≫\\ggε\\varepsilonN1/2−ε\-\\varepsilonAdd\. comb\.stretchO46Chowla’s cosine problem \(Erdős Problem \#510\): does every set A of N positive integers admitθ\\thetawithΣ\\Sigman∈\\inA…Add\. comb\.stretchO47Erdős Problem \#572: the even\-cycle Turán lower bound ex\(n; C2k\)≫\\ggn1\+1/kfor every k≥\\geq3Graph th\.stretchO48The Erdős–Hajnal conjecture: graphs with no induced copy of a fixed graph H contain a clique or an…Graph th\.stretchO49Erdős Problem \#564 \(Erdős–Hajnal–Rado\): is the diagonal 3\-uniform hypergraph Ramsey number R3\(n\) doubly…Comb\.stretchO50Erdős Problem \#714: is the Kővári–Sós–Turán bound sharp, i\.e\. is ex\(n; Kr,r\)≫\\ggn2\-1/rfor every r≥\\geq2?Graph th\.stretchO51Green’s Problem 94 \(Erdős similarity problem for \{1, 1/2, 1/4, …\}\): does every set A⊂\\subsetℝ\\mathbb\{R\}of positive…Anal\./PDEstretchO52Power\-saving bound for 4\-AP\-free sets in F5n\(Green’s Problem 9\(iii\)\)Add\. comb\.stretchO53∙\\bulletThe Andrews–Curtis conjecture for balanced presentations of the trivial groupGroup th\.stretchO54Babai’s conjecture for alternating groups: diam\(An\) is polynomially bounded in nGroup th\.stretchO55Falconer’s distance set conjecture in the planeGeom\./top\.stretchO56∙\\bulletLehmer’s problem: Mahler measures of integer polynomials are bounded away from 1Number th\.stretchO57Auslander–Reiten conjecture for Artin algebrasAlg\./matrixstretchO58Erdős Problem \#1029: does the diagonal Ramsey number satisfy R\(k\) / \(k⋅\\cdot2k/2\)→\\to∞\\infty?Graph th\.stretchO59The Alon–Tarsi 7/5 short cycle cover conjectureGraph th\.stretchyesO60Friedland’s conjecture on the generic rank of complex 3\-tensors in the critical rangeAlg\./matrixstretchO61Erdős–Rousseau sparse\-halves problem \(Erdős Problem \#128\): if every induced subgraph on at least⌊\\lfloorn/2⌋\\rfloor…Graph th\.stretchyesO62Herzog–Schönheim conjecture: in a nontrivial coset partition of a group, two subgroups have the same index…Group th\.stretchyesO63Erdős Problem \#23: can every triangle\-free graph on 5n vertices be made bipartite by deleting at most n2…Graph th\.stretchyesO64Erdős Problem \#364 \(Erdős; Mollin–Walsh\): are there three consecutive powerful numbers?Number th\.stretchyesO65Erdős Problem \#324: is there an integer polynomial f whose pairwise sums f\(a\) \+ f\(b\), a < b nonnegative…Number th\.stretchO66Do odd weird numbers exist? \(Erdős Problem \#470, first question\)Number th\.stretchyesO67Erdős–Lovász Tihany conjecture: every graph withω\\omega\(G\) <χ\\chi\(G\) = a \+ b−\-1 \(a, b≥\\geq2\) is \(a, b\)\-splittableGraph th\.stretchyesO68Erdős–Gyárfás conjecture: every finite graph with minimum degree≥\\geq3 contains a cycle of length 2k\(k≥\\geq2\)Graph th\.coreyes*continued*
\\@makecaption

Open\-90 \(90 items\)\.∙\\bullet= in HQ\-50\. Prio\. = implementation priority; Cert\. = one direction settled by a finite object\.

## Appendix BSource collections

Table[B](https://arxiv.org/html/2610.37739#A2)lists the 62 source collections that contribute problem records in the snapshot of our OpenFrontiers, sorted by record count, with a shortened form of the reuse note recorded in the source registry \(metadata/sources\.json\); the full wording travels with every item insource\.license\. The other registered sources \(71 are registered in total\) are catalogue\-only: for the Kourovka Notebook\([Khukhro and Mazurov, 2026](https://arxiv.org/html/2610.37739#bib.bib33)\)\(1,935 catalogue entries\), Ben Green’s list of 100 problems\([Green, 2025](https://arxiv.org/html/2610.37739#bib.bib34)\), the K3 low\-dimensional topology list and similar indices, only bibliographic pointers were collected, not statements, so they appear in thecataloguesconfiguration and not in this table\. Record counts are source records, not deduplicated conjectures: several collections describe the same problem, and one record may contain several sub\-questions\. Seven collections have at least 100 records; 47 collections have at most 20 records each\. For the AlphaEvolve repository, 8 of its 67 pages \(rediscovery tests of classical results, a competition problem, a programming game and a logic puzzle\) are kept as catalogue rows only; the Optimization Constants and FrontierMath: Open Problems collections are imported in full\.

Source collectionRecordsLicense / reuse noteTheoremDB3,909Selected packets CC0\-1\.0; references keep their own termsAIM Problem Lists3,470Editorially moderated; per\-list termsICM Conjectures2,898Attribution retained; consult original proceedingsErdős Problems \(Thomas Bloom\)634See site; statements paraphrased with attributionFormal Conjectures459Code Apache\-2\.0; text CC BY 4\.0; third\-party terms keptOptimization Constants in Mathematics — Davis, Ivanisvili & Tao115Apache\-2\.0 repository; pages and bound tables attributedOpen Quantum Problems114Attribution retained; consult source for reuse termsAlphaEvolve Repository of Problems — Georgiev et al\.59Apache\-2\.0 repository; pages attributedEpoch AI — FrontierMath: Open Problems49CC BY 4\.0 \(Epoch AI\); pages and prompts attributedTableaux — A notebook of open problems48CC BY 4\.0 \(D\. R\. Worley\); HTML to Markdown, attributedQueueing, Predictions, and LLMs — Mitzenmacher & Shahout42CC BY 4\.0; attributed adaptation, HTML to MarkdownThe Open Problems Project \(computational geometry\)38Academic use with attributionCommunity consensus34Original wordingCOLT Open Problems — supplied archive30Authors keep copyright; papers and audit notes attributedTianyuan Workshop — Open Problems in Mathematical Logic22CC BY 4\.0; attributed adaptation, HTML to MarkdownJacobs — Twenty Open Problems in Quantum Control20Author attribution and references kept; per\-paper termsAnton Petrunin — A Gallery of Geometry Problems15CC0 1\.0 \(A\. Petrunin\); independent summaries of v2Randomstrasse101 — Open Problems of 202515CC BY 4\.0; Bandeira et al\.; HTML to Markdown, attributedAaronson — Quantum Query Complexity12Author attribution and references kept; per\-paper termsOberwolfach 2025 — Analytic Number Theory Problem Session11CC BY\-SA 4\.0; compiled by T\. F\. Bloom; share\-alike keptFOCS 2024 — Quantum Learning10Questions summarized with attribution; slides linkedSimons Institute — Lattices ’22 problems10Summarized with attribution to the Lattices ProgramDagstuhl 25041 — Graph Classes and Algorithmic Complexity8CC BY 4\.0; attributed editorial adaptationJoão Araújo — A survey on varieties generated by small semigroups and a companion website8Brief editorial summaries; article keeps its own licenseWikipedia — Computer science7CC BY\-SA 4\.0; adapted selections, contributors attributedClay Mathematics Institute — Millennium Prize Problems6Statements paraphrased; official formulations linkedWikipedia — Loop theory and quasigroup theory6CC BY\-SA 4\.0; adapted selections, contributors attributedBertrand Clarke — A Cheat Sheet for Bayesian Prediction5Brief editorial summaries; article keeps its own licenseWikipedia — Astronomy5CC BY\-SA 4\.0; adapted selections, contributors attributedWikipedia — Biology5CC BY\-SA 4\.0; adapted selections, contributors attributedWikipedia — Mathematics5CC BY\-SA 4\.0; adapted selections, contributors attributedWikipedia — Physics5CC BY\-SA 4\.0; adapted selections, contributors attributedDagstuhl 25081 — Semirings in Database Theory4CC BY 4\.0; attributed editorial adaptationJMLR — Pre\-trained Gaussian Processes for Bayesian Optimization4CC BY 4\.0; attributed editorial adaptationOpen Problems in Mathematical Biology — Vittadello & Stumpf4CC BY\-SA 4\.0; attributed adaptation, HTML to MarkdownOğuz Şavk — A survey of the homology cobordism group4Brief editorial summaries; article keeps its own licenseWikipedia — Geoscience4CC BY\-SA 4\.0; adapted selections, contributors attributedWikipedia — Information theory4CC BY\-SA 4\.0; adapted selections, contributors attributedWikipedia — Neuroscience4CC BY\-SA 4\.0; adapted selections, contributors attributedAlessandro Carlotto — The general relativistic constraint equations3Brief editorial summaries; article keeps its own licenseDagstuhl — Quantum Error Correction Meets ZX\-Calculus3CC BY 4\.0; section authors attributedFDIG 2025 — Open Problems in Information Geometry3Independent short summaries and pointers; no blanket licenseLiouville Quantum Gravity — Holden & Sun3CC BY 4\.0; attributed adaptation, HTML to MarkdownRobert Benedetto — Current trends and open problems in arithmetic dynamics3Brief editorial summaries; article keeps its own licenseUniversality in Computable Dynamical Systems — Old and New3Independent short summaries and pointers; no blanket licenseWikipedia — Chemistry3CC BY\-SA 4\.0; adapted selections, contributors attributedAndrii Mironchenko — Input\-to\-state stability of infinite\-dimensional systems: recent results and open questions2Brief editorial summaries; article keeps its own licenseArmin Schikorra — Invitation to H\-systems in higher dimensions: known results, new facts, and related open problems2Brief editorial summaries; article keeps its own licenseAxial Algebras — Questions and Conjectures2Independent short summaries and pointers; no blanket licenseEwin Tang — Quantum Learning Questions2Author attribution retained; consult source for termsOpen Problem Garden2Community wikiSIAM Optimization — Open Problems in Optimization2Independent short summaries and pointers; no blanket licenseSimons Workshop — Linear Systems and Eigenvalue Problems2Independent short summaries and pointers; no blanket licenseSmale’s problems for the 21st century2Paraphrased with citationWikipedia — Economics2CC BY\-SA 4\.0; adapted selections, contributors attributedWikipedia — Fair division2CC BY\-SA 4\.0; adapted selections, contributors attributedWikipedia — Statistics2CC BY\-SA 4\.0; adapted selections, contributors attributedarXiv preprints2Per\-paper license; metadata via arXiv APIJMLR — Fast Rates in PAC\-Bayes Meta\-Learning1CC BY 4\.0; attributed editorial adaptationKirby’s problem list in low\-dimensional topology1Paraphrased with citationNathan Segerlind — The complexity of propositional proofs1Brief editorial summaries; article keeps its own licenseXavier Blanc — The crystallization conjecture: a review1Brief editorial summaries; article keeps its own licenseTotal \(62 collections\)12,151*continued*
\\@makecaption

All 62 source collections contributing problem records, sorted by record count\. Records are source records, not deduplicated conjectures\. The reuse note is a shortened form of the registry wording carried on each row insource\.license; it is not a license grant by this project\.

## Appendix CCuration rubric

This appendix records the rules used to admit, tier, score and select benchmark items\. Scores are ordinal curator judgments, not expert consensus and not predictions of model success\.

#### Hard filters\.

A candidate enters Rediscovery\-110 only if \(i\) it was demonstrably a public research question before its resolution, with a traceable source; \(ii\) the located solution settles the same quantifiers and scope as the posed target, so that a special case, a “sufficiently largenn” result or a strengthened hypothesis does not count; \(iii\) no earlier solution was located before its round’s window \(after 2026\-06\-30 for R items, from 2026\-01\-01 for E and N items\); \(iv\) the solution is not a restatement of an old theorem, a withdrawn or retracted paper, or an announcement without proof; and \(v\) equivalent forms, parameter variants and direct corollaries of one construction are merged into one problem family\. An open item must be open in both directions at the status check, precisely posed and not a duplicate or special case of another item\. Every Lean statement records its scope differences from the original question \(for instance, a universe restriction that does not affect the answer\)\.

#### Split groups\.

Items that share a solution paper, a public release or a source are bound to one split group and should be reported as a group: the OpenAI “ten advances” release \(N06, N16, N19, N20, N31, N35, N46\), the Epoch AI FrontierMath Erdős release \(N10, N11, N12, N41\), Benkoski–Erdős 1974 \(N07, O66\), arXiv:2609\.20094 \(R28, R29\) and one paper solving Erdős \#987 and \#990 \(E14, E15\)\. All other items form singleton groups\.

#### Evidence tiers\.

Tier A \(85; R 14, E 23, N 48\): a finite certificate was independently recomputed with exact arithmetic, or a complete Lean proof of the answered statement was compiled locally, in most cases an AI\-assisted formalization; 75 Tier A items rest on a Lean proof and 10 on a certificate\. Four Tier A items \(R26, N13, N49, N50\) are conditional, each with the condition stated in its tier reason, and are excluded from HQ\-50\. Tier B \(21\): a complete solution is corroborated by the problem list’s acceptance, publication or an independent solution, but the full proof was not independently verified\. Tier C \(4: R22, R24, R25, R30\): a solution claim whose verification is pending\.

#### Scores\.

Each item carries ordinal 1–5 curator scores for importance \(1: no discernible research motivation; 3: a traceable, specialised research question; 5: a recognized central conjecture\), statement clarity, formalization cost and proof cost\. Importance is 3/4/5 for 22/49/39 solved items \(mean 4\.15\) and 6/45/39 open items \(mean 4\.37\)\. Scores are not combined into a composite except by the HQ\-50 ranking below\.

#### Dates\.

Each solved item stores the earliest located public solution date and its basis \(arXiv v1, dated public proof post, problem\-list edition, repository commit or manuscript date\)\. The audit read version histories, earlier PDFs, forum threads and pinned commits, but it was not an exhaustive priority search; a later publication, simplification or formalization does not reset a date\. Located dates run starting from 2026\-01\-05\.

#### Leakage controls in the statements\.

Lean files of solved items contain no answers, upstream declaration names or live links that display status\. Citations of erdosproblems\.com, OEIS and Green’s problem list are given as literature references rather than live pages, Wikipedia links point to a pre\-solution revision, and 16 Kourovka items cite a pre\-solution arXiv version of the notebook\. A second pass over the 110 solved files removed semantic hints \(declarative titles became questions; background sentences pointing to the solution route were deleted\)\. In the solver packet, items are renamed to P001–P200 in a salted order, file headers are unified and status\-revealing source lines are removed\.

#### HQ\-50 selection\.

For HQ\-50, we have several more filters compared to OpenFrontiers\-Bench\. Hard filters for all items: the statement compiles and passes the checker and probes, formalization confidence is high, no must\-fix issue, and if both review checks raised issues are all fixed; a newly written statement must have had its primary\-source wording verified\. Solved items must be unconditional Tier A with importance≥4\\geq 4\(importance 3 only if human\-solved, post\-cutoff and reviewed both passed\)\. Open items need importance≥4\\geq 4, clarity 5, both passed reviews, an unrepaired statement, an answer not easily guessed \(excluding O71\) and open status at the check\. The most frequent failures were open\-item reviews other than both passes \(22\), Tier B \(21\), open clarity below 5 \(19\), unfixed issues from both checks \(16\) and importance below 4 \(21 in total\); 55 solved and 48 open items qualified\. The ranking adds points for review outcome \(both passes\+2\+2, one passes\+1\+1\), importance \(55:\+2\+2;33:−1\-1\), a full Lean reference \(\+2\+2; certificate\+1\+1\), recency \(after 2026\-07\-01\+2\+2; April–June\+1\+1\), proof cost≥4\\geq 4\(\+1\+1\) and, for open items, a verbatim upstream statement \(\+1\.5\+1\.5\), a finite\-certificate direction \(\+1\+1\) and priority; it subtracts for unread primary sources, unfixed issues, repair rounds and many scope differences\. Greedy selection enforces one item per solution paper or problem family, two per public release \(three for the OpenAI release of seven unrelated problems\), at most 16 Erdős and 6 Kourovka solved items, at most 4 Erdős open items, at most 8 solved and 2 open items per area, and at most 21 solved items whose key mathematics came from OpenAI models, so that 19 remain for evaluating OpenAI models\. Two items were excluded by hand \(N03, N24; Appendix[G](https://arxiv.org/html/2610.37739#A7)\)\.

## Appendix DLean statements and checks

#### Corpus and platform\.

Corpus Lean attachments \(1,961 for 1,946 problems\) are display\-only: no Lean is executed at export time, the recorded lexicalsorry/admit/axiomscans are not a proof checker, and source\-side “verified” or “solved” labels are kept as dated claims\. Community submissions on the platform are checked separately \(profilelean4\-core\-4\.19\.0\-v1: Lean 4\.19\.0 withStdonly, the theorem built from the stored target, onlypropext,Classical\.choiceandQuot\.soundallowed, a fresh networkless container per check\); a successful check attaches a receipt to the submission and never changes a problem’s status\.

#### Benchmark package\.

The 200 statements form one Lake project pinned to Lean 4\.33\.1, Mathlib0df444aand Formal Conjectures89294ea, of which only the two utility libraries are vendored; a cleanlake buildsucceeds\. Each file declares exactly one theoremFrontierBench\.<ID\>\.main, andsorrymay appear only in the answer placeholder and in the proof ofmain\. Besides the checks of Section[4\.1](https://arxiv.org/html/2610.37739#S4.SS1), automated probes run onmainwith the correct and a wrong answer for solved yes/no items, with both answers for open yes/no items and with the correct answer for value items; no probe proves or refutes a statement\. As corroboration of fidelity, 50 solved items had their answeredmainproved in this environment from public Lean proofs or recomputed certificates\.

#### Reviews\.

Two AI reviewers per item worked independently: one compared the statement clause by clause with the original source, the other tried to prove or refute it cheaply through formalization loopholes\. After at most two repair rounds \(178 items needed none, 20 one, 2 two\), the verdicts were 139 both passes, 38 with one minor problem, and 23 with two minor problems, with no must\-fix issue; formalization confidence is high for 195 items and medium for 5\.

## Appendix EEvaluation details

Table 7:Per\-run details on HQ\-50 \(50 items per condition, one attempt each; 180\-minute budget\)\. Median min = median attempt wall\-clock minutes; \.lean = attempts that left a formal submission; Open acc\. = open items accepted by both checkers, before review\.#### Isolation\.

Every command of an attempt runs in a freshly built root file system that holds only the attempt’s work directory, read\-only prebuilt dependencies and the Lean toolchain, under its own unprivileged user ID with all capabilities dropped, private namespaces \(network included\) and a seccomp filter that forbids sockets, new namespaces, mounts andptrace\. Per attempt, cgroups enforce 5 CPU cores, 24 GB of memory and 4,096 processes, and the work directory and/tmpmay hold at most 10 GB\. The agent CLI runs in an identical jail with a loopback\-only network whose only exits are a model API gateway \(which routes every request, auxiliary calls included, to the evaluated model, keeps server\-side web tools only in C and removes code execution and remote MCP tools\), an MCP server offeringcheck\_submissionand the retrieval tools of B or C, and, in C only, a web proxy that refuses private addresses\. A 20\-item jail check passes on every node\.

#### Harness and protocols\.

The CLIs run with their own system prompt, tools, context management and default reasoning settings\. Claude Code’s output limit was raised to 128k tokens, since GLM\-5\.3 and Qwen3\.8\-27B often think longer than its default of 32k for unknown models; Qwen3\.8\-27B was served with sglang \(262k\-token context\)\. The task prompt contains the packet README, the problem file, the submission rules and the budget\.check\_submissionapplies the grader’s static rules, compares the definitions and the statement ofmainwith the original, compiles and lists the axioms ofmain, without consulting the reference answer\. Under continuation, a session that ends with at least one minute left and no passing submission is resumed \(claude \-\-resume,codex exec resume\) with a message stating the remaining time, the submission status and concrete tool work to try; three consecutive rounds without a successful model call end the attempt as an agent error, and the models are not told about the stall rule\.

#### Frozen retrieval \(B\)\.

The cutoff, 2026\-01\-06, is the same for all items and announced to the model\. arXiv returns papers first submitted before the cutoff, in their latest pre\-cutoff version; Wikipedia, MathOverflow and Math\.SE return the last pre\-cutoff revision \(for Stack Exchange, only questions, answers and comments posted before the cutoff\); OpenAlex shows only journal or proceedings records, because merged preprint records can carry post\-cutoff abstracts; other sites are refused\. Since search engines index today’s text, every hit is re\-verified against the displayed historical text\.

#### Grading\.

Grading runs on the evaluator’s machine with the evaluator\-only answers\. The compile steps run in a networkless jail whose mounts are read\-only except the step’s build directory, so that code executed at compile time cannot alter the reference, the grader, the answers or Mathlib; the comparison reads the compiled modules rather than parsing source\. Comparator, which exports both projects withlean4exportand replays the full export, is pinned and ported to Lean 4\.33, with a fix that also counts structures referenced by projections, without which its own projection attack would pass\. In C, every fetched URL is normalized \(arXiv ID, DOI, repository, problem page\) and compared with the item’s located solution sources, to flag attempts that fetched one\.

#### Models and cutoffs\.

We used Claude Code and Codex as the agent harness\. Claude Sonnet 5\.5, Kimi\-K3, GLM\-5\.3 and DeepSeek\-V4\.1\-Flash were reached through an Anthropic\-compatible bridge, Qwen3\.8\-27B through sglang’s Messages endpoint, and GPT\-6\.1\-sol and GPT\-6\-luna through a Responses\-API bridge\. Grading used the lineage of each provider for the two OpenAI models and Claude Sonnet 5\.5, and no lineage exclusion for the others, whose own solution credits do not occur in HQ\-50\. Cutoffs were 2026\-06\-30 for the Anthropic and OpenAI models, and the public release dates for the open\-weight models \(Kimi\-K3 2026\-06\-13, Qwen3\.8\-27B 2026\-08\-05, GLM\-5\.3 2026\-08\-25, DeepSeek\-V4\.1\-Flash 2026\-09\-10\); the late release of DeepSeek\-V4\.1\-Flash leaves only 5 clean items\. Table[7](https://arxiv.org/html/2610.37739#A5.T7)gives per\-run details; all attempts used evalkit\-0\.3\.

## Appendix FDataset format and licensing

#### Format\.

Problems in the corpus are unified into a universal JSON Schema that documents every field, a validation report, checksums, an input manifest and other necessary information\. Unknown values are null, and missing data is never converted into invented statements or proofs\. Figure[4](https://arxiv.org/html/2610.37739#A6.F4)shows an abridged problem record\. It keeps the source’s own license wording, an MSC code with its mapping basis, a dated status, and an upstream Lean statement\.

```
{"id": "problem:erdos-7",
 "record_kind": "problem",
 "title": "Erdős #7 · number theory /
     covering systems",
 "problem_statement": "Is there a distinct covering
     system all of whose moduli are odd?",
 "background": "Asked by Erdős and Selfridge ...",
 "field": {"main": "math",
     "slug": "number-theory", ...},
 "msc2020": [{"code": "11",
     "basis": "community-map",
     "evidence": "Inferred from community field:
     number-theory"}],
 "status": "open",
 "source": {"key": "erdos-problems",
     "type": "problem-list",
     "url": "https://www.erdosproblems.com/7",
     "license": "See site; statements paraphrased
     with attribution", ...},
 "provenance": {"imported_at": "2026-09-08",
     "status_as_of": "2026-09-08",
     "has_full_text": true,
     "source_record":
       "https://www.erdosproblems.com/7",
     "sha256": "71fbda4a...698e7172", ...},
 "references": [{"kind": "website",
     "citation":
       "Thomas Bloom (ed.), Erdős Problems #7",
     "url": "https://www.erdosproblems.com/7", ...},
     {"kind": "formalization", ...}, ...],
 "formalizations": [{"language": "Lean 4",
     "format": "source-file",
     "commit": "b82b08fa...",
     "toolchain": "leanprover/lean4:v4.33.1",
     "license": "Apache-2.0; original file ...",
     "has_sorry_or_admit": true,
     "verification_status": "not-checked",
     "code": "... @[category research open, AMS 11]
       theorem erdos_7 : answer(sorry) ↔
         ∃ (C : StrictCoveringSystem ℤ), ∀ i,
           ¬ C.moduli i ≤ Ideal.span {2} ∧
           C.moduli i ≠ ⊤ := by
         sorry ...", ...}],
 "proof": null, "proof_status": "not-recorded",
 "lean4_proof": null,
 "lean4_proof_status": "not-recorded",
 "quality_flags": [
     "lean-statement-from-linked-source-file",
     "formalization-contains-placeholder",
     "formalization-not-compiled-during-export"],
 "schema_version": "1.0.0",
 "snapshot_at": "2026-09-10T06:58:35.349Z", ...}
```

Figure 4:An abridged problem record \(Erdős Problem \#7\) from the OpenFrontiers collection\.
#### Licensing and intended use\.

OpenFrontiers is a mixed\-source dataset and grants no new uniform license over third\-party works\. Each item keeps its source’s reuse wording insource\.licenseand each Lean attachment its own terms informalizations\[\]\.license; missing or ambiguous terms mean that no license was established\. Terms range from CC0 and Apache\-2\.0 to share\-alike \(CC BY\-SA: AIM Problem Lists, Wikipedia\) and non\-commercial ones \(the bundled MSC 2020 taxonomy, CC BY\-NC\-SA 4\.0\), so users who need a permissive subset must filter by source key\. The corpus is intended for locating research problems and evaluating research\-level reasoning, not as permissively licensed training data\.

## Appendix GExclusions and changes

We conduct multiple rounds of benchmark filtering during construction\. For example, re\-reviewing the earlier version removed R09 \(Kourovka 11\.9; the answer was already in the literature\) and R11 \(Kourovka 13\.23; the audit found a non\-inner automorphism of the group constructed in the solution preprint\), and moved four open items resolved in 2026 to Rediscovery\-110: N01 \(Beck–Fiala\), N02 \(Kourovka 20\.76\), N03 \(Tu–Deng\) and N04 \(irrationality ofζ⁡\(5\)\\zeta\(5\)\); IDs are not reused\. The overturn review rejected five new candidates, replaced from the reserve: Erdős \#986 and the rank\-two Poisson conjecture for overlap with admitted items, Vaught’s conjecture because its upstream cardinal form follows trivially from the continuum hypothesis, and two special cases or duplicates of admitted items \(2x,3x∈ℤ⇒x∈ℤ2^\{x\},3^\{x\}\\in\\mathbb\{Z\}\\Rightarrow x\\in\\mathbb\{Z\}; Green’s problem 28\)\. Two items were excluded from HQ\-50 by hand: N03 \(two repair rounds, and the original Tu–Deng wording is known only through later papers\) and N24 \(its reduction rests on a single unconfirmed preprint, and the answered statement has no Lean proof\)\. The open status will be regularly updated over time as more previously open problems are gradually resolved\.

## Appendix HUse of AI assistants

We mainly used generative AI agents to locate candidate problems and solution materials and audit their status, write and review the Lean statements of OpenFrontiers\-Bench \(Section[4\.1](https://arxiv.org/html/2610.37739#S4.SS1)\), help build the evaluation harness, grader, and statistics scripts, and polish this paper\.