Compfiles/Imo2006P4.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2006, Problem 4

Determine all pairs $(x, y)$ of integers satisfying the equation $$ 1+2^{x}+2^{2 x+1}=y^{2} . $$

Imports (2)
Imported by 1 file
  1. determine Imo2006P4.solution line 39 source

    no axioms what this means

    Statement uses: Set, Prod, Int

    Proof uses: Insert.insert, Prod.mk, OfNat.ofNat, Neg.neg, Singleton.singleton

    4 instances, coercions and auxiliary constants left out.

  2. problem Imo2006P4.imo2006_p4 line 41 source

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

    Statement uses: Eq, Set, Prod, Int, Set.ofPred, Imo2006P4.imo2006_p4.match_1, Real, HAdd.hAdd, OfNat.ofNat, HPow.hPow, Nat, HMul.hMul, Imo2006P4.solution

    Proof uses: Set.ext, Iff, Membership.mem, Iff.intro, Prod.mk, GE.ge, Decidable.byContradiction, Not, Int.natAbs, LT.lt, Eq.mp, abs, Eq.trans, congr, congrArg, Nat.abs_cast, Eq.symm, Int.cast_ofNat, Int.natCast_natAbs, Iff.mp and 288 more

    370 instances, coercions and auxiliary constants left out.

    Tactic trace: 438 steps (first 200 of 438)

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