Pigeonhole Argument

Prove that something must exist because there are more items than categories.

The Pigeonhole Principle

If you put n+1 pigeons into n boxes, at least one box contains 2+ pigeons.

Sounds trivial, but it's surprisingly powerful:

• •Prove there exist two people in London with the same number of hairs
• •Prove in any group of 6 people, either 3 are mutual friends or 3 are mutual strangers
• •Prove that some Fibonacci number is divisible by 1000

Step 1: Identify the Setup

• • What are the "pigeons"? (items being placed)
• • What are the "holes"? (categories/boxes)
• • Why are there more pigeons than holes?

Step 2: Formalize the Argument

• • Define the mapping: how does each pigeon go into a hole?
• • Count pigeons: prove there are n+1 (or more)
• • Count holes: prove there are at most n
• • Apply pigeonhole: conclude some hole has 2+ pigeons

Tools to use:

• •symbolic_compute: Count sizes
• •lean_prover: Formalize with Finset.card and pigeonhole lemmas

Step 3: Extract the Conclusion

The pigeonhole gives you: "some hole has 2+ pigeons"

Translate this back:

• • What does "same hole" mean for the original problem?
• • What property do items sharing a hole have?
• • State the existence result

Step 4: Lean Formalization

Key lemmas in Mathlib:

• •Fintype.exists_ne_map_eq_of_card_lt - basic pigeonhole
• •Finset.exists_lt_card_fiber_of_mul_lt_card - generalized pigeonhole

-- If |A| > |B|, any f : A → B has a collision
example (h : Fintype.card A > Fintype.card B) (f : A → B) :
    ∃ a₁ a₂, a₁ ≠ a₂ ∧ f a₁ = f a₂ := by
  exact Fintype.exists_ne_map_eq_of_card_lt h f

Common Patterns