Algebra · hard

Statement, exactly as the model and Lean see it

theorem lg_target (n : ℕ) : ∑ i ∈ Finset.range (n + 1), (i : ℚ) = n * (n + 1) / 2 := by

Source: Written for LeanGraph, reference proof certified
Premises used by the reference proof: 44

Traces

Each configuration's full record: what was retrieved, what the model wrote, what Lean said back.

Not verified1 model calls · 1 Lean checks · $0.00008

Attempts

sample 0 · round 0Syntax error3.4 s model time

Proof

have h : ∑ i in Finset.range (n + 1), (i : ℚ) = ∑ i in Finset.range (n + 1), i :=
  congrArg _ (cast_additive (Finset.range (n + 1)) (ℚ) ℕ)
rw [h]
simp only [Finset.sum_range, Nat.cast_add, Nat.cast_one, Nat.cast_zero]
ring

What Lean printed (this is all the model sees on repair)

4:14: error: unexpected token 'in'; expected ','
4:11: error: failed to synthesize instance of type class
  AddCommMonoid (Sort ?u.27)

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
3:85: error: unsolved goals
case h
n : ℕ
⊢ sorry

n : ℕ
h : sorry
⊢ ∑ i ∈ Finset.range (n + 1), ↑i = ↑n * (↑n + 1) / 2

Reference proof

The proof we wrote and certified before any model ran.

induction n with
| zero => simp
| succ k ih =>
  rw [Finset.sum_range_succ, ih]
  push_cast
  ring