Claimed AI-assisted

Strict Pólya inequalities claimed for simply connected planar domains, Dirichlet and Neumann, with Lean formalizations

Quanyu Tang and Zuoqin Wang, working with ChatGPT, claim Pólya's 1954 eigenvalue conjecture in strict form for the Dirichlet Laplacian on every bounded simply connected planar domain and for the Neumann Laplacian on every bounded simply connected planar Lipschitz domain, with Palomar-registered Lean formalizations of both.

Lab: Independent
Model: ChatGPT for the mathematics, version not stated; Aristotle (Harmonic) and Codex for the Lean
Field: Mathematics
Date: 2026-10-09
Human collaborators: Quanyu Tang, Zuoqin Wang
Problem posed: 1954 · open 72 yrs

Sources

Original work

arXivTang and Wang, Strict Dirichlet Pólya Inequality for Simply Connected Planar Domains↗GitHubthe Lean formalization of the Dirichlet result↗GitHubthe Lean formalization of the Neumann result, with the draft manuscript↗

What was found

Pólya conjectured that the Dirichlet eigenvalues of a planar domain of area $|\Omega|$ satisfy $\lambda_j(\Omega) \ge 4\pi j/|\Omega|$ and the Neumann eigenvalues $\mu_j(\Omega) \le 4\pi j/|\Omega|$ , the bounds that Weyl's law approaches from either side; it was proved for domains that tile the plane and is open for general domains. The Dirichlet paper proves $|\Omega|\lambda_j(\Omega) > 4\pi j$ for every $j \ge 1$ on every bounded simply connected planar domain, with no boundary regularity, through a unitary boundary-transport formulation of the Helmholtz equation that relates Dirichlet resonances to eigenphase crossings via the Dirichlet-to-Neumann map: an exact area identity gives the sharp Weyl coefficient, a Ky Fan estimate leaves a strictly positive remainder, and conformal exhaustion handles general domains. The Neumann result proves $|\Omega|\mu_j(\Omega) < 4\pi j$ for $j \ge 1$ on bounded simply connected Lipschitz domains, indexed from $\mu_0 = 0$ , together with the equivalent counting form; its manuscript is not yet on arXiv, and a draft sits in the registered repository. Before this the conjecture was known for tiling domains, disks and a few further families such as annuli, and on 2026-10-05 Speciel proved two thirds of the Dirichlet bound for every planar domain. The two Lean developments are about 27,000 and 100,000 lines.

Novelty check

Searched arXiv on 2026-10-16 for Pólya's conjecture and planar eigenvalue bounds since 2024. Found the ball and annulus results of Filonov, Levitin, Polterovich and Sher, Jiang and Lin's result up to an $\varepsilon$ -loss for large eigenvalues, and Speciel's two-thirds bound for all planar domains (arXiv:2610.05636), posted four days before the Dirichlet preprint; none proves the full bound for a class as wide as simply connected domains. MathDB's record for the conjecture lists it as open for general domains. Nothing in the registry covered Pólya's conjecture.

Caveats and known objections

Graded claimed rather than formal, on this registry's precedent for 2026-09-06-bollobas-nikiforov, which shares an author and has the same shape. Both statements carry Palomar registrations that replay the proofs against Mathlib-only Challenge files with Comparator, and vibemathed read both Challenge files, as was done here, but the definitions of the eigenvalues, of $H^1$ and of Lipschitz domains are the authors' own, and a curator's reading is not a named expert's confirmation that they say what Pólya's conjecture says. A spectral geometer with no stake confirming the two files would support formal. The Dirichlet statement defines $\lambda_j$ by min-max of the Rayleigh quotient over $j$ -dimensional spaces of smooth compactly supported functions in $\Omega$ , with Lebesgue area; the Neumann statement defines Lipschitz domains explicitly, $H^1$ through weak gradients and $\mu_j$ by min-max over $(j+1)$ -dimensional subspaces. Neither informal proof has been read by anyone outside the authors, and the Neumann manuscript is not yet public. Multiply connected domains and higher dimensions remain open, so this is not Pólya's conjecture in general. Autonomy is graded ai-assisted on the authors' own wording, that the result and its informal proof were developed by the authors with assistance from ChatGPT and the Lean with Aristotle and Codex; the division of labour on the mathematics is not described further, and the repositories add that some Lean code and proof steps were AI-generated rather than written line by line.

Machine-checked elsewhere

PalomarPALOMAR-2026-10-09-000003

QuanyuTang/polya-dirichlet-simply-connected-formalization-Palomar-version at ba3690bfd486 · checked 2026-10-09

ProvedPalomarDirichlet.main_result

A Lean proof that typechecks against the recorded statement at a pinned commit under a declared axiom set, checked mechanically rather than by human review. It does not certify that a result is new or of research interest: the only filter on that is a language-model screen, and Palomar states that it adds no human editorial step.

The Dirichlet result. Permitted axioms are exactly propext, Quot.sound and Classical.choice.

PalomarPALOMAR-2026-10-09-000007

QuanyuTang/polya-neumann-simply-connected-formalization-Palomar-version-v2 at f07f1c705186 · checked 2026-10-09

ProvedPalomarPolyaNeumann.strict_neumann_polyaPalomarPolyaNeumann.strict_neumann_polya_count

The Neumann result, for Lipschitz domains. Permitted axioms are exactly propext, Quot.sound and Classical.choice.

The open problem

MathDBPólya's conjecture

383222

Nothing mechanically. It records what a problem says, what is known about it, and the standing of any claimed solution.

Also recorded at

vibemathedstrict-dirichlet-polya-inequality-on-simply-connected-planar-domains

Nothing mechanically. It is a parallel listing of the same result, carrying its own verification label rather than an independent check.

vibemathedstrict-neumann-polya-inequality-on-simply-connected-planar-lipschitz-domains

Nothing mechanically. It is a parallel listing of the same result, carrying its own verification label rather than an independent check.

Nobody outside the lab has checked this yet.

Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.

Submit a check Challenge the grade

Or on GitHub: submit a check challenge the grade send a correction or send a pull request

Entry history (1 event)

2026-10-16AddedEntered the registry graded Claimed and AI-assisted.

Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.

Graded claimed for verification and ai-assisted for autonomy. What these mean.

Cite this entry

Plain text

whataifound.org. (2026). Strict Pólya inequalities claimed for simply connected planar domains, Dirichlet and Neumann, with Lean formalizations. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-10-09-polya-simply-connected

BibTeX

@misc{whataifound-independent-2026-connected,
  title        = {Strict Pólya inequalities claimed for simply connected planar domains, Dirichlet and Neumann, with Lean formalizations},
  author       = {{whataifound.org}},
  year         = {2026},
  howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
  note         = {Result by Independent. Verification: Claimed. Autonomy: AI-assisted.},
  url          = {https://whataifound.org/finding/2026-10-09-polya-simply-connected}
}

Related findings

ClaimedFinite-time blowup for Navier-Stokes with smooth forcing, Clay alternatives C and DOpenAI · 2026-09-08 ClaimedFinite-time blowup for the unforced Euler equations from smooth compactly supported dataOpenAI · 2026-09-08 Formally verifiedErdős Problem 173: a two-coloring of the plane misses at most one triangle, which is equilateralPlasma AI · 2026-10-19

spectral-geometry eigenvalues pde lean formalization argument

← All mathematics findings in the registry