Lean 4 formalization of the corrected Erdős Problem 796, proving the second-order asymptotic and explicit kernel-checked bounds.
Research notes, exact computations, and reproducible verification for MathOverflow 413935
Proof for the off-diagonal commonality region of cycles of length 2k and 2m+1
Proof of the semi-inducibility of the alternating 4k+2 cycles.
Tuza's conjecture for graphs of maximum degree at most seven — paper, certificate catalogue, and exact verifiers
Paper I: a finite, Lean-verified fractional clique-partition bound for split graphs. Part of an Erdős #81 research program; #81 remains open.
Computer-assisted proofs and clean-room audits for the r=10 and r=11 fixed cases of Erdős Problem 617.
Miura-ori origami flip graphs: candidate general diameter proof using convex order, majorization, and discrete Lipschitz functions, with reproducible verification.
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.
Certified length-70 binary (9,1) fixed-backbone theorem: every valid cover uses at most 60 distinct edges of one explicit 64-edge backbone; global bounds unchanged.
Lean 4 formalization and reproducibility artifacts for the exact saturated 6- and 7-Sperner numbers
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."