Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2024P1

module

public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Data.Int.Star
public import Mathlib.Data.Nat.Prime.Factorial
public import Mathlib.NumberTheory.Bertrand

public section


/-!
# USA Mathematical Olympiad 2024, Problem 1

Find all integers $n \geq 3$ such that the following property holds:
if we list the divisors of $n!$ in increasing order as
$1 = d_1 < d_2 < \cdots < d_k = n!$, then we have
$d_2 - d_1 \leq d_3 - d_2 \leq \cdots \leq d_k - d_{k-1}$.
-/

namespace Usa2024P1

/-- The property required of `n`: writing the divisors of `n !` in increasing
order as `1 = d₁ < d₂ < ⋯ < dₖ = n !`, the consecutive gaps are non-decreasing.
We phrase this using consecutive triples: whenever `a < b < c` are divisors of
`n !` such that no divisor of `n !` lies strictly between `a` and `b`, or strictly
between `b` and `c`, we have `b - a ≤ c - b`.
(Note: we write `Nat.factorial n` instead of `n !` since the `!` notation clashes
with `PiLp.vecNotation` under a full `Mathlib` import.) -/
def Good (n : ℕ) : Prop :=
  ∀ a ∈ (Nat.factorial n).divisors, ∀ b ∈ (Nat.factorial n).divisors,
    ∀ c ∈ (Nat.factorial n).divisors,
    a < b → b < c →
    (∀ d ∈ (Nat.factorial n).divisors, d ≤ a ∨ b ≤ d) →
    (∀ d ∈ (Nat.factorial n).divisors, d ≤ b ∨ c ≤ d) →
    b - a ≤ c - b

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

theorem usa2024_p1 (n : ℕ) (hn : 3 ≤ n) : n ∈ solution_set ↔ Good n := sorry

end Usa2024P1

File author(s): Kimi K3

This problem has a complete formalized solution.