## Compfiles: Catalog Of Math Problems Formalized In Lean

## Imo1969P1

```
import Mathlib.Algebra.Ring.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
```

File author(s): Kevin Lacker

This problem has a complete formalized solution.

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

Open with the in-brower editor at live.lean-lang.org: