Algebra · medium

Statement, exactly as the model and Lean see it

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

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

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.00011

Attempts

sample 0 · round 0Lean 3 syntax6.7 s model time

Proof

induction n with d hd,
  { simp [Finset.range, Finset.sum], },
  { have : ∑ i ∈ Finset.range (d + 1), (2 * i + 1) = (d + 1) ^ 2 := hd,
    rw [Finset.range_eq_insert (Finset.range d) (d : ℕ)],
    simp only [Finset.sum_insert, Finset.sum_range_add_const, Finset.sum_range_succ],
    rw [Nat.add_right_inj, Nat.add_assoc, Nat.add_comm],
    rw [Nat.add_one, Nat.pow_succ, Nat.mul_add, Nat.add_mul, Nat.add_assoc, Nat.add_left_comm],
    congr' at hd,
    rw [hd],
    ring,
  }

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

4:20: error: unknown tactic
4:14: error: Invalid syntax for induction tactic: The `with` keyword must be followed by a tactic or by an alternative (e.g. `| zero =>`), but here it is followed by the identifier `d`.

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]
  ring