Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1986P6

module

public import Mathlib.Tactic

public section


/-!
# International Mathematical Olympiad 1986, Problem 6

Given a finite set of points in the plane, each with integer coordinates,
is it always possible to color the points red or white so that for any
straight line L parallel to one of the coordinate axes the difference
(in absolute value) between the numbers of white and red points on L
is not greater than 1?
-/

namespace Imo1986P6

open Finset

/- determine -/ abbrev does_exist : Bool := sorry

/-- **IMO 1986, Problem 6.**  Given a finite set `S` of points in the plane with
integer coordinates, the points can be colored red or white so that on every
line parallel to one of the coordinate axes the numbers of white and red points
differ by at most one.

We encode the coloring by a sign function `ε : ℤ × ℤ → ℤ` with values in
`{1, -1}` (`1` = white, `-1` = red); the sum of `ε` over the points of `S` on a
line is then exactly the difference between the numbers of white and red points
on that line. -/
theorem imo1986_p6 (S : Finset (ℤ × ℤ)) :
    if does_exist then
      ∃ ε : ℤ × ℤ → ℤ,
        (∀ p ∈ S, ε p = 1 ∨ ε p = -1) ∧
        (∀ x : ℤ, |∑ p ∈ S.filter (fun p => p.1 = x), ε p| ≤ 1) ∧
        (∀ y : ℤ, |∑ p ∈ S.filter (fun p => p.2 = y), ε p| ≤ 1)
    else
      ¬ ∃ ε : ℤ × ℤ → ℤ,
        (∀ p ∈ S, ε p = 1 ∨ ε p = -1) ∧
        (∀ x : ℤ, |∑ p ∈ S.filter (fun p => p.1 = x), ε p| ≤ 1) ∧
        (∀ y : ℤ, |∑ p ∈ S.filter (fun p => p.2 = y), ε p| ≤ 1) := sorry

end Imo1986P6

File author(s): Kimi K3

This problem has a complete formalized solution.