Compfiles/Imo1969P1.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def Imo1969P1.goodNats goodNats is the set of natural numbers satisfying the condition in the problem statement, namely the a : ℕ such that n^4 + a is not prime for any n : ℕ line 38 source

   Source documentation

   goodNats is the set of natural numbers satisfying the condition in the problem statement, namely the a : ℕ such that n^4 + a is not prime for any n : ℕ.

   standard axioms: propext what this means

   Statement uses: Set, Nat

   Proof uses: Set.ofPred, Not, Nat.Prime, HAdd.hAdd, HPow.hPow, OfNat.ofNat

   7 instances, coercions and auxiliary constants left out.

   def goodNats : Set ℕ :=
   …

2. theorem Imo1969P1.factorization The key to the solution is that you can factor $z$ into the product of two polynomials, if $a = 4*m^4$ line 46 source

   Source documentation

   The key to the solution is that you can factor $z$ into the product of two polynomials, if $a = 4*m^4$. This is Sophie Germain's identity, called pow_four_add_four_mul_pow_four in mathlib.

   standard axioms: Quot.sound, propext what this means

   Statement uses: Int, Eq, HMul.hMul, HAdd.hAdd, HPow.hPow, Nat, HSub.hSub, OfNat.ofNat

   Proof uses: Eq.symm, pow_four_add_four_mul_pow_four

   36 instances, coercions and auxiliary constants left out.

   theorem factorization {m n : ℤ} :
       ((n - m) ^ 2 + m ^ 2) * ((n + m) ^ 2 + m ^ 2) = n ^ 4 + 4 * m ^ 4 :=
   …

3. theorem Imo1969P1.left_factor_large line 55 source

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

   Statement uses: Int, LT.lt, OfNat.ofNat, HAdd.hAdd, HPow.hPow, Nat, HSub.hSub

   Proof uses: lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HMul.hMul, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, inferInstance, Ring, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.Common.neg_congr and 65 more

   100 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

4. theorem Imo1969P1.right_factor_large line 56 source

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

   Statement uses: Int, LT.lt, OfNat.ofNat, HAdd.hAdd, HPow.hPow, Nat

   Proof uses: lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HMul.hMul, 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, Int.negOfNat, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl and 66 more

   97 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

5. theorem Imo1969P1.int_large line 62 source

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

   Statement uses: Int, LT.lt, OfNat.ofNat, Nat, Int.natAbs

   Proof uses: cast, Eq.trans, congrFun', congrArg, Eq.symm, Nat.cast_one, lt_of_lt_of_le, Int.le_natAbs

   23 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

6. theorem Imo1969P1.not_prime_of_int_mul' line 65 source

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

   Statement uses: Int, Nat, LT.lt, OfNat.ofNat, Eq, HMul.hMul, Not, Nat.Prime

   Proof uses: Int.not_prime_of_int_mul, LT.lt.ne', Int.natAbs, Imo1969P1.int_large

   14 instances, coercions and auxiliary constants left out.

7. theorem Imo1969P1.polynomial_not_prime Every natural number of the form n^4 + 4*m^4 is not prime line 70 source

   Source documentation

   Every natural number of the form n^4 + 4*m^4 is not prime.

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

   Statement uses: Nat, LT.lt, OfNat.ofNat, Not, Nat.Prime, HAdd.hAdd, HPow.hPow, HMul.hMul

   Proof uses: Int, Iff.mpr, Int.ofNat_lt, Imo1969P1.not_prime_of_int_mul', HSub.hSub, Imo1969P1.left_factor_large, Imo1969P1.right_factor_large, Imo1969P1.factorization

   28 instances, coercions and auxiliary constants left out.

   Tactic trace: 3 steps

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

   theorem polynomial_not_prime {m : ℕ} (h1 : 1 < m) (n : ℕ) : ¬Nat.Prime (n ^ 4 + 4 * m ^ 4) := by
   …

8. def Imo1969P1.aChoice We define $a_{choice}(b) := 4*(2+b)^4$, so that we can take $m = 2+b$ in polynomial_not_prime line 77 source

   Source documentation

   We define $a_{choice}(b) := 4*(2+b)^4$, so that we can take $m = 2+b$ in polynomial_not_prime.

   standard axioms: propext what this means

   Statement uses: Nat

   Proof uses: HMul.hMul, OfNat.ofNat, HPow.hPow, HAdd.hAdd

   9 instances, coercions and auxiliary constants left out.

   def aChoice (b : ℕ) : ℕ := 4 * (2 + b) ^ 4

9. theorem Imo1969P1.aChoice_good line 79 source

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

   Statement uses: Nat, Membership.mem, Set, Imo1969P1.goodNats, Imo1969P1.aChoice

   Proof uses: Imo1969P1.polynomial_not_prime, HAdd.hAdd, OfNat.ofNat, LT.lt

   6 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

10. theorem Imo1969P1.aChoice_strictMono aChoice is a strictly monotone function; this is easily proven by chaining together lemmas in the strictMono namespace line 84 source

    Source documentation

    aChoice is a strictly monotone function; this is easily proven by chaining together lemmas in the strictMono namespace.

    standard axioms: propext what this means

    Statement uses: StrictMono, Nat, Imo1969P1.aChoice

    Proof uses: StrictMono.const_mul, OfNat.ofNat, HPow.hPow, HAdd.hAdd, id, StrictMono.nat_pow, of_decide_eq_true, Ne, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, StrictMono.const_add, strictMono_id, LT.lt

    29 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

    theorem aChoice_strictMono : StrictMono aChoice :=
    …

    Mentions: Imo1969P1.aChoice

11. problem Imo1969P1.imo1969_p1 line 92 source

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

    Statement uses: Set.Infinite, Nat, Set.ofPred, Not, Nat.Prime, HAdd.hAdd, HPow.hPow, OfNat.ofNat

    Proof uses: Set.infinite_of_injective_forall_mem, Imo1969P1.aChoice, StrictMono.injective, Imo1969P1.aChoice_strictMono, Imo1969P1.aChoice_good

    17 instances, coercions and auxiliary constants left out.