Strict Dirichlet Pólya inequality on simply connected planar domains

Does the Dirichlet Pólya conjecture hold for every bounded planar domain $\Omega\subset\mathbb R^2$ ? Equivalently, is it true that $4\pi j\leq |\Omega|\lambda_j(\Omega) \qquad(j\ge1),$ where $\lambda_j(\Omega)$ denotes the $j$ -th Dirichlet eigenvalue of $\Omega$ , counted with multiplicity?

Result: Proved(see note)
Status: Partial result
AI contribution: AI-assisted
Method: Argument
Field: Spectral geometry
Posed by: George Pólya, Mathematics and Plausible Reasoning (1954); he proved it for plane-tiling domains in 1961
Year posed: 1954
Years open: 72y
Solved: 2026-10-09
Model: ChatGPT; Aristotle; Codex
Vendor: OpenAI; Harmonic
Collaborators: Quanyu Tang, Zuoqin Wang
Verification: Lean-checked, statement unaudited
Publication: Preprint
Significance: 45 / 100
Disclosed cost: —
Wikipedia: No dedicated article

What was actually shown

Theorem 1.1 of arXiv:2610.13139: for every bounded nonempty simply connected planar domain $\Omega$ , with no boundary regularity assumed, $|\Omega|\lambda_j(\Omega)>4\pi j$ for all $j\ge1$ , equivalently $N_D(E)<|\Omega|E/(4\pi)$ for $E>0$ (eigenvalues counted with multiplicity, endpoint included). This is the strict form of Pólya's Dirichlet inequality on the whole simply connected planar class. Previously it was known for tiling domains (Pólya 1961), disks and sectors (Filonov, Levitin, Polterovich and Sher 2023), annuli and a few further families. Multiply connected planar domains and higher dimensions remain open. The companion strict Neumann result for simply connected Lipschitz domains is a separate entry.

What the AI did

ChatGPT assisted the authors in developing the mathematical result and its informal proof. Aristotle and Codex assisted the authors in producing the Lean formalization, including translating proof ideas into Lean, constructing bridge lemmas, debugging, and source and axiom audits. The authors reviewed the mathematical statement, the correspondence between the informal result and the Lean statements, and the final repository. The Lean kernel and the Palomar verification workflow checked the registered formal proof.

Verification

No independent mathematician has checked this yet. Read by this site on 15 October 2026, not rebuilt. The Palomar record PALOMAR-2026-10-09-000003 v1 was fetched from the registry's data API: registered commit ba3690b, Comparator theorem PalomarDirichlet.main_result, checked with the Lean, nanoda and con-ron kernels, automated review neutral with no warnings, trust level high. Challenge.lean at that commit (identical on main; later commits touch only documentation) was read: Mathlib only, bounded open simply connected Omega in C, and lambda_j defined by min-max of the Rayleigh quotient over j-dimensional spaces of smooth compactly supported functions in Omega, which is the standard Dirichlet eigenvalue. The registered snapshot (about 27,000 lines) was grepped: the only sorry is the Challenge statement hole; no admit, axiom declarations, native_decide, unsafe or implemented_by. The repository's GitHub Actions build and audit passed on the registered commit; the audit asserts only propext, Classical.choice and Quot.sound. A separate check written here on disks and squares (3,000 eigenvalues each) agrees with the strict inequality; it says nothing about general domains. The informal proof was not read. Lean-checked, not Lean-verified: the statement audit is this site's alone and nothing was rebuilt here.

Sources

PaperarXiv
Lean proofLean formalization (GitHub)
Palomar listingPalomar Registry: PALOMAR-2026-10-09-000003 v1
CodeRegistered snapshot, commit ba3690b

Related entries

RelatedPólya, Neumann balls
RelatedStrict Neumann Pólya (simply connected)

Submitted by StormyCobra617 on 09 Oct 2026