Documentation

Archive.Imo.Imo1969Q1

IMO 1969 Q1 #

Prove that there are infinitely many natural numbers $a$ with the following property: the number $z = n^4 + a$ is not prime for any natural number $n$.

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 : ℕ.

Equations
Instances For

    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.

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

    To show that the product is not prime, we need to show each of the factors is at least 2, which nlinarith can solve since they are each expressed as a sum of squares.

    theorem Imo1969Q1.left_factor_large {m : } (n : ) (h : 1 < m) :
    1 < (n - m) ^ 2 + m ^ 2
    theorem Imo1969Q1.right_factor_large {m : } (n : ) (h : 1 < m) :
    1 < (n + m) ^ 2 + m ^ 2

    The factorization is over the integers, but we need the nonprimality over the natural numbers.

    theorem Imo1969Q1.int_large {m : } (h : 1 < m) :
    1 < m.natAbs
    theorem Imo1969Q1.not_prime_of_int_mul' {m : } {n : } {c : } (hm : 1 < m) (hn : 1 < n) (hc : m * n = c) :
    theorem Imo1969Q1.polynomial_not_prime {m : } (h1 : 1 < m) (n : ) :
    ¬Nat.Prime (n ^ 4 + 4 * m ^ 4)

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

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

    Equations
    Instances For

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

      theorem imo1969_q1 :
      {a : | ∀ (n : ), ¬Nat.Prime (n ^ 4 + a)}.Infinite

      We conclude by using the fact that aChoice is an injective function from the natural numbers to the set goodNats.