Strict Neumann Pólya inequality on simply connected planar Lipschitz domains

Does the Neumann Pólya conjecture hold for every bounded, connected planar Lipschitz domain $\Omega\subset\mathbb R^2$ ? More precisely, is it true that $|\Omega|\mu_j(\Omega)\le 4\pi j \qquad(j\ge1),$ where $0=\mu_0(\Omega)<\mu_1(\Omega)\le\mu_2(\Omega)\le\cdots$ are the Neumann eigenvalues 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); tiling case proved by Pólya (1961) and Kellner (1966)
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: Announced
Significance: 42 / 100
Disclosed cost: —
Wikipedia: No dedicated article

What was actually shown

Main theorem: for every bounded simply connected planar Lipschitz domain $\Omega$ , $|\Omega|\mu_j(\Omega)<4\pi j$ for all $j\ge1$ , with $0=\mu_0<\mu_1\le\cdots$ counted with multiplicity; equivalently $N_N(E)>|\Omega|E/(4\pi)$ for $E>0$ , where $N_N$ counts $\mu_j<E$ including $\mu_0$ . It contains the convex planar case, for which Filonov (CPAM 2025) had only a weaker constant, and the disk case of Filonov, Levitin, Polterovich and Sher (2023). Multiply connected domains, non-Lipschitz domains and higher dimensions remain open. The manuscript is not yet on arXiv; a draft is in the registered snapshot. The companion strict Dirichlet result is a separate entry.

What the AI did

ChatGPT assisted the authors in developing the mathematical result and its informal proof. Aristotle (Harmonic) and Codex assisted the authors in producing the Lean formalization, including translating proof ideas into Lean, constructing proof steps and 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-000007 v1 was fetched from the registry's data API: registered commit f07f1c7, Comparator theorems strict_neumann_polya and strict_neumann_polya_count, checked with the Lean, nanoda and con-ron kernels, automated review neutral with no warnings, trust level high. Challenge.lean (Mathlib only, identical on main) was read: Lipschitz domain as open, connected and locally above a Lipschitz graph after a rigid motion; H1 by weak gradients in L2 tested against C_c^inf functions; mu_j by min-max over (j+1)-dimensional subspaces of L2 with no boundary condition, the standard Neumann eigenvalue indexed from mu_0 = 0. The registered snapshot (about 100,000 lines) was grepped: the only sorrys are the two Challenge statement holes; no admit, axiom declarations, native_decide, unsafe or implemented_by. The repository's Actions build passed on the registered commit, and its 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 draft manuscript was not read. Lean-checked, not Lean-verified: the statement audit is this site's alone and nothing was rebuilt here.

Sources

PaperDraft manuscript in the registered snapshot (v3)Companion Dirichlet paper, arXiv:2610.13139
Lean proofGitHub
Palomar listingPALOMAR-2026-10-09-000007 v1
CodeRegistered snapshot, commit f07f1c7

Related entries

RelatedStrict Dirichlet Pólya inequality
RelatedPólya, Neumann balls

Submitted by StormyCobra617 on 09 Oct 2026