extremal-combinatorics

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

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

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 for the off-diagonal commonality region of cycles of length 2k and 2m+1

Exact extremal-set classifications over F31 and F73: sum, product and progression avoidance; original C/C++ and Python verification

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.

Paper I: a finite, Lean-verified fractional clique-partition bound for split graphs. Part of an Erdős #81 research program; #81 remains open.

Lean 4 formalization and reproducibility artifacts for the exact saturated 6- and 7-Sperner numbers

Bounds, exact computations, barriers, and open problems for extremal Seidel quadratic forms on the Boolean cube.

Erdos 20: Lean sunflower lemmas, exact small cases, product constructions, historical build evidence and the open frontier.

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