Compfiles/Imo2008P3.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2008, Problem 3

Prove that there exist infinitely many positive integers n such that n^2 + 1 has a prime divisor which is greater than 2n + √(2n).

Imports (7)
Imported by 1 file
  1. theorem Imo2008P3.p_lemma line 49 source

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

    Statement uses: Nat, Nat.Prime, Nat.ModEq, OfNat.ofNat, GT.gt, Exists, And, Dvd.dvd, HAdd.hAdd, HPow.hPow, Real, HMul.hMul, Real.sqrt

    Proof uses: Fact, Fact.mk, Ne, HMod.hMod, Not.intro, Eq, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, LT.lt, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, inferInstance, Ring, Int.rawCast and 111 more

    179 instances, coercions and auxiliary constants left out.

    Tactic trace: 43 steps

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

  2. problem Imo2008P3.imo2008_p3 line 88 source

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

    Statement uses: Nat, Exists, And, GE.ge, Nat.Prime, Dvd.dvd, HAdd.hAdd, HPow.hPow, OfNat.ofNat, GT.gt, Real, HMul.hMul, Real.sqrt

    Proof uses: LT.lt, Nat.ModEq, Nat.exists_prime_gt_modEq_one, four_ne_zero, Imo2008P3.p_lemma, Nat.le_of_dvd, Nat.succ_pos, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat and 72 more

    103 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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