## Compfiles: Catalog Of Math Problems Formalized In Lean

## Usa1982P4

```
import Mathlib.Tactic
/-!
# USA Mathematical Olympiad 1982, Problem 4
Prove that there exists a positive integer k such that
k⬝2ⁿ + 1 is composite for every integer n.
-/
namespace Usa1982P4
theorem usa1982_p4 :
∃ k : ℕ, 0 < k ∧ ∀ n : ℕ, ¬ Prime (k * (2 ^ n) + 1) := sorry
end Usa1982P4
```

File author(s): Hongyu Ouyang

This problem has a complete formalized solution.

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