The Problem Is the Problem: Towards Scalable Mathematical Discovery
Zeyu Zheng, Shengtong Zhang, Jeremy Avigad, Prasad Tetali, Sean Welleck
cs.AI, math.CO
2026-08-18
CMU researchers replace the pick-one-problem interface with pick-a-direction: a cascade distills 5,245 combinatorics papers into 4,717 open conjectures, attempts each with gpt-5.5, and filters the output to 77 publishable results, all 15 human-reviewed ones mathematically correct.
The standard AI-for-math workflow has humans pick a specific problem and point a model at it. As models improve, that interface becomes the bottleneck: frontier reasoning is purchasable by budget, while problem selection and expert review of proofs are scarce. The humans are wedged at both ends of the pipe while compute sits idle in the middle.
The CMU team (including Sean Welleck of Lean-tooling fame and mathematicians Jeremy Avigad and Prasad Tetali) changes the interface. Instead of a problem, the human supplies a research direction, and the system finds candidate problems in the literature, attempts them, and pushes only the filtered survivors to expert attention. Choosing a direction replaces choosing a problem.
The pipeline, FAR (Find, Attempt, Recommend), borrows the cascade logic of search and recommender systems: cheap models filter a large pool, expensive models handle the narrow, harder tail.
A design choice worth noting: difficulty and importance scores (anchored at unpublishable-exercise vs. top-journal, and no-content vs. Fields-Medal-level) are recorded during the checking stage, before any reasoning budget is spent. That fixes them in advance so the run's outcomes can validate the scores after the fact.
The cascade counts: 51,110 papers → 5,245 → 6,453 candidates → 4,717 open conjectures → 1,050 claimed resolutions → 598 judged correct → 77 publishable. Of 4,717 attempts, 2,905 returned nothing, 443 turned out already resolved, 319 exposed defective statements.
The authors manually reviewed 15 of the 77 artifacts that interested them and found no mathematical error in any. Representative results:
| Target | Type | Result |
| Davies-Jenssen-Perkins-Roberts conjecture (independent-set ratio in triangle-free graphs) | Counterexample | C₅□K{m,m} drives the ratio to 24/13 < 2; C₁₃(1,5) lowers it to 32/19 |
| Erdős-Straus divisibility question | Answer | d(n) = 1 for every fixed n ≥ 2 |
| Ikenmeyer-Pak-Panova symmetric-group character conjecture | Proof | Many-one GapP-completeness holds via two-row partitions |
| Lund-Saraf-Wolf conjecture (unions of lines in F₃q) | Counterexample | Half-tangent family of an elliptic paraboloid gives density 1/2+o(1); counts verified exhaustively for q ≤ 13 |
The difficulty score achieves an AUC of 0.69 against having no accepted resolution (p < 10⁻⁴⁰), importance 0.60 against being graded publishable (p = 0.008). In budget-allocation experiments, ranking by estimated publishability beats uniform random at every budget; when the goal is the single most important artifact, keeping only the top 1/10 by importance before ranking works best.
The scarce resource in AI-for-math has shifted from model capability to expert attention. A 77-to-4,717 compression means every item a mathematician sees has passed model self-certification, a correctness tribunal, and a value grading, cutting review cost by an order of magnitude. For anyone building research infrastructure, this is a complete worked example of porting recommender-cascade thinking into science: cheap models for breadth, expensive ones for depth, allocation strategies with theoretical guarantees (exact or 1-1/e-approximate depending on the objective). The counterexamples deserve notice on their own: counterexamples need no long proofs, which fits the reliable range of current models.
To be honest about the increment: one attempt per conjecture, one pilot domain, and most of the 77 artifacts unpublished. This is a feasibility demonstration of a paradigm, not proven productivity of new mathematics.
Stated by the authors: single attempt per conjecture with multi-attempt strategies unexplored; the bandit view of allocation sketched but not implemented; results depend on corpus coverage and on the specific models in the cascade. Human review covered 15 of 77 artifacts; the other 62 rest on model judging alone. Two concrete lessons: one artifact graded NEW (an Erdős divisor-difference problem) had in fact been settled four months earlier on the Erdős problems site, by Liam Price with ChatGPT-5.2, and the cascade's searches never found it. The Lund-Saraf-Wolf counterexample construction turns out to be a classical object in finite geometry (the half-tangent partition of an elliptic quadric, Bruen-Drudge 1999); the contribution is connecting it to the conjecture. Publishability is a model judgment; the fate of the 77 rests with actual peer review. Total compute cost and spend are not disclosed, so the reproduction bar is unknown.