Number theory · medium

Statement, exactly as the model and Lean see it

theorem lg_target (n : ℕ) : (n ^ 2 + n) % 2 = 0 := by

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

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

Attempts

sample 0 · round 0Hallucinated theorem1.6 s model time

Proof

simp [Nat.mod_eq_mod_of_lt, Nat.pow_two, Nat.add_assoc, Nat.mul_add]

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

4:8: error: Unknown constant `Nat.mod_eq_mod_of_lt`
3:51: error: unsolved goals
n : ℕ
⊢ (n * n + n) % 2 = 0
4:43: warning: This simp argument is unused:
  Nat.add_assoc

Hint: Omit it from the simp argument list.
  [apply] simp [Nat.mod_eq_mod_of_lt, Nat.pow_two, Nat.mul_add]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
4:58: warning: This simp argument is unused:
  Nat.mul_add

Hint: Omit it from the simp argument list.
  [apply] simp [Nat.mod_eq_mod_of_lt, Nat.pow_two, Nat.add_assoc]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`

Reference proof

The proof we wrote and certified before any model ran.

have h : n ^ 2 + n = n * (n + 1) := by ring
rw [h]
exact Nat.even_iff.mp (Nat.even_mul_succ_self n)