Hippocrates' theorem on lunes

hippocrates_lunes

Submitter: Kim Morrison.

Notes: For a right triangle, the sum of the areas of the two Hippocrates lunes equals the area of the triangle. Trusted helpers (det2, closedHalfDisk, hypotenuseSemidisk, horizontalLune, verticalLune, rightTriangle, …) are non-holes; the Euclidean squared distance is used explicitly to avoid the ℝ×ℝ sup metric. Mathlib has no lune-area result. Candidate from §166 of the Knill survey.

Source: Hippocrates of Chios (c. 440 BC). Knill, §166.

Informal solution: Unavailable.

theorem declaration uses `sorry`hippocrates_lunes (a b : ℝ) (ha : 0 < a) (hb : 0 < b) :
    volume (LeanEval.Geometry.HippocratesLunes.horizontalLune a b) + volume (LeanEval.Geometry.HippocratesLunes.verticalLune a b) =
      volume (LeanEval.Geometry.HippocratesLunes.rightTriangle a b) := bya:ℝb:ℝha:0 < ahb:0 < b⊢ volume (horizontalLune a b) + volume (verticalLune a b) = volume (rightTriangle a b)
  sorryAll goals completed! 🐙

Solved by

• @parabamoghv with Aristotle (Harmonic) on Jun 9, 2026 (proof)

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