Map · 05

combinatorics

MSC 05 · Combinatorics

14,470 declarations (12,022 theorems, 2,448 definitions) across 341 files. 13 of the 81 famous theorems listed for this area are in Mathlib (16%), 18 in some Lean library. 380 open conjectures here are stated in Lean.

Files are assigned to areas by a language model reading each file's documentation. Report a file that is in the wrong area.

Subareas5

05A Enumerative combinatorics 7,226
05C Graph theory 4,984
05B Designs and configurations 1,744
05D Extremal combinatorics 402
05E Algebraic combinatorics 114

Famous theorems13 of 81

From the 1000+ theorems project, which classifies each theorem by MSC area.

Not yet in Mathlib · 68

In Mathlib · 13

Binomial theoremadd_pow
Erdős–Ko–Rado theoremFinset.erdos_ko_rado
Four functions theoremfour_functions_theorem
Friendship theoremTheorems100.friendship_theorem
Hales–Jewett theoremCombinatorics.Line.exists_mono_in_high_dimension
Hall's marriage theoremFinset.all_card_le_biUnion_card_iff_exists_injective
Hindman's theoremHindman.FP_partition_regular
Kruskal–Katona theoremFinset.kruskal_katona
Multinomial theoremFinset.sum_pow_eq_sum_piAntidiag_of_commute
Sperner's theoremIsAntichain.sperner
Turán's theoremSimpleGraph.isTuranMaximal_iff_nonempty_iso_turanGraph
Tutte theoremSimpleGraph.tutte

From the 100 theorems list5

Open conjectures stated in Lean380

Statements without proofs, collected by the Formal Conjectures project.

Files341

Largest first. The code after each file is its assigned subarea.