Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1990P3

module

public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.AlgebraicTopology.SimplexCategory.Basic
public import Mathlib.Data.Nat.GCD.Basic
public import Mathlib.Order.Interval.Finset.Nat
public import Mathlib.Tactic.NormNum.Prime
public import Mathlib.Tactic.Ring

public section


/-!
# USA Mathematical Olympiad 1990, Problem 3

Show that for any odd positive integer n, we can always divide the set
{n, n+1, n+2, ... , n+32} into two parts, one with 14 numbers and one with 19,
so that the numbers in each part can be arranged in a circle, with each number
relatively prime to its two neighbours.
-/

namespace Usa1990P3

/-- A circular arrangement `a : Fin k → ℕ` of `k` numbers is *valid* if every entry is
relatively prime to its cyclically-next neighbour (and hence also to its cyclically
previous neighbour, since `Nat.Coprime` is symmetric). -/
def ValidCircle {k : ℕ} [NeZero k] (a : Fin k → ℕ) : Prop :=
  ∀ i : Fin k, Nat.Coprime (a i) (a (i + 1))

theorem usa1990_p3 (n : ℕ) (hn : Odd n) (hn0 : 0 < n) :
    ∃ a : Fin 14 → ℕ, ∃ b : Fin 19 → ℕ,
      Function.Injective a ∧ Function.Injective b ∧
      Disjoint (Finset.univ.image a) (Finset.univ.image b) ∧
      Finset.univ.image a ∪ Finset.univ.image b = Finset.Icc n (n + 32) ∧
      ValidCircle a ∧ ValidCircle b := sorry

end Usa1990P3

File author(s): Kimi K3

This problem has a complete formalized solution.