Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1994P6

import Mathlib.Tactic
import Mathlib.Data.PNat.Basic
import Mathlib.Data.Nat.Nth

/-!
# International Mathematical Olympiad 1994, Problem 6

Show that there exists a set A of positive integers with the following
property: For any infinite set S of primes there exist two positive integers
m ∈ A and n ∉ A each of which is a product of k distinct elements of S for
some k ≥ 2.

-/

namespace Imo1994P6

def IsProductOfkDistinctMembers (x : ℕ) (k : ℕ) (S : Set ℕ) : Prop :=
  ∃ S' : Finset S, S'.card = k ∧ x = ∏ p ∈ S', p.val



theorem imo1994_p6 :
  ∃ A : Set ℕ, (∀ a ∈ A, 0 < a) ∧ ∀ S : Set ℕ, Infinite S ∧ (∀ p ∈ S, p.Prime) →
    ∃ k m n : ℕ, 2 ≤ k ∧
      (m ∈ A ∧ 0 < m ∧ IsProductOfkDistinctMembers m k S) ∧
      (n ∉ A ∧ 0 < n ∧ IsProductOfkDistinctMembers n k S) := sorry

end Imo1994P6

File author(s): Markus Rydh

This problem has a complete formalized solution.