Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1971P3

import Mathlib.Tactic

/-!
# International Mathematical Olympiad 1971, Problem 3

Prove that we can find an infinite set of positive integers of the form 2^n - 3
(where n is a positive integer) every pair of which are relatively prime.
-/

namespace Imo1971P3

theorem imo1971_p3 :
   ∃ s : Set ℕ+,
     s.Infinite ∧
     s.Pairwise fun m n ↦ Nat.Coprime (2 ^ n.val - 3) (2 ^ m.val - 3) := sorry


end Imo1971P3

File author(s): InternLM-MATH LEAN Formalizer v0.1

This problem does not yet have a complete formalized solution.