Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2006P4

module

public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Analysis.MeanInequalities
public import Mathlib.Data.Rat.Star
public import Mathlib.NumberTheory.Real.Irrational
public import Mathlib.Tactic.NormNum.Prime

public section


/-!
# USA Mathematical Olympiad 2006, Problem 4

Find all positive integers n for which there exist an integer k ≥ 2 and
positive rational numbers a₁, a₂, ..., aₖ satisfying
a₁ + a₂ + ... + aₖ = a₁ · a₂ · ... · aₖ = n.
-/

namespace Usa2006P4

/- determine -/ abbrev SolutionSet : Set ℕ := sorry

theorem usa2006_p4 (n : ℕ) (hn : 0 < n) :
    n ∈ SolutionSet ↔
      ∃ l : List ℚ, 2 ≤ l.length ∧ (∀ x ∈ l, 0 < x) ∧ l.sum = (n : ℚ) ∧
        l.prod = (n : ℚ) := sorry

end Usa2006P4

File author(s): Kimi K3

This problem has a complete formalized solution.