OpenFrontiers: A Collection of Open Research Problems and a Benchmark for Scientific Rediscovery
Jiarui Yao, Ruida Wang, Tong Zhang
cs.AI
Oct 27, 2026 · v1
cs.CL cs.LG
TL;DR
Benchmark of 200 research-level math problems with checked Lean 4 statements; LLM agent proofs are graded by two independent Lean checkers with Mathlib.
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.
Problem
No comprehensive collection of open research problems exists, and grading LLMs on research-level problems is hard because such problems lack reference answers and solutions may leak into training data.
Approach
The authors build a corpus of 12,151 open-problem records from 62 sources, 1,946 of which carry Lean 4 statements. From it they curate OpenFrontiers-Bench: 200 mathematics problems with compiled, reviewed Lean 4 statements, split into 110 problems resolved in 2026 and 90 still open. They also define an HQ-50 subset. Agents work in sandboxed Lean workspaces with prebuilt Mathlib under closed-book, frozen-retrieval and live-web conditions, and only proofs accepted by two independent Lean checkers count.
Results
Seven LLM agents rarely rediscover solutions closed-book, solving at most 7 of the 40 resolved HQ-50 items. Live-web success mostly reflects retrieval of published solutions, and no open problems were solved under the native protocol.
| Model | Closed-book | Frozen retrieval | Live web |
|---|
| Claude Sonnet 5.5 | 4 | 3 | 24 |
| GPT-6.1-sol | 7 | 5 | 27 |
| Kimi-K3 | 3 | 2 | 15 |
| DeepSeek-V4.1-Flash | 3 | 3 | 15 |
Solved items of 40 resolved HQ-50 problems (continuation protocol, all items)
