Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1972P1

import Mathlib.Data.Nat.Factorization.Basic

/-!
# USA Mathematical Olympiad 1972, Problem 1

Let (a, b, ... , k) denote the greatest common divisor of the integers a, b, ... k
and [a, b, ... , k] denote their least common multiple.

Show that for any positive integers a, b, c we have
(a, b, c)² [a, b] [b, c] [c, a] = [a, b, c]² (a, b) (b, c) (c, a).
-/

namespace Usa1972P1

open Nat

theorem usa1972_p1 (a b c : ℕ) :
  (gcd a (gcd b c)) ^ 2 * lcm a b * lcm b c * lcm c a =
  (lcm a (lcm b c)) ^ 2 * gcd a b * gcd b c * gcd c a := sorry

end Usa1972P1

File author(s): Shalev Wengrowsky

This problem has a complete formalized solution.