Apollonius's theorem

Proved

FamousTheorems.dist_sq_add_dist_sq_eq_two_mul_dist_midpoint_sq_add_half_dist_sq

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

euclidean-geometrygeometrymathlib

Apollonius's theorem (the median-length formula). For a triangle with median to the midpoint $m$ of one side,

|AB|^2 + |AC|^2 = 2|Am|^2 + \tfrac12 |BC|^2.

The sum of squares of two sides is determined by the median to the third side and that side's length. It is the parallelogram law in disguise — doubling the median produces a parallelogram, and the identity becomes the statement that the sum of squares of the diagonals equals the sum of squares of the sides. That connection is why the result holds in any inner product space and characterises norms coming from inner products. Formalization note. midpoint is the affine midpoint and distances are squared. The result is Mathlib's EuclideanGeometry.dist_sq_add_dist_sq_eq_two_mul_dist_midpoint_sq_add_half_dist_sq.

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 dist_sq_add_dist_sq_eq_two_mul_dist_midpoint_sq_add_half_dist_sq :
    ∀ {V : Type u_1} {P : Type u_2} 
    [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] 
    (a b c : P), dist a b ^ 2 + dist a c ^ 2 = 2 * (dist a (midpoint ℝ b c) ^ 2 + (dist b c / 2) ^ 2) := 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