Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1992P1

import Mathlib.Tactic

/-!
# International Mathematical Olympiad 1992, Problem 1

Find all integers 1 < a < b < c such that
(a - 1)(b - 1)(c - 1) divides abc - 1.
-/

namespace Imo1992P1

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

theorem imo1992_p1 (a b c : ℤ) (ha : 1 < a) (hb : a < b) (hc : b < c) :
    ⟨a, b, c⟩ ∈ solution_set ↔
    (a - 1) * (b - 1) * (c - 1) ∣ a * b * c - 1 := sorry


end Imo1992P1

File author(s): David Renshaw

This problem does not yet have a complete formalized solution.