Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1981P2

module

public import Mathlib.Tactic

public section


/-!
# USA Mathematical Olympiad 1981, Problem 2

What is the largest number of towns that can meet the following criteria?
Each pair is directly linked by just one of air, bus or train.
At least one pair is linked by air, at least one pair by bus and at least
one pair by train. No town has an air link, a bus link and a train link.
No three towns, A, B, C are such that the links between AB, AC and BC are
all air, all bus or all train.
-/

namespace Usa1981P2

/-- The three possible link types between two towns. -/
inductive Link | air | bus | train
  deriving DecidableEq

instance : Fintype Link where
  elems := ⟨↑[Link.air, Link.bus, Link.train], by decide⟩
  complete := fun x => by cases x <;> decide

/-- The set of link types that town `v` has to other towns. -/
abbrev colorsAt {n : ℕ} (f : Fin n → Fin n → Link) (v : Fin n) : Finset Link :=
  (Finset.univ.filter (· ≠ v)).image (f v ·)

/-- A link assignment on `n` towns satisfying all the criteria of the problem:
it is symmetric, all three link types are used, no town has all three link
types, and no three towns are pairwise linked by the same type. -/
abbrev Valid {n : ℕ} (f : Fin n → Fin n → Link) : Prop :=
  (∀ i j, f i j = f j i) ∧
  (∃ i j, i ≠ j ∧ f i j = .air) ∧
  (∃ i j, i ≠ j ∧ f i j = .bus) ∧
  (∃ i j, i ≠ j ∧ f i j = .train) ∧
  (∀ v, (colorsAt f v).card ≤ 2) ∧
  (∀ a b c, a ≠ b → b ≠ c → a ≠ c → ¬ (f a b = f a c ∧ f a b = f b c))

/- determine -/ abbrev answer : ℕ := sorry

theorem usa1981_p2 :
    IsGreatest {n : ℕ | ∃ f : Fin n → Fin n → Link, Valid f} answer := sorry

end Usa1981P2

File author(s): Kimi K3

This problem has a complete formalized solution.