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

AI summary

Overview

Research area: AI evaluation and formal mathematics — specifically, benchmarking large language models on research-level (open or recently resolved) mathematical problems using machine-checked Lean 4 proofs.

Technical level: Advanced. The paper assumes familiarity with LLM agent evaluation, proof assistants (Lean 4 / Mathlib), and research-level mathematics; the prose is readable, but the artifacts (pinned Lean environments, dual-checker grading, per-model contamination exclusions) are specialist material.

Scope (one sentence): The paper introduces OpenFrontiers, a 12,151-record cross-disciplinary corpus of open research problems plus a 200-item Lean 4-stated benchmark (OpenFrontiers-Bench) split into 110 recently solved and 90 still-open mathematics problems, and uses it to measure whether seven LLM agents can "rediscover" published solutions under closed-book, frozen-retrieval, and live-web conditions.

What This Paper Is About

Evaluating LLMs on research-level problems is hard because a research problem, unlike an exam question, has no reference answer at the time it is posed, and problems that later get solved can leak into training data or be looked up online. The authors build a large, provenance-tracked collection of open problems, then carve out a rigorously graded subset of 200 mathematics problems whose statements have been formalized in Lean 4 — 110 that were open into 2026 and now have a located solution, and 90 that are still open. The goal is to test whether models can genuinely rediscover solutions rather than retrieve them, and to establish an infrastructure for tracking progress on problems that remain unsolved.

Key Contributions

1. An open-problems corpus. 12,151 problem records drawn from 62 contributing source collections (71 registered), spanning 10 top-level fields and 32 sub-fields, with verbatim statements, per-record provenance and license text, status labels, MSC 2020 codes (on 65.9% of records) and Lean 4 attachments (on 1,946 records), plus 4,751 catalogue items that carry pointers but no statements.

2. OpenFrontiers-Bench. 200 research-level mathematics problems, each with a Lean 4 statement that compiles in a pinned environment (Lean 4.33.1, Mathlib 0df444a, Formal Conjectures 89294ea) and has passed automated probes plus two independent reviews: Rediscovery-110 (problems open into 2026 with a located solution) and Open-90 (still open), with per-item date and AI-disclosure audits and a 50-item high-quality subset, HQ-50.

3. An evaluation protocol. Three access conditions (closed-book, frozen retrieval over content public before 2026-01-06, and live web) run inside an isolated sandbox, with grading by two independent Lean checkers (including leanprover/comparator), and per-model lineage and cutoff exclusions to control contamination.

4. An empirical study of seven LLM agents. Results on the 40 solved items of HQ-50 showing that closed-book rediscovery is rare (at most 7 of 40) and that live-web success mostly reflects retrieval of published solutions.

Main Findings

• Closed-book rediscovery is rare. Under the native protocol agents solve 0–3 of the 40 solved items; under the continuation protocol 0–7. Continuation helps 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 scores 3/30, 4/15 and 2/15), while open-weight models change by at most two items.

• A handful of easy items dominate. Across the 14 runs (7 models × 2 protocols), the 53 closed-book and frozen-retrieval solves fall on only eight items, and the three importance-3 items (R01, R04, R29), all solved by humans through short constructions, account for 44 of them. Of the 21 importance-5 items, only one (N28, settled by a finite certificate) was solved, once.

• Frozen retrieval does not help systematically. The frozen-retrieval condition exceeds closed-book in two runs (by one and two items) and trails it in three — consistent with a search snapshot that predates every solution.

• Live web measures retrieval, not reasoning. Agents solve 1–27 items under live web, but 167 of the 181 live-web solves came from attempts that fetched a located solution source (preprint, repository or problem page), often with a public Lean proof to adapt. 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 closed-book and frozen-retrieval attempts but in 11 of the 14 live-web runs, each after fetching the problem page or its forum thread.

• Even live web is not saturated. No model solved all 40 already-solved problems even with web access, leaving room to improve information search and retrieval.

• Agents give up early. Natively, Claude Sonnet 5.5 and the GPT models end most attempts within minutes (median 0.3–4.1 of 180 minutes), whereas Qwen3.8-27B mostly runs until the limit; under continuation most Claude Sonnet 5.5 attempts stall, repeating that no progress is possible.

• AI systems are already part of the solution record. For 55 of the 110 Rediscovery-110 items the solution materials credit an AI system with the key mathematics (OpenAI models 46, Anthropic 5, Google 4, Harmonic 3, with several items naming more than one), concentrated after June; 36 disclose assistance with a human-attributed solution and 19 disclose none.

• Contamination control requires more than a date cutoff. Because a model whose lineage produced a solution has effectively seen it, and most checked solutions have a public Lean proof, the protocol excludes such items per model and makes closed-book the main condition; at a 2026-06-30 cutoff the clean subset holds 15 items for OpenAI models, 30 for Anthropic and 32 for unrelated models.

• No open problem was solved without a retrieved solution. The authors report that no Open-90 item was solved by an agent without one, and that a kernel-accepted solution would be new mathematics — but a statement error is the likelier explanation, so any acceptance triggers review before a claim.

Methodology in Plain English

Building the corpus. The authors registered 71 sources of open problems — curated lists, workshop reports, survey sections, prize pages, blogs, Wikipedia subject lists and structured databases — and wrote deterministic fetchers that store file checksums. Everything goes into one schema: the problem's exact original wording, its field, MSC 2020 subject codes, a status label, source and license, references, provenance dates, quality flags, Lean attachments and notes on partial progress (present in 94.9% of records). No deduplication by statement was performed, to preserve the original problems.

Status honesty. Only 50.7% of records are labeled open; 46.0% are labeled unassessed, because historical workshop lists and backlog items assert no current status. Labels record the source's claim as of a stored date, not a local verification, and source-side "solved" claims are kept verbatim in a separate field.

Turning the corpus into a test. Solved candidates came from status changes between successive versions of source lists, 2026 arXiv preprints, and public releases of AI-produced solutions; nine search sweeps produced 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 tried to overturn each new item and rejected 5. Admission required that the problem was demonstrably public before resolution, that the solution settles it with the same quantifiers and scope, that no earlier solution existed, and that it was not a restatement, a withdrawn paper, or an announcement without proof.

Formalizing the statements. Each item targets a single theorem main; yes/no questions are written so a solver must supply the answer and the proof. 93 statements are verbatim from Formal Conjectures, 47 adapted, 60 newly written. Upstream problem files are kept out of the build because at least 35 of them record a solved item's answer. Two reviewers checked each statement — one for fidelity, one attacking its Lean semantics — with up to two repair rounds (139 items ok+ok, 38 minor+ok, 23 minor+minor, no must-fix issues), and comments hinting at answers were rewritten in 47 files. The reviews were run by AI agents.

Selecting HQ-50. Hard filters keep well-formalized, cleanly reviewed statements; 55 solved and 48 open items qualified. A scoring step then ranks them 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, 8 per area among solved items, and at most 21 items whose key mathematics came from OpenAI models).

Running the evaluation. Each attempt gets a fresh sandbox containing only that problem's Lean workspace with prebuilt Mathlib, plus Python with numpy, sympy and mpmath; every command runs without network under an unprivileged user with namespaces, seccomp and cgroup limits, and the problem file carries an opaque ID with status-revealing lines removed. Retrieval happens outside the sandbox and is logged. Each attempt has 3 hours of wall-clock time, 5 CPU cores and 24 GB of memory, one attempt per item per condition, using vendor agent CLIs (Claude Code, Codex) behind a gateway. A submission counts as solved only if both Lean checkers accept it with the reference answer, allowing only propext, Classical.choice and Quot.sound; natural-language proofs and certificates are reported separately, and there is no model-as-judge. The grader was self-tested with accept/reject cases (including a compile-time file write that passes keyword bans) and comparator's 16 official regression attacks.

Why This Matters

Impact on research. The paper makes a case that progress on genuinely open science cannot be measured with exam-style benchmarks whose answers were known to their authors, and that contamination control must account for model lineage, not just publication dates. It also documents that over half of a curated set of 2026 solutions involved AI systems, which reframes what "measuring AI research ability" even means. By publishing date-anchored, formally graded items, it gives the field a reusable instrument rather than a one-off leaderboard.

Real-world applications (as implications of the resource):

• Benchmarking research agents. Labs can plug new prover or agent systems into the same three-condition harness to compare against a fixed historical snapshot.
• Contamination auditing for model releases. The per-model lineage and cutoff exclusion logic offers a template for evaluating models on material published after their training data.
• Curating open-problem infrastructure. The provenance-first schema, status policy (including the deliberate unassessed label) and license tracking are reusable for building problem collections in other fields.
• Tracking human–AI attribution in mathematics. The three-way disclosure classification (AI-produced key mathematics, AI assistance, none disclosed) provides a vocabulary for recording how new results are produced.

Industry relevance. The finding that frontier agents stop within minutes unless resumed — and that resumption materially raises solve counts — is directly actionable for anyone deploying long-horizon reasoning agents. The retrieval findings also matter for search-and-agent product design: live-web success is dominated by locating the published answer, so retrieval quality, and the ability to keep working after a search fails, are separate engineering problems.

Future Directions

• Better harnesses against early stopping. The conclusion explicitly calls for harnesses that keep models thinking longer rather than abandoning a problem — the continuation protocol raised solve counts for every model that stopped earliest, but Claude Sonnet 5.5 attempts mostly stalled while repeating that no progress was possible.

• Extending the formal fragment. The corpus is largely informal: only 16.0% of records carry a Lean 4 statement, and 1,562 of the 1,961 attachments are flagged as containing a placeholder (sorry/admit). Formalizing more of the 12,151 records, and beyond mathematics (the 93.4% mathematics share leaves physics, computer science and other fields thinly covered), is an open engineering problem.

• Widening Rediscovery-110 beyond 110 items. The solved track is currently small enough that eight items account for almost all closed-book solves, and HQ-50 is only 40 solved plus 10 open items; a larger pool of high-importance post-cutoff items would reduce the influence of a few short-construction outliers.

• Clarifying AI attribution and open-status verifiability. The paper notes that "none disclosed" does not imply no AI was used, and that an open record has not been locally verified to be open; better attribution practice and continuous status re-checking — including the review gate triggered by any kernel-accepted Open-90 solution — are needed for the benchmark to stay valid over time.

Target Audience

Researchers and engineers working on LLM reasoning, AI-for-mathematics and formal verification; benchmark designers who need contamination-resistant, machine-graded evaluation; developers building long-horizon agent harnesses; and mathematicians or curators interested in structured, provenance-tracked open-problem infrastructure. Readers without background in Lean 4 or agent evaluation will find the conceptual argument accessible but the protocol sections dense.

Authors’ 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 introduce OpenFrontiers, 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.