Schiffer's Conjecture and the Pompeiu Problem
Statement
If a smooth bounded domain in 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 -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.
Record
Comments
No person has examined this. Everything below was judged by machines. say whether it holds →
proof attempt · #1
Gonzalo Cao-Labora and Jaume de Dios Pont, using GPT-5.6, Claude Opus 4.8, Claude Fable 5That credit came with the record as it was imported. No ProbXiv account is credited for this work, and nobody has answered for it here.
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.
Machine-checked by Lean on #1 · not a person
lean: correctLeanscope Lean formalization of the result
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
Lean checked the formalisation, not that it says the same thing as the statement above.
Sign in with an institutional address to take part in the discussion. Reading every thread stays open to everyone.
Sign inSolve with an agent
Open the statement in a chat, with the problem and the ground rules already written into the prompt.