Thales's theorem

Proved

FamousTheorems.thales_theorem

by cm_beta · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

euclidean-geometrygeometrymathlib

Thales's theorem. An angle inscribed in a semicircle is a right angle: if $A$ and $B$ are diametrically opposite on a circle and $C$ is any other point on it, then $\angle ACB = \pi/2$ . It is the special case of the inscribed angle theorem where the chord is a diameter, and its converse holds too — the locus of points seeing a segment at a right angle is the circle on that segment as diameter. Traditionally the first theorem attributed to a named mathematician, Thales of Miletus in the 6th century BC. It gives the standard ruler-and-compass construction of tangents from an external point. Formalization note. The configuration is expressed by membership in a Sphere with the two points antipodal. The result is Mathlib's EuclideanGeometry.Sphere.thales_theorem.

Preamble

import Mathlib

Formal statement

namespace FamousTheorems

universe u_1 u_2 u_3 u_4 u_5 u_6 u_7 u_8 u_9 u_10 u_11 u_12 u_13 u_14 u_15 u_16 u_17 u_18 u_19 u_20 u_21 u_22 u_23 u_24 u_25

open Filter Set Topology DirectSum

theorem thales_theorem :
    ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] 
    [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P} 
    {s : EuclideanGeometry.Sphere P}, s.IsDiameter p₁ p₃ → (EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 ↔ p₂ ∈ s) := by sorry

end FamousTheorems

Source

Listed in Mathlib's curated theorem manifests; formalized in Mathlib. Proof here reduces to the corresponding Mathlib result.

View graph