Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1991P5

import Mathlib

/-!
# International Mathematical Olympiad 1991, Problem 5

Let ABC be a triangle and P be an interior point of ABC.
Show that at least one of the angles ∠PAB, ∠PBC, ∠PCA is
less than or equal to 30°.

-/

namespace Imo1991P5

open scoped Affine EuclideanGeometry Real

theorem imo1991_p5
    (A B C P : EuclideanSpace ℝ (Fin 2))
    (hABC : AffineIndependent ℝ ![A, B, C])
    (hP : P ∈ interior (convexHull ℝ {A, B, C})) :
    ∠ P A B ≤ π / 6 ∨ ∠ P B C ≤ π / 6 ∨ ∠ P C A ≤ π / 6 := sorry

end Imo1991P5

This problem does not yet have a complete formalized solution.