Mordell's discriminant inequality in the five-point case bounds the absolute value of the polynomial discriminant
in terms of the squared moduli of the roots. For five complex numbers 
, 
, ..., 
with 
, it states
 |
Xu et al. (2026) proved this inequality with equality precisely when the points form a regular pentagon on the unit circle, up to rotation and relabeling.
The argument reduces the possible maximizing configurations to algebraic branches and excludes the competing branches by exact rational interval arithmetic. Xu et al. (2026) report a Lean formalization of the inequality and both directions of the equality characterization.
