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.
Lean 4 formalization of the corrected Erdős Problem 796, proving the second-order asymptotic and explicit kernel-checked bounds.
CLI toolkit for Erdős problem research: literature ingestion, RAG search, and Lean 4 formalization
Stanford AI for Lean Club progress on Erdős problems: papers, frontier notes, visualizer data, and Lean formalization.
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.
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.
The official repository of the Nexus Resonance Codex (NRC)
Computational evidence isolating the log(n) spreadness artifact in the Erdős k=3 Sunflower Conjecture via bitmask-accelerated Simulated Annealing.
The official repository of the Nexus Resonance Codex (NRC) Protein Folding Enhancements.
AI-assisted reproducible SAT, exact-search, and Lean research on open Erdos problems; no full solution claimed.
Weighted Erdős–Szekeres (Erdős #1026) in Lean 4 / Mathlib — human-scale proof plus a referee report, failure atlas, and extracted benchmarks for AI theorem-proving
An AI agent's verification-first campaign on open Erdős problems: which conjectures LLMs can actually crack, and why.
Kernel-certified verification of Erdős problem 364 (three consecutive powerful numbers) to 10^14, with axioms limited to propext, Classical.choice and Quot.sound.
Open, fully rigorous re-certification of White's lower bound for Erdős's minimum-overlap problem (#36), with an independent verifier
Explicit C4-free subgraph certificates for hypercubes Q9 through Q15 with reproducible verification.
Proof claims and reproducible verification for the r=5,6,7,8 cases of Erdős Problem 617.
Citation-audited proof note on the Rademacher formulation of Erdős Problem #521
CC0 unrefereed candidate all-N determination for Erdős Problem 848, with replayable exact certificates and AI-readable evidence maps
Add a description, image, and links to the erdos-problems topic page so that developers can more easily learn about it.
To associate your repository with the erdos-problems topic, visit your repo's landing page and select "manage topics."