# 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) :
¬c.Prime
theorem Imo1969Q1.polynomial_not_prime {m : } (h1 : 1 < m) (n : ) :
¬(n ^ 4 + 4 * m ^ 4).Prime

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 : ), ¬(n ^ 4 + a).Prime}.Infinite

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