Formally verified AI-assisted

Counterexamples to Schiffer's conjecture and the Pompeiu problem

Infinitely many planar domains that are not balls admit a Neumann eigenfunction of the Laplacian that is constant on the boundary, disproving Schiffer's conjecture and, through a classical equivalence, the 1929 Pompeiu problem.

Model
GPT-5.6, Claude Opus 4.8, Claude Fable 5
Field
Mathematics
Date
2026-08-05
Human collaborators
Gonzalo Cao-Labora, Jaume de Dios Pont
Problem posed
1929 · open 97 yrs

What was found

Pompeiu asked in 1929 whether a bounded domain over which some nonzero function integrates to zero under every rigid motion must be a ball. Schiffer's 1957 reformulation asks the same thing through Neumann eigenfunctions of the Laplacian that are constant on the boundary, and appears as Problem 80 on Yau's 1982 list; Williams proved the two formulations equivalent for simply connected domains in 1976. Cao-Labora and de Dios Pont construct infinitely many N-fold symmetric planar domains, with N large, that are not balls and carry such an eigenfunction. The strategy is to relax the problem so that N may be any real number, which corresponds to the Schiffer problem only at integers, apply bifurcation theory there, and show the size of the local bifurcation branch can be taken independently of N. Their Corollary 1.2 applies Williams' equivalence to the same domains, so a single construction settles both problems.

Novelty check

Schiffer's conjecture is Problem 80 on Yau's list, with a partial-results literature running since the 1970s, and the Pompeiu problem has stood since 1929. Both are recorded as open in the standard references and in DeepMind's formal-conjectures repository, which carries a Lean statement of the Pompeiu problem as an unsolved challenge that this work's formalization closes. No prior counterexample to either appears. The construction is new.

Caveats and known objections

A preprint, not peer-reviewed. The Lean 4 verification was written by GPT-5.6 from an early draft of the paper and lives in an author's own repository; it had no independent audit at entry time, and the same group produced both the proof and its formalization. Autonomy graded ai-assisted: the paper is explicit that the novel construction strategy is the authors' own, and that the models were used to verify the asymptotic estimates numerically, to produce first drafts of the proofs of the Bessel function estimates, and to help with exposition.

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.

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

Entry history (1 event)
  1. AddedEntered the registry graded Formally verified 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 formally verified for verification and ai-assisted for autonomy. What these mean.

Cite this entry

Plain text
whataifound.org. (2026). Counterexamples to Schiffer's conjecture and the Pompeiu problem. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-08-05-schiffer-conjecture
BibTeX
@misc{whataifound-independent-2026-conjecture,
  title        = {Counterexamples to Schiffer's conjecture and the Pompeiu problem},
  author       = {{whataifound.org}},
  year         = {2026},
  howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
  note         = {Result by Independent. Verification: Formally verified. Autonomy: AI-assisted.},
  url          = {https://whataifound.org/finding/2026-08-05-schiffer-conjecture}
}

Related findings

← All mathematics findings in the registry