Algebra · medium

Statement, exactly as the model and Lean see it

theorem lg_target (f : ℕ → ℕ) (h0 : f 0 = 1) (hs : ∀ n, f (n + 1) = 2 * f n) (n : ℕ) : f n = 2 ^ n := by

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

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

Attempts

sample 0 · round 0Syntax error2.1 s model time

Proof

induction n with d hd
· rw [h0]
  exact (pow_zero 2)
· rw [hs d, hd, pow_succ 2]
  exact rfl

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 [h0]
| succ k ih => rw [hs, ih, pow_succ]; ring