Number theory · medium

Statement, exactly as the model and Lean see it

theorem lg_target (a b : ℤ) (h : a ≡ b [ZMOD 5]) : a ^ 2 ≡ b ^ 2 [ZMOD 5] := by

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

Traces

Each configuration's full record: what was retrieved, what the model wrote, what Lean said back.

Verified2 model calls · 2 Lean checks · $0.00030

Retrieved lemmas

1. Int.ModEq.pow
2. Int.ModEq.mul
3. Int.ModEq.add
4. Int.ModEq.sub
5. Int.ModEq.of_mul_left
6. Int.ModEq.neg
7. Int.ModEq.mul_left
8. Int.ModEq.trans

Plan

### Explanation of the Proof: We are given that `a ≡ b [ZMOD 5]`, and we want to show that `a^2 ≡ b^2 [ZMOD 5]`. This can be done using the lemma `Int.ModEq.pow`, which states that if `a ≡ b [ZMOD n]`, then `a^m ≡ b^m [ZMOD n]` for any natural number `m`. Since we're raising both sides to the power of 2, we can directly apply this lemma with `m = 2` and `n = 5`. --- ### Lean Proof Skeleton: This proof uses the `Int.ModEq.pow` lemma directly to establish the result.

Skeleton — Lean accepts it with only sorry steps left

have h_pow : a ^ 2 ≡ b ^ 2 [ZMOD 5] := Int.ModEq.pow 2 h
exact h_pow

Attempts

sample 0 · round 0Verified1.6 s model time

Proof

have h_pow : a ^ 2 ≡ b ^ 2 [ZMOD 5] := Int.ModEq.pow 2 h
exact h_pow

Verified proof

theorem lg_target (a b : ℤ) (h : a ≡ b [ZMOD 5]) : a ^ 2 ≡ b ^ 2 [ZMOD 5] := by
  have h_pow : a ^ 2 ≡ b ^ 2 [ZMOD 5] := Int.ModEq.pow 2 h
  exact h_pow

Axioms used: propext, Classical.choice, Quot.sound

Reference proof

The proof we wrote and certified before any model ran.

exact h.pow 2