OEIS Open Uses Lean to Verify 492 Unsolved Conjectures, but Cross-Checking Revises the Pass Count From 147 to 144

Epoch AI researchers have introduced [OEIS Open](https://arxiv.org/abs/2608.11941), which turns 492 unsolved conjectures from the *Online Encyclopedia of Integer Sequences* into a reproducible model benchmark. Each problem is formalized in Lean, and models must submit a formal proof of either the conjecture or its negation. Acceptance relies on the Lean kernel rather than comparison with known answers or grading by another model. This allows the benchmark to test problems with no publicly known solutions while reducing the likelihood that answers appeared directly in training data.

The authors gave models including Claude Opus 4.8, GPT-5.5, and Gemini 3.5 Flash access to basic shell commands, file-editing tools, and the Lean compiler. On the full set, the budget was $50 per problem, and the union of successful proofs across all models covered 147 problems, or 30%. On Lite, a randomly sampled subset of 100 problems, raising the per-problem budget to $200 allowed the best model to reach 44%. Notably, supplying an additional 476,000 arXiv mathematics papers or switching to a more complex DeepAgent loop did not improve Lite performance, suggesting that the current bottleneck may not simply be a lack of retrieved material or planning steps.

To prevent agents from altering the theorem, introducing disallowed axioms, or contaminating the toolchain, each attempt was separated into an offline agent environment and clean compilation and verification containers. SafeVerify rebuilds artifacts from scratch and checks the target declaration’s name, type, and permitted axioms. The public results repository also preserves each problem’s Lean file, token cost, and failure stage for third-party auditing.

The verifier itself, however, is not entirely beyond dispute. When the authors cross-checked Claude Opus 4.8’s results using the Lean team’s Comparator, they found anomalies in the original formalizations of five problems, while two others had merely exhausted SafeVerify’s resources. Under Comparator, the score should therefore be revised from 147/492 to 144/492. Most of these conjectures have attracted little attention, their mathematical significance remains uncertain, and the score measures both mathematical reasoning and Lean engineering ability. Future work should track manual specification audits, verifier standardization, and whether models can reproduce successful proofs at lower cost.