Number theory · easy

Statement, exactly as the model and Lean see it

theorem lg_target (z : ZMod 4) : z * z ≠ 2 := by

Mathlib declaration: sq_ne_two_fin_zmod_four
Held-out module: Mathlib.NumberTheory.PythagoreanTriples
Banned modules (itself + downstream): 2
Reference proof premises (reachable / held-out): 2 / 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.00004

Attempts

sample 0 · round 0Wrong tactic1.3 s model time

Proof

intro h; cases z; intro h; contradiction

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

4:26: error: Tactic `introN` failed: There are no additional binders or `let` bindings in the goal to introduce

case mk
val✝ : ℕ
isLt✝ : val✝ < 3 + 1
h : ⟨val✝, isLt✝⟩ * ⟨val✝, isLt✝⟩ = 2
⊢ False

Reference proof

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

theorem sq_ne_two_fin_zmod_four (z : ZMod 4) : z * z ≠ 2 := by
  change Fin 4 at z
  fin_cases z <;> decide