Lean 4 formalization of the corrected Erdős Problem 796, proving the second-order asymptotic and explicit kernel-checked bounds.
Proof for the off-diagonal commonality region of cycles of length 2k and 2m+1
Erdős Problem 1075: counterexamples for every r >= 5, with a complete Lean formalization
Tuza's conjecture for graphs of maximum degree at most seven — paper, certificate catalogue, and exact verifiers
Certified scoped theorem for binary covering sequences: every valid length-70 (9,1) cover uses at most 60 distinct edges in common with one fixed backbone; global bounds unchanged.
Research notes, exact computations, and reproducible verification for MathOverflow 413935
Proof of the semi-inducibility of the alternating 4k+2 cycles.
Computer-assisted proofs and clean-room audits for the r=10 and r=11 fixed cases of Erdős Problem 617.
AI-assisted mathematical research manuscripts with reproducible materials across combinatorics and words, matrix and coding theory, topology, order and discrete geometry, algebra, matroids, and continuous optimization.
Bounds, exact computations, barriers, and open problems for extremal Seidel quadratic forms on the Boolean cube.
Lean 4 formalization and reproducibility artifacts for the exact saturated 6- and 7-Sperner numbers
Paper I: a finite, Lean-verified fractional clique-partition bound for split graphs. Part of an Erdős #81 research program; #81 remains open.
Erdős Problem 1182: f(n) = Θ(n^{3/2} sqrt(log n)), from a matching lower bound for the minimum Ramsey number of a graph with m edges
Reproducible proofs of eight exact finite Zarankiewicz numbers, including a complete DRAT/LRAT and exact SCIP/VIPR certificate for Z(10,23,3,3)=112, plus Z(13,23,3,3)≤144.
Machine-checked progress on the Brualdi-Goldwasser (1984) Laplacian-ratio maximizer for trees (Lean 4 + Mathlib, no sorry) + Telperion, a sympy-to-Lean certificate pipeline
To associate your repository with the extremal-combinatorics topic, visit your repo's landing page and select "manage topics."