extremal-combinatorics

Here are 3 public repositories matching this topic...

rishigajjala / erdos-796-lean

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

formal-verification number-theory mathlib lean4 erdos-problems extremal-combinatorics multiplicative-sidon-sets

Updated Jul 15, 2026
Lean

jtraverso / erdos-81-chordal-clique-partitions

Star

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

graph-theory formal-verification mathlib lean4 chordal-graphs erdos-problems extremal-combinatorics split-graphs clique-partition triangle-packing

Updated Jul 10, 2026
Lean

dfield / finite-zarankiewicz-closures

Star

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.

graph-theory formal-verification computer-assisted-proof extremal-combinatorics zarankiewicz-problem

Updated Jul 15, 2026
Linear Programming

Improve this page

Add a description, image, and links to the extremal-combinatorics topic page so that developers can more easily learn about it.

Curate this topic

Add this topic to your repo

To associate your repository with the extremal-combinatorics topic, visit your repo's landing page and select "manage topics."

Learn more

Provide feedback

Saved searches

Use saved searches to filter your results more quickly