Combinatorics

Pigeonhole Principle

If n+1 objects are placed into n boxes, some box contains at least two objects

lean4-proofcombinatoricsvisualization

Inclusion-Exclusion Principle

The size of a union is the alternating sum of intersection sizes

lean4-proofcombinatoricsvisualization

Catalan Numbers

The ubiquitous sequence counting balanced parentheses, binary trees, and Dyck paths

lean4-proofcombinatoricsvisualization

Stirling Numbers

Counting partitions of n elements into k non-empty subsets

lean4-proofcombinatoricsvisualization

Bell Numbers

The total number of partitions of a set of n elements

lean4-proofcombinatoricsvisualization

Pascal's Identity

The binomial coefficient recurrence: C(n,k) = C(n-1,k-1) + C(n-1,k), the engine of Pascal's triangle.

lean4-proofcombinatoricsvisualization

Orbit Counting Applications

Necklace, bracelet, and coloring counting via Burnside's lemma — concrete applications of the orbit-counting formula.

lean4-proofcombinatoricsvisualization

Vandermonde's Identity

The convolution identity for binomial coefficients: C(m+n,r) = sum over k of C(m,k)*C(n,r-k).

lean4-proofcombinatoricsvisualization

Chu-Vandermonde Identity

The upper negation generalization of Vandermonde's identity to upper complex parameters via rising factorials.

lean4-proofcombinatoricsvisualization

Ramsey's Theorem

Any 2-coloring of K_6 contains a monochromatic triangle: the Ramsey bound R(3,3) <= 6.

lean4-proofcombinatoricsvisualization

Erdos-Ko-Rado Theorem

The maximum intersecting family of k-subsets of an n-set has size C(n-1,k-1) when n >= 2k.

lean4-proofcombinatoricsvisualization

Polya Enumeration

The cycle index polynomial encodes all Burnside fixed-point counts into one generating function for weighted orbit counting.

lean4-proofcombinatoricsvisualization

Stirling's Approximation

The asymptotic formula n! ~ sqrt(2*pi*n) * (n/e)^n, with the Mathlib proof that n!/stirling(n) tends to 1.

lean4-proofcombinatoricsvisualization