Number theory · easy

Statement, exactly as the model and Lean see it

theorem lg_target {a b : ℤ} : a.natAbs = b.natAbs ↔ a * a = b * b := by

Mathlib declaration: Int.natAbs_eq_iff_mul_self_eq
Held-out module: Mathlib.Data.Int.Order.Lemmas
Banned modules (itself + downstream): 2
Reference proof premises (reachable / held-out): 3 / 0

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

Proof

intro h
split
· rw [h]
· rw [natAbs_mul_self]
  rw [natAbs_mul_self at h]
  rw [h]

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

8:23: error: unexpected token 'at'; expected ']'

Reference proof

Mathlib's own source for this declaration, shown for comparison. It may use lemmas the prover is not allowed to use.

theorem natAbs_eq_iff_mul_self_eq {a b : ℤ} : a.natAbs = b.natAbs ↔ a * a = b * b := by
  rw [← abs_eq_iff_mul_self_eq, abs_eq_natAbs, abs_eq_natAbs]
  exact Int.natCast_inj.symm