Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2020P5

module

public import Mathlib.Algebra.Order.Archimedean.Real.Basic
public import Mathlib.Algebra.Polynomial.Roots

public section


/-!
# USA Mathematical Olympiad 2020, Problem 5

A finite set S of points in the coordinate plane is called overdetermined if |S| ≥ 2
and there exists a nonzero polynomial P(t), with real coefficients and of degree at
most |S| − 2, satisfying P(x) = y for every point (x, y) ∈ S.

For each integer n ≥ 2, find the largest integer k (in terms of n) such that there
exists a set of n distinct points that is not overdetermined, but has k
overdetermined subsets.
-/

open Classical Polynomial

namespace Usa2020P5

/-- A finite set of points in the coordinate plane is *overdetermined* if it has at
least two elements and some nonzero real polynomial of degree at most `|S| - 2`
passes through every point of `S`. -/
def Overdetermined (S : Finset (ℝ × ℝ)) : Prop :=
  2 ≤ S.card ∧ ∃ P : ℝ[X], P ≠ 0 ∧ P.natDegree ≤ S.card - 2 ∧ ∀ p ∈ S, P.eval p.1 = p.2

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

theorem usa2020_p5 (n : ℕ) (hn : 2 ≤ n) :
    IsGreatest {k : ℕ | ∃ S : Finset (ℝ × ℝ), S.card = n ∧ ¬ Overdetermined S ∧
      (S.powerset.filter Overdetermined).card = k} (solution n) := sorry

end Usa2020P5

File author(s): Kimi K3

This problem has a complete formalized solution.