Number theory · medium

Statement, exactly as the model and Lean see it

theorem lg_target (hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p) : FermatLastTheorem := by

Mathlib declaration: FermatLastTheorem.of_odd_primes
Held-out module: Mathlib.NumberTheory.FLT.Four
Banned modules (itself + downstream): 1
Reference proof premises (reachable / held-out): 6 / 1

Traces

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

No configuration has attempted this theorem yet.

Reference proof

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

/--
To prove Fermat's Last Theorem, it suffices to prove it for odd prime exponents.
-/
theorem FermatLastTheorem.of_odd_primes
    (hprimes : ∀ p : ℕ, Nat.Prime p → Odd p → FermatLastTheoremFor p) : FermatLastTheorem := by
  intro n h
  obtain hdvd | ⟨p, hpprime, hdvd, hpodd⟩ := Nat.four_dvd_or_exists_odd_prime_and_dvd_of_two_lt h
    <;> apply FermatLastTheoremWith.mono hdvd
  · exact fermatLastTheoremFour
  · exact hprimes p hpprime hpodd