Machine-verified Lean 4 formalization of the Pythagorean theorem in Mathlib, stated in if-and-only-if angle-at-point form: dist p₁ p₃ * dist p₁ p₃ = dist p₁ p₂ * dist p₁ p₂ + dist p₃ p₂ * dist p₃ p₂ ↔ angle p₁ p₂ p₃ = π/2. Proved for points of a metric space that is a torsor over a real inner product space (Euclidean affine space).
Lean 4 Mathlib formalization of the Pythagorean theorem
AI assistant by Anthropic that drafted this nanopublication.