Illinois compiled 12 151 open problems and tested whether AI can solve them

A team at the University of Illinois Urbana-Champaign has released OpenFrontiers: a catalog of 12 151 open scientific problems and a benchmark of 200 math problems. The benchmark asks a simple question: can an AI agent rediscover a solution that science has only just learned? The agent sees each problem as it was stated before it was solved. A verifier program, not a human, checks the answer. The result is sobering for those who say "AI is already advancing science": in the no-internet mode, the best agent solved 7 of 40 problems.

A map of the unsolved: what is inside the catalog

Until now, open problems have been scattered across conference lists, prize pages, blogs, and sections of survey papers. Each source has its own rules for how to phrase a problem, how to mark its status, and under what license to store it. The authors merged 71 sources into a single schema, and 62 of them supplied the problem texts themselves. Another 4 751 entries stayed in the catalog as an index, with links only.

What is in the corpus:

• 11 349 entries (93.4%) are mathematics. Physics follows (339), then computer science (285) and machine learning (70). • Most problems fall under number theory (2 867) and geometry and topology (2 371). • The largest sources are TheoremDB (3 909), the American Institute of Mathematics lists (3 470), and the Formal Conjectures project (459). • 65.9% of entries carry a code from the MSC 2020 classification used in mathematics. • Only 1 946 entries, or 16%, have a Lean 4 formulation. Lean is a language in which a proof is written so that a computer checks every step.

The authors do not gloss over problem status. For 46% of entries, the status is marked as undetermined: the source simply does not say whether the problem is solved today. Duplicates were not removed, so as not to rewrite other people's formulations.

How the benchmark works and why a cutoff date is not enough

OpenFrontiers-Bench has two parts. Rediscovery-110 contains 110 problems that were open before 2026 and then received a solution. All evidence of the solutions is dated after January 5, 2026. Open-90 contains 90 problems that are still unsolved. For 85 of the solved problems, there is a verified Lean proof or an exact finite certificate, such as a counterexample recomputed with exact arithmetic.

Every one of the 200 problems has a Lean 4 formulation (version 4.33.1, Mathlib library). Of these, 93 formulations were taken verbatim from Formal Conjectures, 47 were adapted, and 60 were written from scratch. Two reviewers checked each formulation: one compared it against the original statement, and the other tried to break its meaning. Both reviewers were language models, not human mathematicians. No critical issues remained, and for 23 problems both checks raised only minor remarks.

The assembly process turned up an awkward detail. In 55 of the 110 solutions, the authors of the sources credit AI systems with the key mathematics. If a model from the same "lineage" produced the solution, it cannot be called a rediscovery. A cutoff date alone is therefore not enough: the protocol excludes such problems for each model separately. The main mode is closed-book, meaning work without network access.

What the seven agents showed

The agents ran on HQ-50: 50 problems selected for quality, 40 of them solved. There were three conditions: no internet, a frozen copy of a search index, and the live web. Only a Lean proof counted, and it had to be accepted by two independent checker programs in an isolated sandbox.

• Without internet, the agents solved between 0 and 7 of the 40 problems. Mostly these were three problems that humans solved with a short construction. • With the live web, the best result was 27 problems. In almost every case, the agent first found a published solution. • No one closed a genuinely open problem without finding an existing solution. • Strong agents often give up without using their time budget when a problem is too hard.

What this means

Benchmarks such as olympiads and exams, where the answer is known in advance, can no longer tell real research from good search. OpenFrontiers shows how to separate the two: block the network, give the problem in its pre-solution wording, and accept only formally verified results. For labs and investors, this is a useful filter against loud claims about "AI scientists." For researchers, it is a ready-made map of the unsolved and a set of problems where success cannot be written off as leakage from training data.

There are limitations too. The benchmark is almost entirely mathematical, and Lean formulations are available for only a small part of the corpus. The formulations were checked by models themselves, although in two independent passes. The data and the benchmark are published on Hugging Face in the FlippyDora/openfrontiers collection.