Inequalities · medium

Statement, exactly as the model and Lean see it

theorem lg_target (n : ℕ) (hn : 1 ≤ n) : n + 1 ≤ 2 ^ n := by

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

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

Attempts

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

Proof

induction n with d hd,
  { intro h, rw [pow_zero], exact le_refl (n + 1) },
  { have h1 : 2 * 2 ^ d = 2 ^ (d + 1) := by rw [pow_add, mul_comm, pow_one],
    calc
      (d + 1) + 1 ≤ 2 * (d + 1) : add_le_add_right (le_reflect (d + 1) 2) _
    ... ≤ 2 * 2 ^ d : mul_le_mul_left (hd d) 2
    ... = 2 ^ (d + 1) : h1 }

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, hn using Nat.le_induction with
| base => norm_num
| succ k hk ih => rw [pow_succ]; omega