Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1977P3

module

public import Mathlib.Tactic

public section


/-!
# International Mathematical Olympiad 1977, Problem 3

Given an integer n > 2, let Vₙ be the set of integers 1 + kn for k a positive integer.
A number m in Vₙ is called indecomposable if it cannot be expressed as the product of
two members of Vₙ. Prove that there is a number in Vₙ which can be expressed as the
product of indecomposable members of Vₙ in more than one way (decompositions which
differ solely in the order of factors are not regarded as different).
-/

namespace Imo1977P3

/-- The set `Vₙ` of natural numbers of the form `1 + k * n` with `k` a positive integer. -/
def Vn (n : ℕ) : Set ℕ := {m | ∃ k : ℕ, 1 ≤ k ∧ m = 1 + k * n}

/-- `m` is indecomposable in `Vₙ` if it belongs to `Vₙ` but cannot be written as a
product of two members of `Vₙ`. -/
def Indecomposable (n : ℕ) (m : ℕ) : Prop :=
  m ∈ Vn n ∧ ¬ ∃ p q : ℕ, p ∈ Vn n ∧ q ∈ Vn n ∧ m = p * q

theorem imo1977_p3 (n : ℕ) (hn : 2 < n) :
    ∃ r ∈ Vn n, ∃ F₁ F₂ : Multiset ℕ,
      (∀ d ∈ F₁, Indecomposable n d) ∧ (∀ d ∈ F₂, Indecomposable n d) ∧
      F₁.prod = r ∧ F₂.prod = r ∧ F₁ ≠ F₂ := sorry

end Imo1977P3

File author(s): Kimi K3

This problem has a complete formalized solution.