Catalan Numbers

Statement

The $n$-th Catalan number is:

They satisfy the recursion:

Visualization

Values $C_0$ through $C_8$:

$n$	0	1	2	3	4	5	6	7	8
$C_n$	1	1	2	5	14	42	132	429	1430

Balanced parentheses for $n=3$ (all $C_3 = 5$ arrangements):

((()))    (()())    (())()    ()(())    ()()()

Dyck paths for $n=3$ — lattice paths from $(0,0)$ to $(6,0)$ that never go below the $x$-axis:

Path 1: ((()))       U U U D D D
         /\
        /  \
       /    \___

Path 2: (()())       U U D U D D
         /\
        /  \/\

Path 3: (())()       U U D D U D
         /\
        /  \   /\

Path 4: ()(())       U D U U D D
        /\  /\
            /  \

Path 5: ()()()       U D U D U D
        /\ /\ /\

Each up-step $U$ corresponds to ( and each down-step $D$ to ). The path must stay at or above height 0.

Recursion unrolled for $C_4 = 14$:

Proof Sketch

Ballot problem / reflection argument: Count lattice paths from $(0,0)$ to $(2n, 0)$ with $+1$ and $-1$ steps that stay non-negative. Total paths: $\binom{2n}{n}$. Bad paths (those that go negative) biject with unrestricted paths from $(-2, 0)$ to $(2n, 0)$ via the reflection principle, numbering $\binom{2n}{n+1}$. So:

Mathlib's Catalan number satisfies catalan_succ: $C_{n+1} = \sum_{i : \text{Fin}(n+1)} C_i \cdot C_{n-i}$.

Connections

• Pigeonhole PrinciplePigeonhole Principle$$|f^{-1}(\{y\})| \geq 2 \;\text{for some}\; y \in B \;\text{when}\; |A| > |B|$$If n+1 objects are placed into n boxes, some box contains at least two objectsRead more → — the ballot problem uses a pigeonhole argument to count bad paths
• Inclusion-Exclusion PrincipleInclusion-Exclusion Principle$$|A \cup B| = |A| + |B| - |A \cap B|$$The size of a union is the alternating sum of intersection sizesRead more → — bad paths counted via complementary counting
• Stirling NumbersStirling Numbers$$S(n,k) = k \cdot S(n-1,k) + S(n-1,k-1)$$Counting partitions of n elements into k non-empty subsetsRead more → — both sequences count partition-like structures; $C_n = S(2n, n)/(n+1)!$ (approximately)
• Bell NumbersBell Numbers$$B_n = \sum_{k=0}^{n} S(n, k)$$The total number of partitions of a set of n elementsRead more → — Bell numbers grow faster; $B_n \approx (n/\ln n)^n$ vs $C_n \approx 4^n / (n^{3/2}\sqrt{\pi})$
• Binomial TheoremBinomial Theorem$$(x+y)^n = \sum_{k=0}^{n} \binom{n}{k} x^k y^{n-k}$$Expanding powers of a sum via binomial coefficientsRead more → — the closed form $C_n = \binom{2n}{n}/(n+1)$ directly uses binomial coefficients
• Lucas's TheoremLucas's Theorem$$\binom{m}{n} \equiv \prod_{i} \binom{m_i}{n_i} \pmod{p}$$Binomial coefficients mod a prime p reduce digit-by-digit in base pRead more → — Lucas's theorem gives $C_p \equiv 2 \pmod{p}$ for prime $p$

import Mathlib.Combinatorics.Enumerative.Catalan

/-- The Catalan recursion: C(n+1) = ∑ᵢ C(i) * C(n-i).
    This is `catalan_succ` in Mathlib. -/
theorem catalan_recursion (n : ℕ) :
    catalan (n + 1) = ∑ i : Fin n.succ, catalan i * catalan (n - i) :=
  catalan_succ n

/-- Verify small values by computation. -/
theorem catalan_vals :
    catalan 0 = 1 ∧ catalan 1 = 1 ∧ catalan 2 = 2 ∧
    catalan 3 = 5 ∧ catalan 4 = 14 := by decide

/-- The number of Dyck words of semilength n equals C(n).
    This is `DyckWord.card_dyckWord_semilength_eq_catalan` in Mathlib. -/
theorem dyck_count_eq_catalan (n : ℕ) :
    Fintype.card { p : DyckWord // p.semilength = n } = catalan n :=
  DyckWord.card_dyckWord_semilength_eq_catalan n