メニュー
Prove existence using the pigeonhole principle - when n+1 items go into n categories, some category has multiple items. Triggers on "must exist", "at least two", "some pair", "among any n", "prove existence of duplicate/collision"
Codex または Claude でインストール この Prompt をコピーして Codex、Claude、または他のアシスタントに貼り付けると、Skill ページを確認してインストールできます。
SOC 職業分類に基づく
Explore a mathematical conjecture - gather evidence, find counterexamples, or build toward a proof. Triggers on "explore", "investigate", "what if", "is it true that", "find pattern", "check if"
Determine convergence or divergence of series using ratio test, root test, comparison test, and integral test. Triggers on "series converges", "test for convergence", "ratio test", "root test", "comparison test", "integral test", "sum of 1/n"
Prove geometric theorems using coordinate geometry. Convert shapes to algebraic expressions, use distance formula, midpoint formula, and slope calculations. Triggers on "prove using coordinates", "analytic geometry", "distance formula", "show collinear", "prove perpendicular", "prove parallel"
Prove identities or existence using combinatorial counting - double counting, bijections, inclusion-exclusion. Triggers on "count", "number of ways", "how many", "bijection", "one-to-one correspondence", "combinatorial proof"
Prove statements directly by assuming the hypothesis and deriving the conclusion through logical steps. Triggers on "prove directly", "show that", "demonstrate", "verify", "simple proof"
Prove limit statements using epsilon-delta definitions. Triggers on "epsilon-delta", "limit", "prove continuous", "show limit equals", "formal limit proof"
| name | pigeonhole-argument |
| description | Prove existence using the pigeonhole principle - when n+1 items go into n categories, some category has multiple items. Triggers on "must exist", "at least two", "some pair", "among any n", "prove existence of duplicate/collision" |
Prove that something must exist because there are more items than categories.
If you put n+1 pigeons into n boxes, at least one box contains 2+ pigeons.
Sounds trivial, but it's surprisingly powerful:
| Question | Answer |
|---|---|
| Pigeons | [what objects] |
| Holes | [what categories] |
| Count | [n+1 pigeons, n holes] |
symbolic_compute: Count sizeslean_prover: Formalize with Finset.card and pigeonhole lemmasThe pigeonhole gives you: "some hole has 2+ pigeons"
Translate this back:
Key lemmas in Mathlib:
Fintype.exists_ne_map_eq_of_card_lt - basic pigeonholeFinset.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
| Pattern | Pigeons | Holes |
|---|---|---|
| Residues | Numbers | Remainders mod n |
| Graph coloring | Edges | Colors |
| Birthdays | People | Days of year |
| Subsets | Subsets of {1,...,n} | Possible sums |