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

File author(s): Hongyu Ouyang

This problem has a complete formalized solution.

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