Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2020P2

module

public import Mathlib.Algebra.Order.BigOperators.Group.Finset
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Data.Int.ConditionallyCompleteOrder
public import Mathlib.Data.Int.Star
public import Mathlib.Order.ConditionallyCompleteLattice.Basic
public import Mathlib.Tactic.Linarith
public import Mathlib.Tactic.Linarith.Lemmas
public import Mathlib.Tactic.NormNum.Ineq
public import Mathlib.Tactic.Ring.Basic
public import Mathlib.Tactic.Zify

public section


/-!
# USA Mathematical Olympiad 2020 Problem 2

An empty 2020 × 2020 × 2020 cube is given, and a 2020 × 2020 grid of square
unit cells is drawn on each of its six faces. A beam is a 1 × 1 × 2020
rectangular prism. Several beams are placed inside the cube subject to the
following conditions:

* The two 1 × 1 faces of each beam coincide with unit cells lying on opposite
  faces of the cube. (Hence, there are 3 · 2020² possible positions for a beam.)
* No two beams have intersecting interiors.
* The interiors of each of the four 1 × 2020 faces of each beam touch either a
  face of the cube or the interior of the face of another beam.

What is the smallest positive number of beams that can be placed to satisfy
these conditions?
-/

namespace Usa2020P2

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

theorem usa2020_p2 :
    IsLeast {m | ∃ S : Finset (Beam 2020), S.Nonempty ∧ DisjointBeams S ∧ Supp S ∧
      S.card = m} solution := sorry

end Usa2020P2

File author(s): Kimi K3

This problem has a complete formalized solution.