Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2020P4

module

public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.AlgebraicTopology.SimplexCategory.Basic
public import Mathlib.Analysis.Normed.Ring.Lemmas
public import Mathlib.Data.Int.Star
public import Mathlib.RingTheory.Coprime.Lemmas
public import Mathlib.Tactic.LinearCombination
public import Mathlib.Tactic.LinearCombination.Lemmas

public section


/-!
# USA Mathematical Olympiad 2020, Problem 4

Suppose that (a₁, b₁), (a₂, b₂), ..., (a₁₀₀, b₁₀₀) are distinct ordered pairs
of nonnegative integers. Let N denote the number of pairs of integers (i, j)
satisfying 1 ≤ i < j ≤ 100 and |aᵢbⱼ − aⱼbᵢ| = 1. Determine the largest
possible value of N over all possible choices of the 100 ordered pairs.
-/

namespace Usa2020P4

/-- The determinant `aᵢ bⱼ − aⱼ bᵢ` of two ordered pairs of nonnegative
integers, viewed as an integer. -/
def det (P Q : ℕ × ℕ) : ℤ := (P.1 : ℤ) * (Q.2 : ℤ) - (Q.1 : ℤ) * (P.2 : ℤ)

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

/-- USA Mathematical Olympiad 2020, Problem 4 -/
theorem usa2020_p4 :
    IsGreatest {N : ℕ | ∃ v : Fin 100 → ℕ × ℕ, Function.Injective v ∧
      N = (Finset.univ.filter fun p : Fin 100 × Fin 100 =>
        p.1 < p.2 ∧ |det (v p.1) (v p.2)| = 1).card} answer := sorry

end Usa2020P4

File author(s): Kimi K3

This problem has a complete formalized solution.