Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1984P2

module

public import Mathlib.Algebra.Order.Star.Basic
public import Mathlib.Data.Int.ConditionallyCompleteOrder
public import Mathlib.Data.Nat.Factorization.Defs
public import Mathlib.GroupTheory.GroupAction.Ring
public import Mathlib.Order.Interval.Finset.Nat
public import Mathlib.Tactic.LinearCombination
public import Mathlib.Tactic.Ring.Basic

public section


/-!
# USA Mathematical Olympiad 1984, Problem 2

Can one find a set of n distinct positive integers such that the
geometric mean of any (non-empty, finite) subset is an integer?
Can one find an infinite set with this property?
-/

namespace Usa1984P2

open scoped Nat

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

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

theorem usa1984_p2a (n : ℕ) :
    if does_exist_finite then
      ∃ s : Finset ℕ, s.card = n ∧ (∀ x ∈ s, 0 < x) ∧
        ∀ t : Finset ℕ, t ⊆ s → t.Nonempty → ∃ m : ℕ, m ^ t.card = ∏ x ∈ t, x
    else
      ¬ ∃ s : Finset ℕ, s.card = n ∧ (∀ x ∈ s, 0 < x) ∧
        ∀ t : Finset ℕ, t ⊆ s → t.Nonempty → ∃ m : ℕ, m ^ t.card = ∏ x ∈ t, x := sorry

theorem usa1984_p2b :
    if does_exist_infinite then
      ∃ S : Set ℕ, S.Infinite ∧ (∀ x ∈ S, 0 < x) ∧
        ∀ s : Finset ℕ, s.Nonempty → ↑s ⊆ S → ∃ m : ℕ, m ^ s.card = ∏ x ∈ s, x
    else
      ¬ ∃ S : Set ℕ, S.Infinite ∧ (∀ x ∈ S, 0 < x) ∧
        ∀ s : Finset ℕ, s.Nonempty → ↑s ⊆ S → ∃ m : ℕ, m ^ s.card = ∏ x ∈ s, x := sorry

end Usa1984P2

File author(s): Kimi K3

This problem has a complete formalized solution.