Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1990P1

module

public import Mathlib.Algebra.BigOperators.Fin
public import Mathlib.AlgebraicTopology.SimplexCategory.Basic
public import Mathlib.Data.ZMod.Defs
public import Mathlib.InformationTheory.Hamming

public section


/-!
# USA Mathematical Olympiad 1990, Problem 1

A license plate has six digits from 0 to 9 and may have leading zeros.
If two plates must always differ in at least two places, what is the
largest number of plates that is possible?
-/

namespace Usa1990P1

/-- A license plate: six digits, each from 0 to 9 (leading zeros allowed).
We model digits as elements of `ZMod 10` so that digit sums modulo ten
are available for the checksum argument. -/
abbrev Plate := Fin 6 → ZMod 10

/-- A collection of plates is valid if any two distinct plates in it
differ in at least two places. -/
def IsValid (S : Finset Plate) : Prop :=
  ∀ p ∈ S, ∀ q ∈ S, p ≠ q → 2 ≤ hammingDist p q

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

theorem usa1990_p1 :
    IsGreatest {k : ℕ | ∃ S : Finset Plate, S.card = k ∧ IsValid S} answer := sorry

end Usa1990P1

File author(s): Kimi K3

This problem has a complete formalized solution.