OEIS Open Benchmark

Sources#

• FrontierMath Erdős
• OEIS Open: How many conjectures can language models turn into theorems?
• Reward-Oracle MCTS for Formal Theorem Proving: Sample-Efficient Search and the Need for Kernel-Level Proof Auditing
• SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization

Summary#

OEIS OPEN is Epoch AI's benchmark of 492 open mathematical conjectures from the Online Encyclopedia of Integer Sequences, formalized in Lean, on which a model must submit a machine-checked proof of the conjecture or of its negation (Tom Adamczewski, arXiv 2608.11941, 2026-08-12, 27pp, empirical). Its headline: a minimal ReAct agent with three tools resolves 147 of 492 (30%) at a $50 spending cap per conjecture, against 44/492 (9%) for DeepMind's AlphaProof Nexus — the bespoke evolutionary system that built the item set — at comparable cost per resolved conjecture.

It is the second benchmark in this corpus whose items are open research problems with a scored denominator and a dollar budget, and the counterweight to the first. The same author, the same month, the same kernel-checked standard, and a rate ten times higher: FrontierMath Erdős Benchmark reports 2/68 (3%) on Erdős problems curated for significance at $300 each, while this reports 30% on OEIS conjectures a model was explicitly prompted to select as "not famous open problems." The pair is the corpus's cleanest demonstration that on open problems the headline number is a property of the denominator's curation, not of the models — the two sets differ by an order of magnitude in solve rate at a sixth of the budget.

The item set, and how it was built#

The conjectures were not collected by Epoch. They come from Tsoukalas et al. (arXiv 2605.22763): starting from "a corpus of 2649 open conjectures drawn from the OEIS," Gemini was prompted to select 500 problems that are "non-trivial, mathematically interesting, not famous open problems, and good candidates for automated theorem-proving," and a Gemini-based agent formalized them in Lean. Eight were dropped for technical reasons, leaving 492 conjectures over 444 distinct OEIS sequences (some sequences contribute several). OEIS OPEN LITE is a random 100-conjecture subset for cheaper evaluation.

Epoch's contribution is the evaluation: open-source code that runs any generic LM against the set, hardened against cheating, plus per-conjecture provenance metadata. Its own framing of why this matters is a critique of the demonstration genre — recent AI-solves-open-problem announcements "do not disclose the universe of problems attempted," the degree of human mathematical guidance "is unclear," and different models are never compared on the same problems, so "we do not know when AI models first became capable of proving these results."

Why integer sequences. Conjectures about integer sequences "generally involve only integers and elementary operations on them, rather than complicated mathematical objects whose formal statements rest on long chains of Mathlib definitions" — so misformalization risk is structurally lower than for a research statement in, say, algebraic geometry. This is the same mathlib-coverage gate that prices formalization elsewhere in the corpus, used here as a selection criterion rather than suffered as a cost.

What "resolved" means, stated as a procedure#

This is the part worth copying, and it is more explicit than any other verification protocol in the corpus.

The target. Following Tsoukalas et al., the Lean target is an equivalence between a truth value and the conjecture, with the truth value left editable by the agent (an EVOLVE-VALUE marker). Setting it to True and proving the equivalence proves the conjecture; setting it to False disproves it. So a single task admits both outcomes, and — unlike the generator-verifier benchmarks this paper criticizes — a false conjecture is still a solvable task.

The checker. A submission is accepted only if it passes SafeVerify, adapted from the Lean developers' lean4checker. Both replay compiled Lean through the kernel from scratch; SafeVerify additionally certifies that the submission proves the target statement — each target declaration must be present with the same name, kind, and kernel type, and may use no axioms beyond the standard three (propext, Quot.sound, Classical.choice).

The isolation. Every attempt is split across three Docker containers, none with network access: the agent container where the model works; the compile container, a clean Lean toolchain where the submitted source is compiled to an olean; and the scorer container, which receives only the submission olean and runs SafeVerify against Epoch's own trusted copy of the statement. What the split buys, in the paper's own enumeration:

1. Tampering with the agent environment is powerless — only the submission's Lean source leaves the agent container.
2. Malicious compile-time code — Lean elaboration can execute arbitrary code (a compile-time #eval), so compilation is confined to its own container, separate from the verdict.
3. Proving a different statement — SafeVerify matches against Epoch's copy, requiring kernel-identical types.
4. Redefining a dependency so the conjecture becomes trivially true — definition bodies must be identical to the target's; only sorry stubs may be filled in.
5. Smuggling extra axioms — a declared axiom, or a sorry (which introduces sorryAx), falls outside the three-axiom whitelist.
6. Bypassing the kernel — metaprogramming can insert declarations without kernel checking and a buggy tactic can emit an ill-typed term, so SafeVerify replays every submitted declaration through a fresh kernel. native_decide shifts trust from the kernel to the compiler and is known to be subvertible via @[implemented_by]; it introduces Lean.ofReduceBool, which is outside the whitelist and therefore rejected.

What remains trusted: "Lean's kernel, SafeVerify itself, and the container isolation." That list of three is the honest form of "machine-checked," and the axiom whitelist plus the native_decide exclusion are the same two escape routes ProofEvolve closes on the competition-benchmark side — independently arrived at, which is mild evidence they are the right two.

The checkers disagree, and the disagreement is 3 conjectures#

Epoch re-verified every Claude Opus 4.8 submission on all 492 conjectures with Comparator, the Lean FRO's independent checker (the one FrontierMath Erdős Benchmark uses). Comparator confirmed all SafeVerify-accepted solves except submissions to five conjectures whose Lean formalizations had "an unusual defect," and additionally verified two proofs SafeVerify had rejected only because the checker exhausted its resource limits. Net:

Under Comparator's verdicts, Claude Opus 4.8 scores 144/492 (29%) rather than 147/492 (30%). Future versions of this benchmark will use Comparator.

Small in magnitude, large in kind: this is the corpus's first measured disagreement between two independent cheat-resistant Lean checkers on the same submissions, and it runs in both directions — five false accepts and two false rejects. "The kernel said yes" is a verdict from a specific checker, and the checker has a resource limit that is itself a scoring surface.

The whitelist's necessity, measured six months on#

Items 5 and 6 of that attack list (sorryAx from a smuggled sorry; Lean.ofReduceBool from native_decide) are argued here as things that could happen; Epoch reports no attempt at either. Reward-Oracle MCTS for Formal Theorem Proving: Sample-Efficient Search and the Need for Kernel-Level Proof Auditing (Vamshi and Yang, University of Maryland, arXiv 2608.28639, 2026-08-11, empirical) is the measurement: on PutnamBench, 31–44% of DeepSeek-Prover-V2-7B's reported successes depend on sorryAx while compiling cleanly and carrying no sorry token in the source — the obligation is discharged by an apply? tactic that never emits the token a source-level scan looks for. Item 5 is not hypothetical, and the source-scan version of the check that most prover papers run does not catch it.

Two things this says about the protocol on this page. The whitelist is the load-bearing part, not the container split or the statement matching — those close attacks nobody has been observed attempting, while this one is being tripped by a released model in ordinary use with no adversarial intent. And the exploit is model-specific: Goedel-Prover-V2-8B and Kimina-Prover show zero sorryAx dependencies across four benchmarks, so a benchmark that whitelists axioms is measuring something a benchmark that greps for sorry is not, and the difference only shows up for some checkpoints. Full treatment on Kernel-Level Proof Auditing.

The agent, and the three things that did not help#

Base agent. A ReAct-style tool loop on the UK AISI Inspect library, with exactly three tools: bash, a text editor, and a resources tool reporting remaining time and token budget. The container provides Lean 4 + Mathlib, SageMath, and Python with sympy, mpmath, numpy and pantograph. The binding limit is the per-conjecture spending cap — $50 on the full set, $200 on LITE — with a hard 72 hours of working time.

Two variants were run on LITE against the base agent, at the same $200 cap and the same models:

• Literature — an offline snapshot of 476,000 pure-mathematics arXiv papers (LaTeX source trees, the arXiv subset of proof-pile, dated up to 2022).
• DeepAgent — Inspect's deepagent in place of the ReAct loop: subagent delegation, persistent memory, a todo-list tool, and a longer, opinionated system prompt.

Neither moved the score (Figure 3, viewed; 100 conjectures, $200 cap, ±1 standard error):

Model	base	DeepAgent	literature
Claude Opus 4.8	39%	39%	39%
GPT-5.5	36%	41%	37%
Gemini 3.5 Flash	29%	29%	28%

The paper's summary is one sentence: "Agent variants had no effect." The single non-trivial-looking cell — GPT-5.5's +5 points from DeepAgent — sits inside overlapping error bars on n=100 and is not reproduced by the other two models. Read as an ablation this is unusually clean: same model, same verifier, same cap, and the affordances that define the entire many-agent and agent-memory literature buy nothing in a domain with a sound per-step verifier.

The literature null is the more surprising of the two. Giving a model a library of 476,000 mathematics papers is the closest thing in the corpus to the "offline collection of mathematics papers" that FrontierMath Erdős Benchmark hands its models as a matter of course — and here it is measured, and it is worth zero. The paper does not investigate why, which leaves two readings it cannot separate: these conjectures are not the kind whose resolution lives in the literature (47% of them sit on OEIS entries with no links or references at all), or an agent given a 476,000-paper corpus and a bash tool does not find the relevant paper.

Adopted anyway downstream. The FrontierMath Erdős Benchmark methods paper (FrontierMath Erdős) cites both nulls and keeps the deepagent and the 476,000-paper snapshot in its default agent regardless, "as future models may be able to make better use of them" — a design choice made against this page's evidence, not because of it. It also describes this benchmark's 492 conjectures as "of uncertain mathematical significance", the same curation contrast this page draws.

Results#

Full set, $50 cap, one run per model (Figure 1 right, viewed; each bar split into proofs and disproofs):

System	Resolved	Proved	Disproved
Claude Opus 4.8	30% (147/492)	19%	11%
GPT-5.5	26%	16%	10%
Gemini 3.5 Flash	22%	13%	9%
AlphaProof Nexus (reported)	9% (44/492)	—	—

LITE, $200 cap, base agent (Figure 1 left, viewed):

Model	Resolved	Proved	Disproved
Claude Fable 5	44%	25%	19%
GPT-5.6 Sol	43%	25%	18%
Claude Opus 4.8	39%	21%	18%
GPT-5.5	36%	18%	18%
Gemini 3.5 Flash	29%	15%	14%

Fable 5 and GPT-5.6 Sol were run only on LITE and only with the base agent.

Roughly 40% of "resolved" conjectures are false#

The proof/disproof split is stated nowhere in the abstract and is the most under-sold number in the paper. On the full set Opus 4.8's 30% is 19 points proved and 11 disproved — 37% of its solves are counterexamples. On LITE at $200 the disproof share is higher still: 18 of Opus's 39 points, 19 of Fable 5's 44, and 14 of Gemini 3.5 Flash's 29 — between 43% and 48%. Two consequences:

• The benchmark measures refutation at least as much as proof. Finding a counterexample to a statement about integers is a search problem a model with bash, SageMath and a Python stack is well-equipped for, and the disproof share rising with budget is consistent with search paying off. This is the same asymmetry Automated Conjecturing records from the conjecture-generation side, where refutation has a free graded signal and proof does not.
• A high disproof rate is evidence about the item set, not only about the models. Nearly half of the resolvable conjectures in a curated set of "mathematically interesting" open conjectures are simply wrong. That is a fact about what survives OEIS editorial review, and it bounds how much a rising score here should be read as mathematical progress.

The cost curve: ~10 points per 10× spend, no plateau#

Figure 2 (viewed) plots, for every run, the fraction of conjectures resolved as a function of the spend at the moment of resolution, so reading the curve at $x$ estimates the solve rate of a run capped at $x$. Across all eight curves the rise is roughly linear in log-spend, on the order of ten percentage points per tenfold increase, from about 3–10% at $0.50 to 22–44% at the caps, with no visible plateau at $200.

Average cost per resolved conjecture on the full set: $6 (GPT-5.5), $9 (Gemini 3.5 Flash), $10 (Claude Opus 4.8), maximum $47. By comparison, the AlphaProof Nexus authors estimated in personal correspondence that their cost per resolved OEIS conjecture was "roughly $10 on average, and up to about $50 for the hardest few" — which is what makes the 147-vs-44 comparison a comparison at matched cost per solve rather than a budget advantage.

Epoch's own extrapolation, and the one number here that is a projection rather than a measurement: because LITE is a random subset, at $200 per conjecture the best current models would be expected to resolve about 216 of the 492, up from 147 at $50.

Two denominators, not one. The 30%-at-$50 and 44%-at-$200 figures are frequently quoted together and are not the same measurement: 30% is one model on 492 conjectures, 44% is a different model on a 100-conjecture subset at 4× the budget. The comparable pair within one model is Opus 4.8's 30% at $50 on the full set and 39% at $200 on LITE — about nine points for a quadrupling, which is where the "ten points per decade" slope comes from.

The newest generation is not a jump#

Fable 5 (44%) and GPT-5.6 Sol (43%) are the top two on LITE, and their lead over the previous generation (Opus 4.8 at 39%) is a few percentage points, inside or near the error bars. The paper says so directly: "On this benchmark, Claude Fable 5 and GPT-5.6 Sol do not represent a qualitative jump in autonomous AI proving." Set against the same models scoring 0/68 on FrontierMath Erdős Benchmark a month later, the reading is that both benchmarks agree the generation gap is small and disagree completely about the absolute level.

The models solve nearly the same conjectures#

Derived from Figure 5 (viewed) rather than stated in the prose: the per-proposer bars label how many of each proposer's conjectures were solved by at least one of the three $50 runs, and those numerators sum to about 150 of 492 (31%) — against 147 for Claude Opus 4.8 alone. Three different frontier models from three labs, run independently, add roughly three conjectures to the best single model's set. (The denominators sum to exactly 492, which is the arithmetic check; one numerator is legible only to ±1, so read the union as ~150, not exactly 150.)

If that holds, the resolvable subset is a near-fixed property of the problems rather than of any model's idiosyncratic strengths — which is the opposite of the picture FrontierMath Erdős Benchmark's off-protocol data suggests at the hard end, where the same model on the same problem succeeds on 1 of 4 attempts. The two are compatible if per-problem success is bimodal: reliably solvable or essentially never, with a thin middle.

The composition of the denominator, measured#

Epoch collected provenance metadata that no other open-problem benchmark in this corpus has: for each conjecture, who proposed it and when (via GPT-5.5 matching each Lean statement to the OEIS text and revision history — a proposer for 488 and a date for 489 of the 492, 443 rated high-confidence), plus two proxies for literature attention (citations listed on the OEIS entry, and OpenAlex works whose full text references the sequence).

Attention. 47% of the conjectures sit on OEIS entries that list no links or references at all, and on the full set the 0-citation bin is the largest (n=230) and has the highest solve rate (~35/33/25% for the three models, against ~24/19/18% at 1–2 citations). The 10+ bin (n=15) looks higher still but is fifteen items with error bars spanning twenty points. On the OpenAlex measure, 451 of 492 sequences have zero citing works. So the benchmark is overwhelmingly composed of conjectures nobody has written about, and the ones nobody has written about are the ones that fall.

Proposers. 127 distinct proposers, but the distribution is extreme: the prolific conjecturer Zhi-Wei Sun proposed 37% of OEIS OPEN (180 of 492) and 36% of LITE, and his are the hardest — ~16% solved by at least one of three runs, against 41% for the 176 conjectures from the 116 long-tail proposers and 30% for Peter Bala's 56. More than a third of the benchmark is one person's conjectures, and a model's score is substantially a score on Zhi-Wei Sun.

Age. Solve rate by proposal year runs backwards from the naive expectation: on LITE the pre-2012 bins are solved ~71–75% and the 2012–2021 bins ~13–39%. Those old bins hold 7 and 4 conjectures, so the effect is four or five items wide; the full-set bins (n=35/31/175/132/116, three conjectures excluded for having no recorded date) are where any real version of this claim would have to live.

Contamination immunity, and its dated expiry#

OEIS OPEN makes the same prevention-by-construction argument as the unsolved-item-set design: open problems' "solutions cannot leak into training corpora, at least until they are solved," and Epoch notes that every model evaluated has a training cutoff predating the publication of Tsoukalas et al., so none could have learned the proofs released with that paper. The stated mitigation is the same denominator filter: "conjectures resolved before a model's training cutoff can be filtered out, and all models compared on the remaining smaller set."

The expiry is not hypothetical here, it has already started. DeepMind released its OEIS proofs with the 2026-05 paper — 38 of them, per this paper's footnote, although that paper reports 44 solves — and Epoch has now released the accepted Lean proofs for its own 153-conjecture resolved set at github.com/epoch-research/LeanOpenProblems-results. So at least 153 of the 492 items — 31% — have a published machine-checked proof as of 2026-09, rising toward ~190 (39%) to the extent DeepMind's 38 are disjoint from Epoch's 153, which neither source reports and which is unlikely given that both sets are drawn from the easy tail. A model trained after this paper is evaluated on a set that is at least a third pre-solved in public. The instrument is consumed by its own success faster than FrontierMath Erdős Benchmark's, precisely because it works better.

The limitations the paper states about itself#

Worth recording in full, because the paper is unusually forthcoming and because three of the four bear directly on how the 30% should be read:

1. Most conjectures have likely received little attention. Stated three separate times, and supported by the metadata above rather than asserted. The selection prompt explicitly excluded famous open problems; OEIS editors filter for well-definedness, not for depth. Epoch's suggested fix: "Future work could use LMs to explicitly select problems that have received considerable mathematical interest rather than excluding them."
2. Misformalization risk, with the dataset taken as-is. Tsoukalas et al. had a human review all 44 conjectures their system resolved and found no misformalizations; Epoch performed no further validation and writes that "it seems likely that at least some conjectures are misformalized." Its argument for why the benchmark survives this is a relative one — misformalizations are likely easier to resolve, and unlikely to advantage one model over another, so the set remains useful for comparing models even if the absolute rate is inflated. That is the right argument and it does not save the headline number, which is an absolute claim.
3. No credit for reductions to famous open problems. Only a proof or a disproof counts, but "mathematicians also value results that relate a conjecture to a famous open problem" — proving that a conjecture implies the Collatz conjecture "would often be considered the definitive word on it," and scores zero here.
4. Resolved conjectures leak into training data, per the section above.

There is one more, stated as a footnote rather than a limitation: a conjecture "could in principle be independent of Lean's axiomatic foundation, in which case neither it nor its negation is provable and the task is unsolvable" — the formal-proof analogue of the unsolvable-item problem Epoch criticizes in generator-verifier benchmarks (where FM:OP estimates 10–40% of problems may have no solution of the required form). Here it is presumably negligible and is not quantified.

Why formal proof, argued against the alternatives#

The paper's introduction is the corpus's clearest statement of why an open-problem benchmark should demand a Lean proof rather than a checkable object, and it argues it against two named competitors — HorizonMath (101 problems) and FrontierMath: Open Problems (FM:OP, 50 problems), both of which make unsolved problems verifiable by restricting to problems with a generator-verifier gap (candidate solutions are hard to find and cheap to check). Four objections:

1. Coverage. "The vast majority of open problems have no generator-verifier gap: they call for a proof of a general statement rather than the exhibition of a checkable object."
2. Evidence, not proof. HorizonMath describes accepted closed forms as "best regarded as conjectures until proven"; FM:OP explicitly allows verifiers providing "strong numerical evidence."
3. Soundness rests on hand-crafted code. HorizonMath needs an LLM judge to reject hard-coded constants and numerical root-finding; FM:OP's bespoke per-problem verifiers are labor-intensive and error-prone — in July 2026 two problems were removed because their verifiers "would not detect correct solutions with high enough fidelity."
4. Computational checking is one-sided. A verifier confirms an exhibited object works; if no such object exists the task is unsolvable, and FM:OP estimates 10–40% of its problems are unsolvable.

The formal route trades these for two costs it names honestly: only conjectures statable in Mathlib qualify, and "results reflect formalization ability as well as mathematical ability, since a model may find a correct argument yet fail to formalize it." Note that objection 3 is the shape AI-Driven Formal Proof Search keeps recording from the other direction — a verified-proof pipeline falls back on LLM judges for statement provenance, while a checkable-object pipeline falls back on them for solution legitimacy. Neither escapes the judge; they differ in where it sits.

The proofs are read back by a model, and nobody checked that#

A detail from Appendix A.1 that belongs on Logical vs Intelligible Proof: Table 1's sequence descriptions, conjecture statements and proof summaries were written by GPT-5.6 Sol agents given the accepted Lean proof, the OEIS entry, and sandboxed access to the Mathlib source tree. The paper reports no human check on these summaries.

This is the intelligibility gap being papered over by exactly the machinery the kernel was supposed to replace. The proof is certified; the only human-readable account of what the proof does is an uncertified LM narration of a Lean file. Anyone reading Table 1 to learn how a conjecture was resolved is reading a model's story about a kernel's verdict, and the two are guaranteed to be about the same object only in the sense that the model was shown the file. It is not a flaw in the benchmark — the verdicts are unaffected — but it is a concrete instance of the logical/intelligible split appearing inside a paper that does everything else right.

Connections#

• FrontierMath Erdős Benchmark — the sibling and the counterweight: same evaluator, same author, same month, same kernel-checked standard, and 3% against this page's 30% because one denominator was curated for significance and this one was curated to exclude famous problems. Read together they price the curation axis at roughly 10× solve rate and 6× budget
• AI-Driven Formal Proof Search — the paradigm this scores, and the fourth denominator it supplies: open research conjectures, uncurated for significance, with a cheap fixed budget and a full item-set run for every model
• Agentic Loops Overtake Bespoke Systems — the head-to-head this page exists to supply: a three-tool ReAct loop resolves 147/492 against the bespoke evolutionary system's 44/492 on the bespoke system's own item set, at matched cost per solve — with the model generation confounded, and with a matched-model DeepAgent ablation that comes out exactly null
• Evolutionary Proof Search — the machinery on the losing side of that comparison, re-measured against a denominator its authors chose
• AlphaProof Nexus — the system that built the item set and reported 44/492; the one whose result is now the baseline bar in someone else's figure
• Many-Agent Proof Harnesses — the DeepAgent arm is the smallest clean test of that page's premise: subagents, persistent memory and a todo list, same model and same $200 cap, and the score does not move
• Automated Conjecturing — the upstream supply: 2,649 human-proposed open OEIS conjectures filtered to 500 by a model, with 37% of the survivors from one prolific conjecturer and 47% sitting on entries with no citations — the attention distribution that page's triviality problem predicts, measured
• Benchmark Contamination and Decontamination — the second instance of immunity-by-unsolvedness, and the first where the expiry is dated: at least 153 of the 492 items now have published machine-checked proofs, four months after the set was built
• Logical vs Intelligible Proof — the appendix's LM-written proof summaries: a kernel-certified proof whose only human-readable account is an unchecked model narration
• Compute-Controlled Benchmarking — the budget written into the score's definition again, and here with the spend curve published rather than a single cap: ~10 points of solve rate per 10× spend, measured across eight runs
• Large-Scale Test-Time Compute — the log-linear, un-plateaued cost curve on open research problems, which is the scaling measurement FrontierMath Erdős Benchmark names as missing and cannot supply at its own rates
• Kernel-Level Proof Auditing — the page that turns this one's attack list into a measurement: a compile-plus-sorry-scan harness (the check most prover papers run) accepts sorryAx-dependent proofs at a 31–44% rate for one released model, which is item 5 of the list above happening in the wild without anyone trying
• Lean — the verification substrate; SafeVerify's three-axiom whitelist, native_decide exclusion and three-container split are the strictest protocol statement in the corpus, and the Comparator cross-check is the first measured disagreement between two of its checkers
• Epoch AI — the evaluator
• Claude Fable 5 — top scorer on LITE at 44%, and the paper's evidence that the newest generation is not a qualitative jump here
• UK AI Security Institute — Inspect, the library the base agent and the DeepAgent variant are both built on
• Statement Drift — the general failure behind this page's misformalization caveat: a statement taken as-is from an autoformalizer is a trusted copy nobody has read, so a kernel-accepted resolution can be a valid proof of the wrong conjecture

Open Questions#

• Is the resolvable subset a fixed property of the problems? The union of three $50 runs across three labs' models is ~150 of 492, against 147 for the best single model — i.e. model diversity adds about three conjectures. Falsifiable directly: publish the per-conjecture solve matrix and report pairwise overlaps, or run one model k times and compare the k-run union to the three-model union. If model diversity really buys nothing, the benchmark measures problem difficulty alone and pass@k reporting on it is meaningless.
• Does the literature null survive a retrieval-shaped test? 476,000 arXiv papers changed no model's score, but the agent had only bash over a LaTeX source tree and no retrieval index, and 47% of the conjectures sit on OEIS entries with no references at all. Separating "the answers are not in the literature" from "the agent cannot find them" needs one of: a keyword/embedding index over the same corpus, or a solve-rate split between conjectures whose sequences do and do not have citing works under the literature arm specifically.
• How many of the 153 resolved conjectures were misformalized? Epoch performed no validation and expects some to be wrong; Tsoukalas et al. reviewed their 44 and found none. Every accepted proof is public, so this is answerable by the same human review at roughly 3.5× the effort — and it is the one check that would turn the 30% from an upper bound into a measurement. Extended 2026-09-29 by SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization (empirical): no count, but a prior and a method. On a different object (agents generating statements from informal text, not a benchmark author formalizing them) the best system compiles 61.8% and is aligned 11.2%, and 65 of 110 compiling outputs fail both implication directions; a benchmark whose statements are given avoids that generation failure but not the author's formalization error (ShadowBench itself withdrew one problem for a faulty reference statement and excluded 31% of ProofNet for known faulty references). The method transfers: forward and backward checks against independently formalized shadow theorems can be run on the 153 resolved statements.

Sources#

• OEIS Open: How many conjectures can language models turn into theorems? — Tom Adamczewski (Epoch AI), "OEIS Open: How many conjectures can language models turn into theorems?", arXiv 2608.11941, 2026-08-12, 27pp, ~19,500 words, empirical. Benchmark and scaffold open-sourced at github.com/epoch-research/LeanOpenProblems; per-sample results, rejected submissions and verifier output at LeanOpenProblems-results. Single-author paper from the organization that also authored FrontierMath Erdős Benchmark, evaluating five commercial models it does not sell, and whose headline comparison is against a competitor's published system — the COI runs toward Epoch's benchmark franchise rather than toward any model. It disciplines itself in the direction that costs it the headline: the Comparator cross-check that lowers its own number to 144/492 is in a footnote rather than suppressed, and the AlphaProof Nexus cost estimate that makes the 3.3× comparison fair was obtained from the losing system's authors by correspondence. Parse note: PDF-derived (docling 2.126.0, MLX layout and table stages, 27pp, 15 table-blocks, 8 pictures, confidence excellent, all ingest checks ok). The 15 blocks are page-continuations of one logical table (Table 1), reconciled in full against pdftotext -layout on the local PDF — 100 data rows, the A-number multiset identical to the reference parse, and all 100 cost values identical. One page-break weld: the A226163 row absorbed the tail of the A365179 row's conjecture and proof-summary text across the p. 12/13 boundary. No number is lost and no row is missing; nothing from Table 1 is cited on any wiki page beyond its row count and cost range. Internal inconsistency, unresolved: the appendix says Table 1 shows "the 100 costliest of the 153 conjectures resolved by either Claude Fable 5 on LITE or Claude Opus 4.8 on the full set" and that 35 were resolved by both — but 147 + 44 − 35 = 156, not 153. The consistent reading is that the 35 counts overlap among Table 1's displayed 100 rows rather than across all 153, which would put the true overlap at 38; the paper does not say, and the text is confirmed verbatim against pdftotext, so this is the authors' arithmetic and not a parse artifact. All figure numbers above were read from the images in and cross-checked arithmetically: Figure 4's citation bins sum to 492 and 100, Figure 5's proposer denominators sum to exactly 492, and Figure 6's year bins sum to 489 with the three undated conjectures excluded as the caption states. Figure 5's Zhi-Wei Sun numerator renders ambiguously at 28 or 29, which is why the derived three-run union is quoted as ~150
• Reward-Oracle MCTS for Formal Theorem Proving: Sample-Efficient Search and the Need for Kernel-Level Proof Auditing — Vamshi & Yang (University of Maryland), arXiv 2608.28639, 2026-08-11, 14pp, empirical. Cited here for one thing: the measured prevalence of sorryAx-dependent successes under a compile-plus-source-scan harness, which prices item 5 of this page's attack list. Its benchmarks (MiniF2F, PutnamBench, two physics sets) are closed competition problems and share no items with this one, so nothing in it bears on the 147/492 figure or on SafeVerify's own verdicts. Full treatment on Kernel-Level Proof Auditing
• FrontierMath Erdős — Adamczewski & Bloom, arXiv 2609.25050, 2026-09-06, empirical. Cited for the sibling's decision to keep this page's two null affordances; full treatment on FrontierMath Erdős Benchmark.
• SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization — Han et al., arXiv 2608.29270, 2026-08-29, empirical. Cited here only to extend the misformalization open question: a measured 11.2% aligned against 61.8% compiling for generated statements, a different object from OEIS Open's given statements. Full treatment on Kernel-Level Proof Auditing.