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.

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.

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

Lean 4 formalization of the corrected Erdős Problem 796, proving the second-order asymptotic and explicit kernel-checked bounds.

Papers, proofs and research records for eight Erdős problems, including what is established and what remains open.

Python programs and examples for checking research and software results: rerunning affected tasks, checking AI work claims and comparing forecasts.

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.

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 proof of Erdős Problem 181 (Erdos 181): the Ramsey number of the n-dimensional hypercube satisfies R(Q_n) = O(2^n), linear in its number of vertices; formalization with Mathlib

The official repository of the Nexus Resonance Codex (NRC)

Stanford AI for Lean Club progress on Erdős problems: papers, frontier notes, visualizer data, and Lean formalization.

Lean 4 proof of the finite case of Erdős Problem 172 (Erdos 172, Hindman sums and products): every finite colouring of the positive integers has, for each m, an m-element set whose nonempty subset sums and products share one colour; formalization with Mathlib

AI-agent pipeline producing machine-verified Lean 4 proofs — four PRs merged into Google DeepMind's formal-conjectures

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

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

AlphaProof Nexus evolution on Erdős Problem #25 — does every congruence-avoiding set have a logarithmic density? Open problem, formalized in Lean 4.

Proof claims and reproducible verification for the r=5,6,7,8 cases of Erdős Problem 617.

Preprint 'Prime powers in prime gaps and Erdős Problem #458' and its Lean 4 formalization. #458 remains open; VERIFICATION.md lists what is proved and what is assumed.

Computer-checkable proofs and recorded checks for research on eight Erdős problems. Papers and current claims: wcook04/plectis-erdos.