OpenFrontiers: A Collection of Open Research Problems and a Benchmark for Scientific Rediscovery

• Research problems lack a known reference answer, while open-problem statements and status are dispersed across sources with differing conventions and licensing.Tasks must be time-anchored so models receive formulations public before resolution and located solutions remain evaluator-only.Source: §1 · p. 1
• The corpus records 12,151 problems from 62 collections across 10 fields, with Lean 4 statements attached to 1,946 records.Uncertain status is labeled unassessed rather than promoted to open.Source: §1 · p. 1
• OpenFrontiers-Bench contains 200 research-level mathematics problems with compiling Lean 4 statements, automated verifications, and two independent reviews.Rediscovery-110 comprises 110 problems resolved in 2026; Open-90 contains 90 still-open problems.Source: §1 · p. 2
• Closed-book agents solve 0–7 of 40 solved items, while live-web successes mostly follow retrieval of published solutions.The evaluation covers seven agents on HQ-50 and accepts only Lean proofs checked by two independent checkers.Source: §1 · p. 2
• The evaluation protocol tests three access conditions in an isolated sandbox and grades proofs with two independent Lean checkers.Items are excluded per model when its lineage produced the key mathematics, and closed-book is the main condition.Source: §1 · p. 2

Benchmarks for mathematical and scientific reasoning

• Existing benchmarks often grade final answers or unittested programs, whereas OpenFrontiers dates actually open questions by located solution evidence and admits expert-reviewed proofs.Several existing sets use held-out questions or refresh items from new competitions and papers.Source: §2 · pp. 2–3

Proof-level and formal evaluation

• Formal benchmarks use proof assistants such as Lean 4, while OpenFrontiers writes and reviews pinned statements because only 16.0% of corpus records carry Lean 4 statements.Its protocol grades solutions with two independent Lean checkers.Source: §2 · p. 3

Open-problem collections

• Open-problem lists and databases are often bound to one community, format, and notion of openness, and their statuses can drift as problems are solved.OpenFrontiers registers sources under one schema with verbatim statements, per-record provenance, license text, and an unassessed status for uncertainty.Source: §2 · p. 3

3 The OpenFrontiers Corpus

• The corpus snapshot contains 12,151 problem records from 62 collections in 10 fields, plus 4,751 catalogue items, and does not deduplicate statements.Status filtering is tied to a particular date because open problems may be solved over time.Source: §3 · p. 3

3.1 Sources and acquisition

• A 71-source registry includes 62 collections contributing records, with the remainder providing catalogue pointers; deterministic fetchers and a unified schema preserve provenance and verbatim statements.The schema also stores source and license wording, status dates, quality flags, Lean attachments, and partial-progress context.Source: §3.1 · pp. 3–4
• Unassessed is the default when sources do not assert current status, and an open label records the source's claim rather than a locally verified status.Source-side solved or verified labels are retained as claims while the original statement is kept.Source: §3.1 · p. 4

3.2 Corpus statistics

• Mathematics contributes 11,349 records (93.4%); 50.7% of all records are labeled open, 46.0% unassessed, and only 41 solved.TheoremDB, ICM Conjectures, and Erdős Problems supply most open records; many unassessed records come from AIMPL, TheoremDB, and Formal Conjectures.Source: §3.2 · p. 4
• Of 1,946 records with Lean statements, 1,562 carry a placeholder flag and none has a canonical accepted proof or locally verified Lean proof.Lean statements are display-only in the corpus; formal checking occurs in the platform sandbox and benchmark grader.Source: §3.2 · p. 4, §3.1 · p. 4
• Among 3,389 records with known posed years, decade counts rise from 260 in the 1970s to 869 in the 2010s and 878 in the 2020s.Figure 2c omits 91 records posed before 1950.Source: §3.2 · p. 5, Figure 2 · p. 5

4 OpenFrontiers-Bench: A Retrospective Rediscovery Benchmark

• OpenFrontiers-Bench contains 200 research-level mathematics problems with checked Lean 4 statements; Rediscovery-110 has 110 resolved items and Open-90 has 90 still open at status check.HQ-50 is the 50-item subset evaluated in Section 5.Source: §4 · p. 5

4.1 Construction

• Rediscovery-110 admits problems posed publicly before resolution, with matching quantifiers and scope, no located earlier solution, and solution evidence dated after 2026-01-05.Its tiers include 85 items with independently recomputed finite certificates or compiled Lean proofs, 21 corroborated but not re-verified solutions, and 4 claims pending verification.Source: §4.1 · p. 5
• The benchmark statements use a pinned Lean environment, exclude upstream problem files that may reveal answers, and are checked by two independent reviewers for source fidelity and Lean semantics.The 200 statements passed automated checks, and no must-fix issue remained after review.Source: §4.1 · pp. 5–6

4.2 Rediscovery-110 and Open-90

• Rediscovery-110 spans nine areas; 75 of its 85 Tier A items rely on a full Lean proof, while the other 10 rely on an exact certificate.Group theory and number theory lead with 19 items each.Source: §4.2 · p. 6
• Solution materials credit AI with key mathematics for 55 of 110 resolved items; 41 of the 76 items with post-June solution evidence fall in that group.The protocol excludes items whose solution lineage matches a model, because a post-cutoff solution date alone does not ensure the model has not seen it.Source: §4.2 · p. 6
• Open-90 includes 26 items retained from an earlier split and 64 additions; 38 have a direction settled by a finite object, and accepted solutions trigger review because statement error is considered likelier than new mathematics.The authors recently checked item status to keep the split relatively reliable.Source: §4.2 · p. 6

4.3 HQ-50

• HQ-50 selects 40 solved and 10 open items through quality filters, ranking, and caps on shared sources, problem families, areas, and other item groups.All 50 statements were rechecked for open status during the agent evaluation.Source: §4.3 · pp. 6–7

5.1 Access conditions and environment

• Attempts run in fresh, network-isolated sandboxes; closed-book uses no retrieval, frozen retrieval is limited to pre-cutoff sources, and live web logs all URLs as a leakage reference.The frozen snapshot predates every located solution, while live web mainly measures information retrieval.Source: §5.1 · p. 7

5.2 Grading

• A solution counts only when the Lean proof with the reference answer is accepted by both independent checkers; checker disagreement counts as unsolved.The main metric counts formal proofs, not accompanying natural-language proofs or certificates.Source: §5.2 · p. 7

5.3 Models and harness

• Seven agents receive one attempt per item and condition, with three hours, five CPU cores, and 24 GB of memory; continuation resumes the same session when an agent stops early.Agents run in sandboxed vendor CLIs with the model and server-side tools controlled by the harness.Source: §5.3 · p. 7

5.4 Results

• Across 14 runs, 53 closed-book and frozen-retrieval solves fell on eight items, and three short-construction items accounted for 44 solves.The 21 importance-5 items produced only one solve, once.Source: §5.4 · p. 7
• Closed-book agents solved 0–7 of 40 solved items; live web yielded 1–27 items, with 167 of 181 C solves following a located-solution fetch.Frozen retrieval did not help systematically: it exceeded closed-book in two runs and trailed it in three.Source: §5.4 · pp. 7–8, Table 3 · p. 8
• Native runs often ended within minutes for Claude Sonnet 5.5 and GPT models, whereas continuation made most agents use nearly the full budget and yielded more solved problems.Most Claude Sonnet 5.5 continuation attempts stalled after repeated rounds without tool use.Source: §5.4 · p. 8

6 Conclusion

• Closed-book rediscovery was rare across seven LLM agents, and live-web successes mostly retrieved published solutions.Even with Internet access, models did not correctly resolve all already solved problems.Source: §6 · p. 8
• OpenFrontiers comprises 12,151 research-problem records from 62 collections across 10 fields and a 200-problem mathematics benchmark with checked Lean 4 statements.The benchmark was graded by two independent Lean checkers under three access conditions.Source: §6 · p. 8
• Models sometimes solved open problems within a fixed budget but tended to give up early before making substantive progress.The authors identify deeper, longer-running harnesses as a development need.Source: §6 · p. 8
• The authors conclude that OpenFrontiers exposes room to improve information search and retrieval and the ability to explore open problems thoroughly.Source: §6 · p. 8

A Benchmark item lists

• Tables 4 and 5 list all 200 benchmark items, marking the 50 HQ-50 items with a bullet after each ID.The displayed problem titles are curator titles, not the text shown to models, which receive the Lean file from the solver packet.Source: A Benchmark item lists · pp. 11–12
• For Rediscovery-110, the tables give evidence tier, solution-evidence date, and AI disclosure class; for Open-90, they give implementation priority and whether one direction is settled by a finite object.The AI disclosure classes are AI, assist, and none; “none” means no AI use was disclosed in reviewed materials, not that none occurred. Open-90 priority is pilot, core, or stretch, and is not a difficulty estimate.Source: A Benchmark item lists · p. 12
• The item list spans curator-grouped research areas and includes problems such as Beck–Fiala discrepancy and finite-group questions.Areas are curator groupings into ten areas; solution URLs, split groups, Lean declaration names, scope differences, review verdicts, and pending gates are retained in package files.Source: A Benchmark item lists · pp. 12–13
• Resolved-item examples range from the Tu–Deng conjecture and irrationality of ζ(5) to the Navier–Stokes Millennium Problem and soficity of groups.The list also includes graph-theoretic, algebraic, geometric, and combinatorial problems.Source: A Benchmark item lists · p. 13
• Rediscovery-110 contains 110 items selected in three rounds; its caption marks HQ-50 membership and defines the tier, solution-date, and disclosure-class fields.The caption identifies R, E, and N as selection rounds with different cutoff dates; AI denotes disclosure class.Source: Table 4 · p. 14
• Open-item examples include Lehmer’s totient problem, the Scholz addition chain conjecture, the Erdős Matching Conjecture, and the prime power conjecture for finite projective spaces.The listed problems also span graph theory, geometry, combinatorics, and analysis.Source: A Benchmark item lists · p. 14

• Examples include the maximum number of mutually unbiased bases in C6, Borsuk’s partition problem in dimension 4, Ryser’s conjecture, and the Kummer–Vandiver conjecture.Source: A Benchmark item lists · p. 14
• Other listed questions span additive combinatorics and graph theory, including Sidon sets, even-cycle Turán bounds, Ramsey numbers, and the Kővári–Sós–Turán bound.Source: A Benchmark item lists · p. 15
• Open-90 lists 90 items; • marks HQ-50 membership, “Prio.” denotes implementation priority, and “Cert.” indicates one direction settled by a finite object.Source: Table 5 · p. 15

B Source collections

• 62 source collections contribute records, but counts are source records rather than deduplicated conjectures; some catalogue-only sources contribute pointers rather than statements.The registry records shortened reuse notes, with full wording carried on each item.Source: B Source collections · p. 16, Table 6 · p. 17

C Curation rubric

• Candidates must trace to a public research question, match the resolved question’s scope, and meet timing, proof, and problem-family deduplication rules.Open items must be precisely posed, open in both directions at status check, and not duplicates or special cases.Source: C Curation rubric · pp. 17–18
• Resolved items are assigned evidence tiers: 85 Tier A items have independently checked Lean proofs or exact certificates, while 21 Tier B and 4 Tier C items have less complete verification.Four conditional Tier A items are excluded from HQ-50.Source: C Curation rubric · p. 18
• Curators score importance, clarity, formalization cost, and proof cost ordinally; scores are not combined except in HQ-50 ranking.Importance scores average 4.15 for solved items and 4.37 for open items.Source: C Curation rubric · p. 18
• Solution dates use the earliest located public evidence, but the audit was not an exhaustive priority search.A later publication, simplification, or formalization does not reset the stored date.Source: C Curation rubric · p. 18
• HQ-50 applies quality filters and a ranked selection, while item caps constrain representation across sources, families, areas, and model lineages.Selection also binds items sharing a solution paper, public release, or source into split groups.Source: C Curation rubric · pp. 18–19

D Lean statements and checks

• Corpus Lean attachments are display-only and are not proof-checked at export, whereas community submissions are checked separately in a fresh networkless container.A successful community check attaches a receipt but does not change problem status.Source: D Lean statements and checks · p. 19
• All 200 benchmark statements form a pinned Lean 4.33.1 project, and a clean build succeeds.Each file declares one theorem; automated probes test appropriate answers without proving or refuting statements.Source: D Lean statements and checks · p. 19
• Two independent AI reviews compare each statement with its source and test for formalization loopholes; 139 items passed both reviews.After up to two repair rounds, no item had a must-fix issue; confidence was high for 195 items and medium for five.Source: D Lean statements and checks · p. 19

E Evaluation details

• Each attempt runs in a fresh isolated environment with resource limits, and the agent’s only network exits are restricted to approved model, submission, and retrieval services.A 20-item jail check passes on every node.Source: E Evaluation details · p. 19
• The harness applies static submission checks and resumes unfinished sessions with at least one minute remaining, ending attempts after three rounds without a successful model call.The checks compare the submitted theorem with the original and compile it without consulting the reference answer.Source: E Evaluation details · p. 19
• Frozen retrieval uses a shared 2026-01-06 cutoff and verifies search hits against historical versions; some sites and post-cutoff text are excluded.arXiv, Wikipedia, MathOverflow, and Math.SE return pre-cutoff material under the stated rules.Source: E Evaluation details · pp. 19–20
• Table 7 reports one attempt per item per condition under a 180-minute budget, including median minutes, formal submissions, and open items accepted by both checkers.Compare these measures across conditions; the caption does not state the outcome of that comparison.Source: Table 7 · p. 20
• Model lineages and release dates determine clean-item exclusions, and DeepSeek-V4.1-Flash has only five clean items because of its late release.The reported runs used evalkit-0.3.Source: E Evaluation details · pp. 20–21

F Dataset format and licensing

• Corpus records use a universal JSON Schema with validation information, checksums, and an input manifest; unknown values remain null rather than becoming invented statements or proofs.Records retain source license wording, dated status, MSC mapping basis, and upstream Lean statements.Source: F Dataset format and licensing · p. 21
• OpenFrontiers grants no uniform license over third-party works, and each item retains its source reuse wording and formalization terms.Missing or ambiguous terms mean no license was established.Source: F Dataset format and licensing · p. 21
• Users seeking a permissively licensed subset must filter by source key; the corpus is intended for locating research problems and evaluation, not permissively licensed training data.Source: F Dataset format and licensing · p. 21

G Exclusions and changes

• Four problems resolved in 2026 were moved into Rediscovery-110 after review.The review also removed R09 because its answer was already in the literature and R11 after an audit found a non-inner automorphism in the solution preprint.Source: G Exclusions and changes · p. 21
• The overturn review rejected five new candidates, replacing them from the reserve: Erdős #986 and the rank-two Poisson conjecture overlapped admitted items, Vaught’s upstream cardinal form followed trivially from the continuum hypothesis, and two others were special cases or duplicates.Source: G Exclusions and changes · p. 21
• N03 and N24 were manually excluded from HQ-50 over wording and evidence concerns.N03 needed two repair rounds and its original wording is known only through later papers; N24’s reduction rests on one unconfirmed preprint, and the answered statement has no Lean proof.Source: G Exclusions and changes · p. 21
• Open-status labels will be updated as more previously open problems are resolved.Source: G Exclusions and changes · p. 21

H Use of AI assistants

• AI agents helped locate candidate problems and solution materials and audit their status.Source: H Use of AI assistants · p. 21
• AI agents helped write and review the Lean statements for OpenFrontiers-Bench.Source: H Use of AI assistants · p. 21
• AI agents helped build the evaluation harness, grader, and statistics scripts, and polish the paper.Source: H Use of AI assistants · p. 21