Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1996P6

import Mathlib.Data.Int.Basic

/-!
# USA Mathematical Olympiad 1996, Problem 6

Determine, with proof, whether there is a subset X of the integers with
the following property: for any integer n there is exactly one pair (a, b)
of elements of X satisfying a + 2b = n.
-/

namespace Usa1996P6

def UniqueRepresentationSet (X : Set ℤ) : Prop :=
  ∀ n : ℤ, ∃! p : ℤ × ℤ,
    p.1 ∈ X ∧ p.2 ∈ X ∧ p.1 + 2 * p.2 = n

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

theorem usa1996_p6 :
    does_exist ↔ ∃ X : Set ℤ, UniqueRepresentationSet X := sorry

end Usa1996P6

File author(s): Karl Mehltretter

This problem does not yet have a complete formalized solution.