Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1985P1

import Mathlib.Tactic

/-!
# USA Mathematical Olympiad 1985, Problem 1

Determine whether or not there are any positive integral solutions of
the simultaneous equations

          x₁² + x₂² + ⋯ + x₁₉₈₅² = y³
          x₁³ + x₂³ + ⋯ + x₁₉₈₅³ = z²

with distinct integers x₁, x₂, ⋯, x₁₉₈₅.
-/

namespace Usa1985P1

/- determine -/ abbrev does_exist : Bool := sorry

abbrev is_valid (x : ℕ → ℤ) (y z : ℤ) : Prop :=
    (∀ i ∈ Finset.range 1985, 0 < x i) ∧
    0 < y ∧ 0 < z ∧
    ∑ i ∈ Finset.range 1985, x i ^ 2 = y ^ 3 ∧
    ∑ i ∈ Finset.range 1985, x i ^ 3 = z ^ 2 ∧
    ∀ i ∈ Finset.range 1985, ∀ j ∈ Finset.range 1985, i ≠ j → x i ≠ x j

theorem usa1985_p1 :
    if does_exist
    then ∃ x y z, is_valid x y z
    else ¬ ∃ x y z, is_valid x y z := sorry


end Usa1985P1

File author(s): David Renshaw

This problem has a complete formalized solution.