Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2007P6

import Mathlib

/-!
# International Mathematical Olympiad 2007, Problem 6

Let n be a positive integer. Consider
  S = {(x, y, z) : x, y, z ∈ {0, 1, ... , n}, x + y + z > 0}
as a set of (n + 1)³ - 1 points in three-dimensional space. Determine the smallest possible
number of planes, the union of which contains S but does not include (0, 0, 0).
-/

namespace Imo2007P6

abbrev Point := Fin 3 → ℝ

structure Plane where
  poly : MvPolynomial (Fin 3) ℝ
  totalDegree_eq_one : poly.totalDegree = 1

def coordSet (n : ℕ) : Finset ℝ := (Finset.range (n + 1)).map ⟨Nat.cast, Nat.cast_injective⟩
def S (n : ℕ) : Set Point := { p | (∀ i : Fin 3, p i ∈ coordSet n) ∧ p 0 + p 1 + p 2 > 0 }
def IsAdmissible (n : ℕ) (T : Finset Plane) : Prop :=
  (∀ p ∈ S n, ∃ P ∈ T, P.poly.eval p = 0) ∧
  (∀ P ∈ T, P.poly.eval 0 ≠ 0)

/- determine -/ abbrev solution_value (n : ℕ+) : ℕ := sorry

theorem imo2007_p6 (n : ℕ+) :
    IsLeast { k | ∃ T : Finset Plane, IsAdmissible n T ∧ T.card = k } (solution_value n) := sorry

end Imo2007P6

File author(s): Markus Rydh, Codex

This problem has a complete formalized solution.