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
Plectis by Will Cook: an open-source prototype for mathematical exposition and collaborative research. Eight Erdős programmes, short and long papers, Lean proofs, cross-problem mathematics and reusable infrastructure, with explicit sources, evidence and contribution credit.
Plectis: Lean research on Erdős problems. Read it at wcook04.github.io/plectis. This repository holds the website source and the earlier Python toolkit; the Lean proofs are in wcook04/plectis-erdos.
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 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 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₁,₃,₃.
The official repository of the Nexus Resonance Codex (NRC)
AI-agent pipeline producing machine-verified Lean 4 proofs — four PRs merged into Google DeepMind's formal-conjectures
A quantitative corollary of Bradač’s theorem resolving Erdős Problem 920
Stanford AI for Lean Club progress on Erdős problems: papers, frontier notes, visualizer data, and Lean formalization.
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.
Computational evidence isolating the log(n) spreadness artifact in the Erdős k=3 Sunflower Conjecture via bitmask-accelerated Simulated Annealing.
Preprint series on fractional and integral clique partitions, chordal graphs and quantitative stability, with bilingual manuscripts, Lean 4 formalizations and audit evidence.
A continuously re-verified ledger of mathematical records. Mirrors published bounds and constants, re-checks them daily, and goes red when a cited record moves.
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.
Results mined from a 30,438-object ore ledger and re-checked from scratch, including one PROVED claim shown false
To associate your repository with the erdos-problems topic, visit your repo's landing page and select "manage topics."