The Pólya eigenvalue conjecture asserts that the Dirichlet and Neumann eigenvalues of the negative Laplacian
on a bounded domain 
satisfy
 |
(1)
|
for 
,
where 
is the volume of the unit ball,
is the volume of the domain, 
are the eigenvalues
for Neumann boundary conditions, and
are the eigenvalues for Dirichlet
boundary conditions, counted with multiplicity (Dai and Sun 2026).
Dai and Sun (2026) proved the Neumann inequality for every circular annulus 
with 
,
 |
(2)
|
for all 
.
Their proof combines analytic estimates with computer-assisted interval certificates
covering the remaining parameter ranges.
Tang and Wang (2026a) reported the strict Dirichlet inequality
 |
(3)
|
for every nonempty bounded, simply connected planar domain 
and every 
. Their proof and accompanying
formalization have not been independently checked here.
Tang and Wang (2026b) separately reported the strict Neumann inequality
 |
(4)
|
for every nonempty bounded, simply connected planar domain 
with Lipschitz
boundary and every 
. The indexing begins with 
. The general conjecture remains open.
Tang and Wang (2026a,b) acknowledge ChatGPT assistance with technical arguments and Aristotle and Codex assistance with Lean formalizations. The registered Neumann development passed machine checks, but independent specialist review of the complete argument had not been reported as of Oct. 15, 2026.
