Documentation

Archive.Imo.Imo2008Q3

IMO 2008 Q3 #

Prove that there exist infinitely many positive integers n such that n^2 + 1 has a prime divisor which is greater than 2n + √(2n).

Solution #

We first prove the following lemma: for every prime p > 20, satisfying p ≡ 1 [MOD 4], there exists n ∈ ℕ such that p ∣ n^2 + 1 and p > 2n + √(2n). Then the statement of the problem follows from the fact that there exist infinitely many primes p ≡ 1 [MOD 4].

To prove the lemma, notice that p ≡ 1 [MOD 4] implies ∃ n ∈ ℕ such that n^2 ≡ -1 [MOD p] and we can take this n such that n ≤ p/2. Let k = p - 2n ≥ 0. Then we have: k^2 + 4 = (p - 2n)^2 + 4 ≣ 4n^2 + 4 ≡ 0 [MOD p]. Then k^2 + 4 ≥ p and so k ≥ √(p - 4) > 4. Then p = 2n + k ≥ 2n + √(p - 4) = 2n + √(2n + k - 4) > √(2n) and we are done.

theorem Imo2008Q3.p_lemma (p : ) (hpp : Nat.Prime p) (hp_mod_4_eq_1 : p 1 [MOD 4]) (hp_gt_20 : p > 20) :
∃ (n : ), p n ^ 2 + 1 p > 2 * n + (2 * n)
theorem imo2008_q3 (N : ) :
nN, ∃ (p : ), Nat.Prime p p n ^ 2 + 1 p > 2 * n + (2 * n)