Codex Swarm Claims 19 Erdős Problem Solutions

A math project highlighted on Hacker News says it used 20 Codex accounts running in parallel to tackle open problems from erdosproblems.com — and now lists 19 proposed solutions, including 13 full solutions formalized in Lean 4.

The site, Starfleet Math, is careful to note that many problems marked “open” may already have informal or partial answers online, and says it tried to avoid those cases but “most likely failed in certain cases.” It also asks readers to report attribution mistakes.

Two examples stand out in the material provided.

For Erdős Problem #123, which carries a $250 prize, the project claims a full proof of the intended nondegenerate version: for pairwise-coprime integers a, b, c > 1, every sufficiently large integer can be written as a sum of distinct terms of the form a^i b^j c^k, with no chosen term dividing another. The write-up says the main obstacle was constructing a multiplicatively wide seed interval, and that the key step was an “optional interior shell” on a single homogeneous exponent level. The final theorem is formalized in Lean as Erdos123.erdos_123, and the project says the build contains no proof placeholders and no sorryAx. It also notes the webpage’s literal statement a, b, c ≥ 1 is false at (1,1,1), so the formal result uses a, b, c > 1.

Recommended reading

31% solar module drops indium for cheap tin oxide

For Erdős Problem #254, the project says it proved that if A ⊆ ℕ satisfies both a dyadic shell growth condition and ∑_{n∈A} ‖θn‖ = ∞ for every real 0 < θ < 1, then every sufficiently large natural number is a sum of distinct elements of A. The theorem appears in Lean as Erdos254.erdos_254. According to the report, the proof’s two big moves were showing that the set of “bad” phases is countable, then replacing missing ergodic machinery with a finite-cyclic spectral proof.

The page presents each result with a problem statement, a claimed theorem, a detailed report, and a download link labeled “Full Solution & Verify with Your AI.” The headline number remains the punchline: 19 proposed solutions, 13 full solutions, all from a parallelized 20-account Codex run.