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 numbers 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, Adam Kurkiewicz

This problem has a complete formalized solution.