Morley's trisector theorem

morley_theorem

Submitter: Kim Morrison.

Notes: The triangle formed by the adjacent angle-trisectors of any nondegenerate Euclidean triangle is equilateral. Trusted helpers (IsEquilateralTriple, LiesInTriangle, IsMorleyConfiguration) are non-holes. Mathlib has Euclidean angles but not Morley's theorem. Candidate from §162 of the Knill survey.

Source: F. Morley (c. 1899). Knill, §162.

Informal solution: Unavailable.

theorem declaration uses `sorry`morley_theorem (A B C P Q R : LeanEval.Geometry.Morley.Plane)
    (h : LeanEval.Geometry.Morley.IsMorleyConfiguration A B C P Q R) :
    LeanEval.Geometry.Morley.IsEquilateralTriple P Q R := byA:PlaneB:PlaneC:PlaneP:PlaneQ:PlaneR:Planeh:IsMorleyConfiguration A B C P Q R⊢ IsEquilateralTriple P Q R
  sorryAll goals completed! 🐙

Solved by

• @GanjinZero with Seed Prover (ByteDance) on Jun 10, 2026