Planar Pólya–Szegő conjecture for the first buckling eigenvalue
The Pólya–Szegő conjecture asks whether, among all bounded planar domains of a prescribed area and with sufficiently regular boundary, the disk minimizes the first buckling eigenvalue of a clamped plate.
For a domain , definewhere is the closure of in the Sobolev norm.
The conjecture asserts thatwhenever is a disk satisfying .
- Result
- Proved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-assisted
- Method
- Argument
- Field
- Spectral geometry
- Posed by
- G. Pólya and G. Szegő, Isoperimetric Inequalities in Mathematical Physics (1951)
- Year posed
- 1951
- Years open
- 75y
- Solved
- 2026-10-18
- Model
- ChatGPT; Aristotle; Codex
- Vendor
- OpenAI; Harmonic
- Collaborators
- Quanyu Tang, Haiqi Zhang
- Verification
- Lean-checked, statement unaudited
- Publication
- Announced
- Significance
- 40 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
The authors prove the planar Pólya-Szegő conjecture for every open set of finite positive area, without assumptions on connectedness, boundedness, boundary regularity or the sign of an eigenfunction: , with equality if and only if is an open disk. The route is a new sharp buckling-Dirichlet comparison combined with Faber-Krahn, and the disk formula . All five statements are formalized in Lean 4 and registered at Palomar (PALOMAR-2026-10-18-000008). The informal manuscript is a working draft (v5, 18 October 2026) in the repository, not yet on arXiv. Dimensions remain open.
What the AI did
Quanyu Tang and Haiqi Zhang developed the original informal mathematical proof with assistance from ChatGPT.
Aristotle (Harmonic) constructed an initial Lean formalization based on the authors' proof. Codex (OpenAI) subsequently completed the missing proof obligations, including the unconditional analytic components, translated further mathematical arguments into Lean, performed API migration and dependency checks, and carried out semantic and axiom audits.
The resulting formalization covers the sharp planar buckling–Dirichlet comparison, the sharp area inequality, the exact characterization of the equality case, and the buckling eigenvalue formula for disks.
Verification
No independent mathematician has checked this yet. Read by this site on 3 November 2026, not rebuilt. Palomar record PALOMAR-2026-10-18-000008 v1 fetched from the registry's data API: commit 5311f47, five Comparator theorems, kernels Lean, nanoda and con-ron, automated review neutral with no warnings, trust level high. The SHA-256 of PlanarBucklingChallenge.lean and PlanarBucklingSolution.lean at that commit match the record. The Challenge file (Mathlib only, 161 lines) was read: Lambda_1 is the infimum of the integral of (Delta v)^2 over the integral of |grad v|^2 on the H^2 closure of smooth compactly supported functions in Omega, the Dirichlet eigenvalue likewise on the H^1 closure, Bessel zeros from the power series; the headline theorem is the conjecture for every open Omega of finite positive area, with equality only for an open disk, which covers the problem as posed. The snapshot (185 Lean files, about 57,000 lines) was grepped: the only sorry are the five Challenge holes; no admit, axiom declarations, native_decide, unsafe or implemented_by. Lean verification, Palomar checks and the official preflight passed on GitHub Actions at that commit; permitted axioms are propext, Quot.sound and Classical.choice. The manuscript was not read in detail. Lean-checked, not Lean-verified: the statement audit is this site's alone and nothing was rebuilt here.
Sources
- PaperManuscript working draft v5 (PDF)
- Lean proofLean statement: PlanarBucklingChallenge.lean
- Palomar listingPalomar Registry — PALOMAR-2026-10-18-000008 (v1)
- CodeGitHub repositoryRegistered snapshot, commit 5311f47
- Problem recordAIM catalogue, Problem 007 (Colbrook)
- OtherAIM issue 174: proposed resolution of Problem 007Related: strict Dirichlet Pólya inequality (same author)
Submitted by StormyCobra617 on