Compfiles/Usa2022P4.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2022, Problem 4

Determine all pairs of primes (p, q) where p - q and pq - q are both perfect squares.

Imports (2)
Imported by 1 file
  1. determine Usa2022P4.solution_set line 26 source

    no axioms what this means

    Statement uses: Set, Prod, Nat

    Proof uses: Singleton.singleton, Prod.mk, OfNat.ofNat

    2 instances, coercions and auxiliary constants left out.

  2. problem Usa2022P4.usa2022_p4 line 28 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Iff, Membership.mem, Prod, Set, Usa2022P4.solution_set, Prod.mk, And, Nat.Prime, Exists, Eq, HAdd.hAdd, HPow.hPow, OfNat.ofNat, HMul.hMul

    Proof uses: Iff.intro, HEq, Eq.refl, And.intro, Mathlib.Meta.NormNum.isNat_prime_2, Mathlib.Meta.NormNum.isNat_ofNat, Bool, Bool.true, Mathlib.Meta.NormNum.isNat_minFac_4, Mathlib.Meta.NormNum.IsNat.raw_refl, Mathlib.Meta.NormNum.minFacHelper_0, Bool.false, Mathlib.Meta.NormNum.isNat_minFac_2, Exists.intro, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_add, Mathlib.Meta.NormNum.isNat_pow, Mathlib.Meta.NormNum.one_natPow, Mathlib.Meta.NormNum.IsNatPowT.run, Mathlib.Meta.NormNum.IsNatPowT.bit0 and 148 more

    153 instances, coercions and auxiliary constants left out.

    Tactic trace: 97 steps

    Open to load the checked before-and-after goal states.