Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2001P5

import Mathlib.Geometry.Euclidean.Triangle


/-!
# International Mathematical Olympiad 2001, Problem 5

Let `ABC` be a triangle. Let `AP` bisect `∠BAC` and let `BQ` bisect `∠ABC`,
with `P` on `BC` and `Q` on `AC`. If `AB + BP = AQ + QB` and `∠BAC = 60°`,
what are the angles of the triangle?
-/

open Affine EuclideanGeometry
open scoped Real

variable {V X : Type*}
variable [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace X] [NormedAddTorsor V X]

noncomputable section

namespace Imo2001P5

variable (X) in
/-- The problem's configuration. -/
structure Setup where
  (A B C P Q : X)
  P_on_BC : Wbtw ℝ B P C
  AP_bisect_BAC : ∠ B A P = ∠ P A C
  Q_on_AC : Wbtw ℝ A Q C
  BQ_bisect_ABC : ∠ A B Q = ∠ Q B C
  dist_sum : dist A B + dist B P = dist A Q + dist Q B
  BAC_eq : ∠ B A C = π / 3

theorem imo2001_p5 (s : Setup X) :
    ∠ s.A s.B s.C = 4 * π / 9 ∧ ∠ s.A s.C s.B = 2 * π / 9 := sorry

end Imo2001P5

File author(s): Jeremy Tan

This problem has a complete formalized solution.

The solution was imported from mathlib4/Archive/Imo/Imo2001Q5.lean.