import Mathlib.Tactic

/-!
# International Mathematical Olympiad 2015, Problem 2

Determine all triples of positive integers a, b, c such that each of
ab - c, bc - a, ca - b is a power of two.
-/

namespace Imo2012P2

/- determine -/ abbrev solution_set : Set (ℤ × ℤ × ℤ) := sorry

def is_power_of_two (n : ℤ) : Prop := ∃ m : ℕ, n = 2 ^ m

theorem imo2015_p2 (a b c : ℤ) :
    (a,b,c) ∈ solution_set ↔
      0 < a ∧ 0 < b ∧ 0 < c ∧
      is_power_of_two (a * b - c) ∧
      is_power_of_two (b * c - a) ∧
      is_power_of_two (c * a - b) := sorry

This problem does not yet have a complete solution.