VibeMathedMath problems solved with AI
Sign in

Schiffer's Conjecture and the Pompeiu Problem

If a smooth bounded domain in Rn\mathbb{R}^n admits a Neumann eigenfunction of the Laplacian that is constant on the boundary, must the domain be a ball? Pompeiu posed an equivalent integral-equation form in 1929; Schiffer's 1957 reformulation via Neumann eigenfunctions is the version on Yau's 1982 list (Problem 80), and Williams proved the two formulations logically equivalent for simply connected domains in 1976. Cao-Labora and de Dios Pont construct infinitely many planar domains with large NN-fold symmetry that are not balls and admit such an eigenfunction, disproving Schiffer's conjecture; applying Williams' classical reduction to the same domains (their Corollary 1.2) disproves Pompeiu's problem as well.

Result
Disproved(see note)
Status
Resolved
AI contribution
AI-assisted
Method
Argument
Field
Spectral geometry
Posed by
D. Pompeiu (1929); reformulated via Neumann eigenfunctions by M. M. Schiffer (1957)
Year posed
1929
Years open
97y
Solved
2026-08-05
Model
GPT-5.6, Claude Opus 4.8, Claude Fable 5
Vendor
OpenAI, Anthropic
Collaborators
Gonzalo Cao-Labora, Jaume de Dios Pont
Verification
Lean-verified
Publication
Preprint
Significance
53 / 100
Disclosed cost
—
Wikipedia
No dedicated article

What was actually shown

Also refutes the 1929 Pompeiu problem: Corollary 1.2 applies Williams' classical 1976 equivalence to the same constructed domains, so this is one construction settling both, not two separate results.

What the AI did

Models with coding harnesses were used in multiple parts of the research: numerically verifying the asymptotic estimates, producing first drafts of the proofs of the Bessel function estimates, and helping with exposition.

The Lean4 verification of the proof was written by GPT 5.6 from an early draft of the paper. The novel construction strategy is the authors' own.

Verification

A day-old preprint. The paper states that a Lean4 verification of the proof was written by GPT 5.6, available at https://github.com/jaumededios/Schiffer. It solves the Pompeiu Problem challenge provided by https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Wikipedia/PompeiuProblem.lean

Sources

Changelog2 changes
  • AmberOsprey611changed What the AI did from “Models with coding harnesses were used in multiple parts of the research: numerically veri…” to “Models with coding harnesses were used in multiple parts of the research: numerically veri…”, also Method, Verification note, Verification, What the AI did
  • SilentTapir335changed More links from “lean-proof: Lean formalization of Theorem 1.1 and Corollary 1.2 | https://github.com/jaume…” to “lean-proof: Lean formalization of Theorem 1.1 and Corollary 1.2 | https://github.com/jaume…”

Discussion