## 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.

Open with the in-brower editor at live.lean-lang.org: