Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1970P6

import Mathlib

/-!
# International Mathematical Olympiad 1970, Problem 6

In a plane there are 100 points, no three of which are collinear.
Consider all possible triangles having these points as vertices.
Prove that no more that 70% of these triangles are acute.
-/

namespace Imo1970P6

open scoped EuclideanGeometry Real RealInnerProductSpace
open EuclideanGeometry Finset

abbrev Pt := EuclideanSpace ℝ (Fin 2)

theorem imo1970_p6
    (P : Fin 100 → Pt)
    (hP : ∀ a b c : Fin 100,
             List.Nodup [a, b, c] → ¬ Collinear ℝ {P a, P b, P c}) :
    let cardAll := Nat.card { s : Finset (Fin 100) | s.card = 3 }
    let cardAcute := Nat.card { s : Finset (Fin 100) | s.card = 3 ∧
      ∃ a b c : Fin 100, s = {a, b, c} ∧
      ∃ t : Affine.Triangle ℝ Pt, ![P a, P b, P c] = t.points ∧ t.AcuteAngled }
    (cardAcute : ℚ) / cardAll ≤ 7 / 10 := sorry

end Imo1970P6

File author(s): David Renshaw

This problem has a complete formalized solution.