ProbXiv
sign in
Problem archiveProblem record

Statement

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.

Record

Comments

No person has examined this. Everything below was judged by machines. say whether it holds →

  1. proof attempt · #1

    Gonzalo Cao-Labora and Jaume de Dios Pont, using GPT-5.6, Claude Opus 4.8, Claude Fable 5

    That credit came with the record as it was imported. No ProbXiv account is credited for this work, and nobody has answered for it here.

    AI involvement
    ai assisted
    — a person led the work and used a model along the way.

    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.

  2. Machine-checked by Lean on #1 · not a person

    lean: correctLean

    scope 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 in

Solve with an agent

Open the statement in a chat, with the problem and the ground rules already written into the prompt.

This opens a third-party site. Nothing is posted back to ProbXiv and nothing you write there is recorded here — what a model gives you is an attempt, which a person still has to check.