The Pólya-Szegő buckling conjecture (Pólya and Szegő 1951) asserts that a disk minimizes the first clamped buckling eigenvalue among smooth bounded planar domains of prescribed area. The problem is distinct from minimizing the fundamental vibration frequency of a clamped plate (Ashbaugh and Laugesen 1996, pp. 383-386).
The first buckling eigenvalue of an open planar set
is the infimum of the Rayleigh
quotient
|
(1)
|
where
is the topological closure in the Sobolev
space
of the real-valued smooth
functions with compact support contained in
.
Here
is the gradient and
is the Laplacian. On a
sufficiently smooth bounded domain,
is the least eigenvalue
of
with clamped boundary conditions
, where
is the outward unit normal
vector. The vibrating clamped-plate equation instead has the form
.
|
(2)
|
where
is the first positive zero of the Bessel
function of the first kind
. The conjectured inequality is therefore
|
(3)
|
with equality only for disks, where denotes area.
Tang and Zhang (2026ab) reported this inequality and its equality characterization for every open planar set of finite positive area, without assumptions of connectedness, boundedness, boundary regularity, or a fixed sign for a first eigenfunction. Their claimed equality condition is exact equality with an open disk, rather than equality up to a set of area zero. They also reported the sharp comparison
|
(4)
|
where
is the first Dirichlet eigenvalue of the Laplacian
and
is the first positive zero of the Bessel
function of the first kind
.
The authors report ChatGPT assistance with their mathematical proof and Aristotle and Codex assistance with the Lean formalization. As of Oct. 25, 2026, the formalization was publicly registered and automated checks were reported, but independent specialist review of the new argument had not been reported.