Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2014P3

import Mathlib.Tactic
import Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

/-!
# USA Mathematical Olympiad 2014, Problem 3

Prove that there exists an infinite set of points

… , P₋₃, P₋₂, P₋₁, P₀, P₁, P₂, P₃, …

in the plane with the following property:
For any three distinct integers a, b, and c,
points Pₐ, P_b, P_c are collinear if and only if a+b+c=2014.
-/

notation "Pt" => EuclideanSpace ℝ (Fin 2)

namespace Usa2014P3

theorem usamo2014_p3 : ∃ P : ℤ → Pt, ∀ a b c : ℤ,
    a ≠ b ∧ b ≠ c ∧ c ≠ a → (Collinear ℝ {P a, P b, P c} ↔ a + b + c = 2014) := sorry
end Usa2014P3

File author(s): Evan Chen

This problem has a complete formalized solution.