Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2021P4

module

public import Mathlib.Tactic
public import Mathlib.Data.Nat.Nth
public import Mathlib.NumberTheory.ArithmeticFunction.Misc

public section


/-!
# USA Mathematical Olympiad 2021, Problem 4

A finite set S of positive integers has the property that, for each s ∈ S,
and each positive integer divisor d of s, there exists a unique element t ∈ S
satisfying gcd(s, t) = d. (The elements s and t could be equal.)

Given this information, find all possible values for the number of elements of S.
-/

namespace Usa2021P4

/-- The property from the problem statement: `S` is a finite set of positive integers
such that for every `s ∈ S` and every positive divisor `d` of `s` there exists a unique
`t ∈ S` with `Nat.gcd s t = d`. -/
def IsValid (S : Finset ℕ) : Prop :=
  (∀ s ∈ S, 0 < s) ∧ ∀ s ∈ S, ∀ d : ℕ, 0 < d → d ∣ s → ∃! t : ℕ, t ∈ S ∧ Nat.gcd s t = d

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

theorem usa2021_p4 (n : ℕ) :
    n ∈ solution_set ↔ ∃ S : Finset ℕ, IsValid S ∧ S.Nonempty ∧ S.card = n := sorry

end Usa2021P4

File author(s): Kimi K3

This problem has a complete formalized solution.