Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1991P3

import Mathlib.Tactic

/-!
# International Mathematical Olympiad 1991, Problem 3

Let S = {1, 2, ..., 280}. Find the smallest natural number n such
that every n-element subset of S contains five numbers which are
pairwise relatively prime.
-/

namespace Imo1991P3

/- determine -/ abbrev solution : ℕ := sorry

theorem imo1991_p3 :
    IsLeast
      {n : ℕ | ∀ T ⊆ Finset.Icc 1 280, T.card = n →
        ∃ U ⊆ T, U.card = 5 ∧ (U : Set ℕ).Pairwise Nat.Coprime}
      solution := sorry

end Imo1991P3

This problem does not yet have a complete formalized solution.