Planar Schiffer and Pompeiu conjectures disproved by two independent groups
One proof has a Lean certificate written by GPT-5.6
Event confirmedAwaiting review
Importance: major (4 of 5)The takeaway
In August 2026 two groups independently disproved Schiffer’s conjecture (Yau’s Problem 80) and the planar Pompeiu problem (1929).
Status
- Claim
Event confirmedAwaiting review
- Our reporting
- High confidence
- Verification
- Lean-verified
- Importance
- Major (4 of 5)
- Last verified
- 30 September 2026
Your AI and this story
- GPT-6 Astra95 days after its cutoff
- Claude Opus 5.534 days after its cutoff
- Gemini 4 Hydrogen125 days after its cutoff
- Grok 4.764 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 34 days before it.
Key facts
- Schiffer’s conjecture: if a smooth domain has a Neumann eigenfunction that is constant on the boundary, the domain is a ball (Problem 80 in Yau’s 1982 problem list). The planar Pompeiu problem dates to Pompeiu’s papers of 1929
- Colbrook & Stepaniants (arXiv 2608.01579, 3 Aug 2026): one bounded, simply connected, non-circular domain with real-analytic boundary, close to an explicit degree-301 polynomial conformal map with ten-fold symmetry; eigenvalue k in (31.967007261, 31.967007293); existence certified by an interval-arithmetic contraction argument
- Colbrook & Stepaniants AI declaration: ‘ChatGPT 5.5 in the form of codex was used to help debug an early version of some of the code. All of its outputs were checked line by line by the authors.’
- Cao-Labora & de Dios Pont (arXiv 2608.05114, 5 Aug 2026): infinitely many N-fold symmetric counterexamples for large N. They relax N to a real parameter and use bifurcation theory with branch size uniform in N. No computer assistance is needed in the proof
- Cao-Labora & de Dios Pont AI usage: ‘LLMs, in the form of GPT 5.5 and 5.6, Claude Opus 4.8 and Claude Fable 5’ were used to numerically verify asymptotic estimates, draft first versions of the Bessel-function estimate proofs and help with exposition; ‘The Lean4 verification of the proof was written by GPT 5.6’
- Lean repository jaumededios/Schiffer (created 4 Aug 2026) contains challenge files for Schiffer’s conjecture and for the Pompeiu statement in Google DeepMind’s Formal Conjectures repository. It follows a slightly different route from the paper because Mathlib lacks elliptic regularity
- Follow-up (arXiv 2608.08953, 9 Aug): Colbrook, Sadeghi and Stepaniants disproved the unrestricted planar Berenstein conjecture (the Dirichlet counterpart). Their AI declaration says ChatGPT 5.6 ‘suggested ideas contributing to early versions of Lemma 3.2 and Proposition 3.5, as well as to a revised version of the code’, starting from a warm start of the authors’ own draft and code
- Colbrook presented the result as ‘A Shortcake Counterexample to the Planar Pompeiu and Schiffer Conjectures’ at Princeton (PACM seminar, 16 Sep 2026)
Show 1 more
- Status: preprints, not yet peer-reviewed; the Cao-Labora–de Dios Pont proof is Lean-checked
What happened
On 3 August 2026 Matthew Colbrook and George Stepaniants posted a counterexample to the planar Pompeiu and Schiffer conjectures. They found a domain numerically, then proved that an exact counterexample exists near it with an interval-arithmetic contraction argument. Two days later Gonzalo Cao-Labora and Jaume de Dios Pont posted an independent construction of infinitely many counterexamples. Their method is bifurcation theory with a real-valued symmetry parameter. It is purely analytic, and their Lean certificate was written by GPT-5.6. Cao-Labora and de Dios Pont note in their paper that Colbrook and Stepaniants posted an independent construction two days earlier. On 9 August Colbrook’s group used the same machinery to disprove the planar Berenstein conjecture, this time with ChatGPT 5.6 contributing ideas to some lemmas.
Why it matters
Schiffer’s conjecture is a classic rigidity question and appears on Yau’s list of open problems. The episode shows the range of AI roles in mid-2026 papers on the same problem. In one paper it only debugged code. In another it checked estimates, drafted proofs and wrote the full formal verification. In a third it proposed ideas that the authors then developed.
What is disputed or not yet verified
| Verification | Computer-assisted interval certificate (Colbrook–Stepaniants); Lean 4 formalisation (Cao-Labora–de Dios Pont); not yet peer-reviewed |
|---|
Sources
7 sources from 5 sites. Numbers match the chips in the text.
7 sources: 5 primary, 2 reactions
Primary
- arXiv 2608.01579: A computer-assisted counterexample to the planar Pompeiu and Schiffer conjectures (Colbrook, Stepaniants)arxiv.org, paper
- arXiv 2608.05114: Counterexamples to Schiffer’s Conjecture (Cao-Labora, de Dios Pont)arxiv.org, paper
- GitHub: jaumededios/Schiffer (Lean 4 formalisation)github.com, code
- Zenodo: Pompeiu–Schiffer validation certificate (Colbrook)zenodo.org, code
- arXiv 2608.08953: A computer-assisted counterexample to the planar Berenstein conjecturearxiv.org, paper
Reactions
- Princeton PACM seminar: A Shortcake Counterexample to the Planar Pompeiu and Schiffer Conjecturespacm.princeton.edu, discussion
- Wikipedia: Pompeiu problemen.wikipedia.org, discussion
Changes
- Filed