Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2019P5

module

public import Mathlib.Algebra.CharP.Defs
public import Mathlib.Algebra.Ring.IsFormallyReal
public import Mathlib.Analysis.Normed.Field.Lemmas
public import Mathlib.Data.Int.ModEq
public import Mathlib.Data.Nat.Factorization.Basic
public import Mathlib.Data.Nat.Prime.Int
public import Mathlib.Tactic.LinearCombination
public import Mathlib.Tactic.LinearCombination.Lemmas

public section


/-!
# USA Mathematical Olympiad 2019, Problem 5

Let m and n be relatively prime positive integers. The numbers m/n and n/m are
written on a blackboard. At any point, Evan may pick two of the numbers x and y
written on the board and write either their arithmetic mean (x+y)/2 or their
harmonic mean 2xy/(x+y). For which (m, n) can Evan write 1 on the board in
finitely many steps?
-/

namespace Usa2019P5

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

theorem usa2019_p5 (m n : ℕ) (hm : 0 < m) (hn : 0 < n) (hmn : m.Coprime n) :
    (m, n) ∈ solution_set ↔ Writable m n 1 := sorry

end Usa2019P5

File author(s): Kimi K3

This problem has a complete formalized solution.