Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1983P3

import Mathlib.Tactic

/-!
# International Mathematical Olympiad 1983, Problem 3

Let a, b, c be positive integers, no two of which have a common divisor
greater than 1. Show that 2abc − ab − bc − ca is the largest integer
which cannot be expressed in the form xbc + yca + zab, where x, y, z
are non-negative integers.
-/

namespace Imo1983P3

theorem imo1983_p3 (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
    (hab : Nat.Coprime a b) (hbc : Nat.Coprime b c) (hca : Nat.Coprime c a) :
    IsGreatest
      {n : ℤ | ¬∃ x y z : ℕ, n = x * (b * c) + y * (c * a) + z * (a * b)}
      (2 * a * b * c - a * b - b * c - c * a) := sorry

end Imo1983P3

This problem does not yet have a complete formalized solution.