Number theory · easy

Statement, exactly as the model and Lean see it

theorem lg_target (a : ℤ) : a ^ 2 % 4 = 0 ∨ a ^ 2 % 4 = 1 := by

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

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

Attempts

sample 0 · round 0Lean 3 syntax3.2 s model time

Proof

cases a with n;
constructor;
· simp [pow, mod_eq_mod_of_divisible];
  rw [mod_eq_mod_of_divisible (div_two_mul_two_eq_self (n + 1))];
  simp [pow, mod_eq_mod_of_divisible];
· simp [pow, mod_eq_mod_of_divisible];
  rw [mod_eq_mod_of_divisible (div_two_mul_two_eq_self n)];
  simp [pow, mod_eq_mod_of_divisible];

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

4:16: error: unknown tactic
4:10: error: Invalid syntax for case analysis 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 `n`.

Reference proof

The proof we wrote and certified before any model ran.

rcases Int.even_or_odd' a with ⟨k, rfl | rfl⟩
· left; ring_nf; omega
· right; ring_nf; omega