mathlib3 documentation

mathlib-archive / imo.imo1969_q1

IMO 1969 Q1 #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 imo1969_q1.good_nats :

good_nats 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

imo1969_q1.good_nats = {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 imo1969_q1.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 imo1969_q1.left_factor_large {m : ℤ} (n : ℤ) (h : 1 < m) :

1 < (n - m) ^ 2 + m ^ 2

theorem imo1969_q1.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 imo1969_q1.int_large {m : ℤ} (h : 1 < m) :

theorem imo1969_q1.not_prime_of_int_mul' {m n : ℤ} {c : ℕ} (hm : 1 < m) (hn : 1 < n) (hc : m * n = ↑c) :

theorem imo1969_q1.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 imo1969_q1.a_choice (b : ℕ) :

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

Equations

imo1969_q1.a_choice b = 4 * (2 + b) ^ 4

theorem imo1969_q1.a_choice_good (b : ℕ) :

imo1969_q1.a_choice b ∈ imo1969_q1.good_nats

theorem imo1969_q1.a_choice_strict_mono :

strict_mono imo1969_q1.a_choice

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

theorem imo1969_q1 :

{a : ℕ | ∀ (n : ℕ), ¬nat.prime (n ^ 4 + a)}.infinite

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