Number theory · medium

Statement, exactly as the model and Lean see it

theorem lg_target (n : ℕ) : Nat.gcd (2 * n + 1) (n + 1) = 1 := by

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

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.6 s model time

Proof

induction n with d hd
· exact Nat.gcd 1 2 = 1
· have h : Nat.gcd (2 * d + 1) (d + 1) = 1 := hd
  have h1 : Nat.gcd (2 * (d + 1) + 1) (d + 2) = 1 :=
    by rw [Nat.gcd_eq_gcd_of_gcd_eq_gcd]
      exact Nat.gcd (2 * d + 1) (d + 1) = 1
  rw [Nat.gcd_eq_gcd_of_gcd_eq_gcd] at h1
  exact 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.

have : 2 * n + 1 = n + (n + 1) := by ring
rw [this, Nat.gcd_add_self_left]
simp