Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1976P3

import Mathlib.Tactic
import Mathlib.Data.Int.Basic
import Mathlib.Data.Set.Insert
import Mathlib.Algebra.Group.Even

/-!
# USA Mathematical Olympiad 1976, Problem 3

Determine all integral solutions of a² + b² + c² = a²b².
-/

namespace Usa1976P3

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

theorem usa1976_p3 (a b c : ℤ) :
    a^2 + b^2 + c^2 = a^2 * b^2 ↔ ⟨a,b,c⟩ ∈ solution_set := sorry

end Usa1976P3

File author(s): Maximiliano Onofre Martínez

This problem has a complete formalized solution.