Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1970P4

import Mathlib.Tactic

/-!
# International Mathematical Olympiad 1970, Problem 4

Determine the set of all positive integers n with the property that
the set {n, n + 1, n + 2, n + 3, n + 4, n + 5} can be partitioned
into two sets such that the product of the numbers in one set
equals the product of the nubmers in the other set.
-/

namespace Imo1970P4

/- determine -/ abbrev SolutionSet : Finset ℕ+ := sorry

theorem imo1970_p4 (n : ℕ+) :
    n ∈ SolutionSet ↔
      ∃ s1 s2 : Finset ℕ,
        s1 ∪ s2 = Finset.Icc n.val (n.val + 5) ∧
        s1 ∩ s2 = ∅ ∧
        ∏ m ∈ s1, m = ∏ m ∈ s2, m := sorry


end Imo1970P4

File author(s): David Renshaw

This problem does not yet have a complete formalized solution.