On the Five-Point Case of Mordell's Problem
Tiancheng Xu, Guowei Dou, Wensheng Yu
math.CV
Oct 4, 2026 · v1
math.OC
TL;DR
The five-point Mordell discriminant inequality and both directions of its equality case are fully formalized in Lean 4 with Mathlib, including verified interval-bound checks.
Abstract
For five complex points $z_1,\ldots,z_5$ satisfying $\sum_i|z_i|^2=5$, Mordell's discriminant inequality states that $\prod_{i<j}|z_i-z_j|^2\leq5^5$, with equality precisely for a unit regular pentagon, up to rotation and permutation. We organize its proof around a direct comparison of discriminant values. A global maximizer gives a centered stationary configuration, whose coefficient equations reduce the generic case to two quartic branches. On each branch, the absolute value of a cubic polynomial gives the original discriminant objective after accounting for the normalization scale. Exact rational interval bounds exclude both branches from the maximum, and the exceptional coefficient cases leave the regular pentagon. The argument determines the maximizing configuration without reconstructing all stationary shapes. We have completed a full Lean formalization of the five-point inequality and both directions of its equality condition, including all reductions and finite checks used in this proof.
Problem
Mordell's discriminant inequality for five complex points with total squared modulus 5 states that the product of squared pairwise distances is at most 5^5, with equality only for the unit regular pentagon. The goal is a proof of this inequality and its equality case that can be fully machine-checked.
Approach
A global maximizer exists by compactness and must be centered and stationary. The stationarity equations, written in terms of the coefficients of the root polynomial, reduce the generic case to two quartic branches. On these branches the absolute value of a cubic gives the discriminant objective, and exact rational interval bounds rule both branches out. The exceptional coefficient cases are then shown to yield the regular pentagon. Everything is formalized in Lean 4 with Mathlib, with an interval evaluation procedure proved sound.
Results
The inequality and both directions of the equality condition are proved, determining the maximizer without reconstructing all stationary configurations. The complete Lean formalization, covering all reductions and finite checks, is available at github.com/dgjszy/mordell-five.
