Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2005P4

module

public import Mathlib.Algebra.BigOperators.Intervals
public import Mathlib.Data.Finset.NatAntidiagonal
public import Mathlib.Data.Set.Card
public import Mathlib.Tactic.NormNum.BigOperators
public import Mathlib.Tactic.Ring

public section


/-!
# USA Mathematical Olympiad 2005, Problem 4

Legs L₁, L₂, L₃, L₄ of a square table each have length n, where n is a positive
integer. For how many ordered 4-tuples (k₁, k₂, k₃, k₄) of nonnegative integers
can we cut a piece of length kᵢ from the end of leg Lᵢ (i = 1, 2, 3, 4) and
still have a stable table? (The table is stable if it can be placed so that
all four of the leg ends touch the floor. Note that a cut leg of length 0 is
permitted.)
-/

namespace Usa2005P4

/- determine -/ abbrev solution (n : ℕ) : ℕ := sorry

theorem usa2005_p4 (n : ℕ) :
    {k : ℕ × ℕ × ℕ × ℕ | k.1 ≤ n ∧ k.2.1 ≤ n ∧ k.2.2.1 ≤ n ∧ k.2.2.2 ≤ n ∧
      k.1 + k.2.2.1 = k.2.1 + k.2.2.2}.ncard = solution n := sorry

end Usa2005P4

File author(s): Kimi K3

This problem has a complete formalized solution.