OpenFrontiers: A Collection of Open Research Problems and a Benchmark for Scientific Rediscovery
Source
arxiv.org
Author
Jiarui Yao, Ruida Wang, Tong Zhang
Date
Why it matters
Provides a Lean-verified, contamination-aware way to measure whether agents can solve research-level problems. Early results show closed-book rediscovery is rare, which tempers capability claims.
Key takeaways · AI-distilled
OpenFrontiers pairs a corpus of 12,151 open research problems, recording statements, context windowThe maximum amount of text a model can consider at once — its working memory for the current conversation or task.Full definition → and progress, with a 200-problem math benchmarkA standard public test set for comparing AI models — the shared scoreboards behind every "model X beats model Y" claim.Full definition →: 110 problems resolved in 2026 and 90 still open.
Each benchmark problem has a Lean 4 statement checked by automated probes and two independent reviews, and submitted proofs are graded by two independent checkers in an isolated sandboxAn isolated environment where AI-generated code or agent actions run without being able to touch anything real.Full definition →.
Seven LLMA large language model — the neural network behind tools like Claude and ChatGPT, trained on huge amounts of text to predict what comes next.Full definition → agents were tested on the HQ-50 subset under closed-book, frozen-retrieval and live-web conditions. Closed-book, they rediscovered at most 7 of 40 resolved problems; live-web success mostly reflected retrieving published solutions.
Terms in this piece · Glossary
benchmark — A standard public test set for comparing AI models — the shared scoreboards behind every "model X beats model Y" claim.
LLM — A large language model — the neural network behind tools like Claude and ChatGPT, trained on huge amounts of text to predict what comes next.
context window — The maximum amount of text a model can consider at once — its working memory for the current conversation or task.
sandbox — An isolated environment where AI-generated code or agent actions run without being able to touch anything real.
articleThe Problem Is the Problem: Towards Scalable Mathematical DiscoveryZeyu Zheng, Shengtong Zhang, Jeremy Avigad, Prasad Tetali, Sean Welleck
articleRePro: Proof-Verified Benchmark Rewriting for Reliable Evaluation of LLM Mathematical Problem SolvingXiyuan Zhou, Zhuoqi Li, Xinlei Wang, Yirui He, Yuhao Wu, Yuheng Cheng, Yan Xu, Junhua Zhao, Jinjin Gu
blogThe Epoch Brief - July 31, 2026Elliot Stewart