Number theory · easy

Statement, exactly as the model and Lean see it

theorem lg_target (p : ℕ) (hp : p.Prime) (h2 : p ≠ 2) : Odd p := 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.00027

Retrieved lemmas

1. Nat.Prime.odd_of_ne_two
2. Nat.Prime.eq_two_or_odd'
3. Nat.Prime.even_sub_one
4. Nat.Prime.eq_two_or_odd
5. Nat.Prime.odd_iff
6. Nat.Prime.five_le_of_ne_two_of_ne_three
7. quadraticChar_odd_prime
8. ZMod.exists_sq_eq_neg_two_iff

Plan

### Explanation of the Proof: The goal is to prove that a prime number `p` (different from 2) is odd. This is a basic number theory result. In Lean's Mathlib, there is a lemma `Nat.Prime.odd_of_ne_two` which directly states that if `p` is a prime and `p ≠ 2`, then `p` is odd. Therefore, the proof is very straightforward: we simply apply this lemma. --- ### Lean Proof Skeleton: This proof uses the direct lemma `Nat.Prime.odd_of_ne_two` to show that `p` is odd given that it is a prime and not equal to 2.

Skeleton — Lean accepts it with only sorry steps left

have h_odd : Odd p := Nat.Prime.odd_of_ne_two hp h2
exact h_odd

Attempts

sample 0 · round 0Verified2.1 s model time

Proof

have h_odd : Odd p := Nat.Prime.odd_of_ne_two hp h2
exact h_odd

Verified proof

theorem lg_target (p : ℕ) (hp : p.Prime) (h2 : p ≠ 2) : Odd p := by
  have h_odd : Odd p := Nat.Prime.odd_of_ne_two hp h2
  exact h_odd

Axioms used: propext

Reference proof

The proof we wrote and certified before any model ran.

exact hp.odd_of_ne_two h2