import Mathlib.Algebra.GroupPower.Identities
import Mathlib.Data.Int.NatPrime
import Mathlib.Tactic.Linarith
import Mathlib.Data.Set.Finite

/-!
# International Mathematical Olympiad 1969, Problem 1

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

open Int Nat

namespace Imo1969P1

theorem imo1969_p1 : Set.Infinite {a : ℕ | ∀ n : ℕ, ¬Nat.Prime (n ^ 4 + a)} := sorry

This problem has a complete solution written by Kevin Lacker.

The solution was imported from mathlib4/Archive/Imo/Imo1969Q1.lean.