erdos-problems

An open, checkable map of AI-assisted discovery in mathematics, named in honor of Paul Erdős's problems. Every result of ours carries receipts: two independent checks, a control and a rerunnable certificate.

CLI toolkit for Erdős problem research: literature ingestion, RAG search, and Lean 4 formalization

The official repository of the Nexus Resonance Codex (NRC) Protein Folding Enhancements.

Independent exact certification of machine-generated mathematics — exact arithmetic, no code shared with the claimant, refusal as a verdict.

Lean 4 proof of the dimension-five variants of Erdős problem 1007: the least edge count of a graph of dimension five is 15, attained by K₆ and K₁,₃,₃.

Lean 4 proof of the extremal half of Erdős problem 1007: a graph of dimension four with nine edges and no isolated vertex is K₃,₃.

Lean 4 source and selected Comparator/Palomar checks for eight Erdős problem programmes. Current claims and papers: wcook04/plectis-erdos.

Connected bipartite graphs of degeneracy exactly r with ex(n,H) ≥ c·n^(2−1/r+1/(28r²)), refuting the Erdős–Simonovits degeneracy conjecture (Erdős problem #146) for every r ≥ 2, with the exact limits of the method. Machine-checked in Lean 4.

Preprint series on fractional and integral clique partitions, chordal graphs and quantitative stability, with bilingual manuscripts, Lean 4 formalizations and audit evidence.

A source-linked index of open math problems solved, refuted, or settled with AI — tracking the July 2026 wave. Verification-status badges, Lean/DRAT certificates, priority caveats.

Results mined from a 30,438-object ore ledger and re-checked from scratch, including one PROVED claim shown false

Erdős–Graham #411 (r=2): the Steinerberger–Hercher bridge, the base-6 cascade (axiom-free Lean), and the omega-ladder; no exceptional prime below 1.33e14. Residual gap open; retraction preserved.

Open, fully rigorous re-certification of White's lower bound for Erdős's minimum-overlap problem (#36), with an independent verifier

An observed prime-descent law for Erdos 710 with five primes held out as a live test, five sealed Hall theorems, and a closed form for the Erdos 1044 extremal family

An AI agent's verification-first campaign on open Erdős problems: which conjectures LLMs can actually crack, and why.

Lean 4 formalization of the k = 1 case of JSP-000467 / Erdős problem 577

A quantitative corollary of Bradač’s theorem resolving Erdős Problem 920

Computational attacks on Erdos 850 and 273: a 4.6e11 exhaustion frontier, an exact parity-split reduction, full receipts, and the negative prior-art result that retired one lane

Automated frontier-model attempts at every open Erdős problem — verdicts, completeness scores, full transcripts.

Paper and partial Lean 4 formalization for a p^(8/15) lower bound on factorial residues modulo a prime