Hlawka's inequality for 
in an inner product
space 
states that
 |
where the norm 
denotes the norm induced by the inner product.
More generally, a Hlawka constant 
for a normed space is a factor
such that the triple deficit 
is at most 
times the sum of the three pair deficits 
, 
, and 
.
Audenaert and Kittaneh (2017) asked whether the Schatten norm has a finite Hlawka constant 
independent of the matrix dimension.
Esa (2026) reported a Lean-formalized proof that such a constant exists exactly when
.
No finite constant exists for 
, already for 
matrices, or for 
, already for 
matrices. For complex diagonal matrices and 
, the same project gives the sharp constant 
as an explicit one-variable maximum
and proves
 |
The sharp constant for general matrices was not determined. GPT-5.6 Sol and GPT-6 Astra reportedly co-developed and formalized the arguments under human direction. As of Sep. 27, 2026, the Lean sources had passed the project's automated checks, but independent specialist review had not been reported.
