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$.

def Imo1969Q1.goodNats : Set ℕ

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

• Imo1969Q1.goodNats = {a : ℕ | ∀ (n : ℕ), ¬Nat.Prime (n ^ 4 + a)}

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) : ¬Nat.Prime 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.

def Imo1969Q1.aChoice (b : ℕ) : ℕ

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

Equations

• Imo1969Q1.aChoice b = 4 * (2 + b) ^ 4

theorem Imo1969Q1.aChoice_good (b : ℕ) : Imo1969Q1.aChoice b ∈ Imo1969Q1.goodNats

theorem Imo1969Q1.aChoice_strictMono : StrictMono Imo1969Q1.aChoice

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.