Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2023P1

import Mathlib.Tactic

/-!
# International Mathematical Olympiad 2023, Problem 1

Determine all composite integers n>1 that satisfy the following property:
if d₁,d₂,...,dₖ are all the positive divisors of n with
1 = d₁ < d₂ < ... < dₖ = n, then dᵢ divides dᵢ₊₁ + dᵢ₊₂ for every
1 ≤ i ≤ k - 2.
-/

namespace Imo2023P1

abbrev ConsecutiveFactors (n a b : ℕ) :=
  a ∣ n ∧ b ∣ n ∧ a < b ∧ ¬∃ c, (c ∣ n ∧ a < c ∧ c < b)

abbrev Dividable (n : ℕ) :=
  ∀ {a b c : ℕ},
    ConsecutiveFactors n a b ∧ ConsecutiveFactors n b c
    → a ∣ b + c

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

theorem imo2023_p1 : solution_set = { n | 1 < n ∧ Dividable n } := sorry

end Imo2023P1

File author(s): Clayton Knittel

This problem has a complete formalized solution.