Erdős problems
Every problem in the Erdős catalogue this system has worked on, with the machine-checked partial results and what remains open.
mapped 1,217 · worked 84 · accepted by OEIS 9 · gate-verified 88
The problem sky
verifiedobstruction / null
Verified contributions
OEIS A309370 — nine verified Sidon records
Nine integer-sum Sidon lower bounds (n = 9,11,12,13,14,15,16,19,20), each independently re-verified, editor-approved and published. The campaign's first external adoption event.
Erdős #993 — forest-surface frontier extension
By Hoggar's theorem a non-unimodal forest needs a non-log-concave component; swept 112,916 generalized trees + 253,695 forest products — all unimodal. The forest surface prior tree-only searches left untouched.
Erdős #302 — improved published bound
f(N) ≤ (155923/180048 + o(1))·N ≈ 0.86601·N, beating the prior best verifiable certificate. Reproduced the published baselines exactly before confirming the new base.
Six verified reductions naming the missing theorem
For #1094, #366, #699, #1093, #376, #488 — gate-verified reductions that isolate the exact open input a number theorist would need. Honest grades, never “solved.”
What the gate rejected
Each was a plausible claim an adversarial probe killed before it could bank.
Independent re-count of the witness against the actual OEIS values.
Phantom. The real improvement was 9 records — which then earned adoption.
Prior-art check before spending compute.
Already solved (Adenwalla, in Lean). Killed before the search ran.
Literature/prior-art check against the active frontier.
Not novel — Tao is at the general/primes frontier. Blocked.
Re-read the problem's actual quantifier (for every k).
Infinitary — a new finite example, not a solve. Graded extends_prior_work.
Honest grade ledger
The grade distribution is the campaign’s honesty made legible: most of the work is nulls, partial proofs, and reductions that name the missing theorem — never inflated to “solved.”
Check it yourself
One command re-checks every result here from its evidence.
vela reproduce examples/erdos-problems