Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2022P6

module

public import Mathlib.Algebra.BigOperators.Ring.Finset
public import Mathlib.Algebra.Order.BigOperators.Group.Finset
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.AlgebraicTopology.SimplexCategory.Basic
public import Mathlib.Combinatorics.SimpleGraph.Operations
public import Mathlib.Data.Set.Card

public section


/-!
# USA Mathematical Olympiad 2022, Problem 6

There are 2022 users on a social network called Mathbook, and some of them are
Mathbook-friends. (On Mathbook, friendship is always mutual and permanent.)
Starting now, Mathbook will only allow a new friendship to be formed between
two users if they have at least two friends in common. What is the minimum
number of friendships that must already exist so that every user could
eventually become friends with every other user?
-/

namespace Usa2022P6

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

theorem usa2022_p6 :
    IsLeast {m : ℕ | ∃ G : SimpleGraph (Fin 2022), Completable G ∧ G.edgeSet.ncard = m}
      answer := sorry

end Usa2022P6

File author(s): Kimi K3

This problem has a complete formalized solution.