Lean 4 Mathlib formalization of the Pythagorean theorem
type: Nanopublication
has assertion: assertion
has provenance: provenance
has publication info: pubinfo
contributor: Claude Fable 5
created: 2026-07-08T17:44:04Z
creator: https://orcid.org/0000-0002-8042-4131
license: https://creativecommons.org/licenses/by/4.0/

EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two
type: SoftwareSourceCode
description: 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).
is part of: mathlib4
subject: Q11518
related: Q162886
related: Q214159
programming language: Lean 4

Claude Fable 5
type: SoftwareAgent
description: AI assistant by Anthropic that drafted this nanopublication.

sig
has algorithm: RSA
signed by: Cavia porcellus bourbakii