Analysis · Partial differential equations · Spectral geometry · Conjecture
Schiffer and Pompeiu conjectures
Must a bounded simply connected planar domain be a disk if it supports a nonconstant Helmholtz solution with constant boundary value and zero normal derivative?
DisprovedOpenMath assessment · Oct 13, 2026
- Literature: 2 preprints · 3 projects
- Formal: 3 complete proofs
- Computation: None recorded
- Review: Not yet reviewed
Frontier 1 report →
Earlier version 5 of this page. View current →
Overview
Known
The cited August papers give two distinct planar non-disk constructions: a certified analytic tenfold witness and an infinite smooth bifurcation family. Their formal and computational evidence have different exact scopes.
Latest
Precise statement
Let Ω be a bounded simply connected planar domain with smooth boundary. Schiffer’s rigidity question assumes a positive eigenvalue λ and a nonconstant real solution of Δu + λu = 0 in Ω, with u = 1 and ∂νu = 0 on the boundary. The value one is a normalization. The related Pompeiu question asks whether every non-disk such domain has the Pompeiu property: a continuous function whose integral over every rigid copy of Ω vanishes must be identically zero.
Definitions
- Overdetermined boundary conditions
- The Helmholtz solution has both constant boundary value and zero normal derivative. A domain satisfying both need not be circular in the cited constructions.
Background
Question paraphrased by OpenMath. Original wording is available in the sources.
Landscape
Figures and explorable examples. Selecting a statement opens its exact wording.
The certified tenfold domain
Ten shallow petals: the boundary is real-analytic and not a circle (the certificate proves |p₁| ≥ 12, so φ is not linear). It is drawn from the certificate's centre; the certificate proves a true solution within radius 10⁻⁶ of that centre in its weighted coefficient norm.
Visual setup
A noncircular domain with overdetermined boundary data
The question concerns a single simply connected domain supporting the interior equation and both boundary conditions.
Reading boundary. This illustrative outline is neither the tenfold certificate centre nor a member of the proved bifurcation family. It displays the common geometric setup without claiming a numerical witness.
Read the disk-rigidity statementQuestion scopeInspect the analytic construction● Proved under stated assumptionsInspect the smooth family● Proved under stated assumptions
The two constructions share this setup but have different geometry and evidence.
Results
The question 1
- DisprovedPlanar disk rigidity for overdetermined Helmholtz dataColbrook & Stepaniants 2026
The positive rigidity assertion is refuted by the analytic and smooth constructions.
Conjecture · Primary formulation
DisprovedColbrook & Stepaniants 2026Planar disk rigidity for overdetermined Helmholtz data
Every bounded simply connected planar domain Ω with C∞ boundary admitting a nonconstant smooth real u and λ > 0 with in Ω, u = 1 and on ∂Ω is a disk.Assumptions
- Bounded simply connected planar domain with smooth boundary.
- A positive eigenvalue and a nonconstant smooth solution up to the boundary.
In this problem
The positive rigidity assertion is refuted by the analytic and smooth constructions. The C² Lean construction has a separately stated regularity scope.
Sources
Counterexamples 3
- ProvedAn analytic tenfold counterexampleColbrook & Stepaniants 2026Formalized
The narrow k interval belongs to the numerical certificate.
Theorem · Counterexample
ProvedColbrook & Stepaniants 2026An analytic tenfold counterexample
There exist a bounded simply connected non-disk Ω with real-analytic Jordan boundary and tenfold symmetry, a nonconstant classical real u and such that in Ω, u = 1 and on ∂Ω.Assumptions
- Planar domain; real-analytic boundary.
- The exact construction and certified bounds of Colbrook–Stepaniants.
- Geometry
- Simply connected non-disk; tenfold symmetry
- Boundary / field
- Real-analytic Jordan boundary; classical real field
- Numerical input
- k ∈ (31.967007261,31.967007293); eigenvalue λ = k²
- Evidence scope
- Numerical certificate and separately linked complete formal proof; the latter uses coarser exact bounds at the same dyadic centre
In this problem
The narrow k interval belongs to the numerical certificate. The corresponding eigenvalue is k², not k.
Formal proofs
- Analytic tenfold Schiffer and Pompeiu counterexample ↗Complete formal proof reported externally
Sources
- ProvedInfinitely many smooth symmetry ordersCao-Labora & Jaume de Dios Pont 2026
Cao-Labora–de Dios Pont’s uniform bifurcation theorem supplies an infinite family without a numerical certificate.
Theorem · Counterexample
ProvedCao-Labora & Jaume de Dios Pont 2026Infinitely many smooth symmetry orders
For infinitely many integers N ≥ 2 there are a bounded simply connected star-shaped non-disk Ω with C∞ boundary and N-fold symmetry, λ > 0 and a nonconstant satisfying in Ω, u = 1 and on ∂Ω.Assumptions
- Planar star-shaped domains with smooth boundary.
- Existence for infinitely many integer symmetry orders, not a prescribed N.
- Geometry
- Star-shaped non-disks for infinitely many N ≥ 2
- Boundary / field
- C∞ boundary and field on the closure
- Numerical input
- Uniform bifurcation argument; no numerical certificate
- Evidence scope
- Smooth manuscript family; its exact infinite-family scope is not claimed by the C² formal statement
In this problem
Cao-Labora–de Dios Pont’s uniform bifurcation theorem supplies an infinite family without a numerical certificate.
Sources
- ProvedA formal non-disk failing the Pompeiu propertyJaume de Dios Pont & Cao-LaboraFormalized
The theorem derives Pompeiu failure from its own Schiffer witness through Green’s identity.
Theorem · Counterexample
ProvedJaume de Dios Pont & Cao-LaboraA formal non-disk failing the Pompeiu property
There exist a nonempty bounded star-shaped planar non-disk Ω with C² boundary and a continuous real f, not identically zero, such that the integral of f over every rigid-motion image of Ω equals zero.Assumptions
- Planar Lebesgue measure and all affine isometries.
- The star-shaped C² witness provided by the cited formal construction.
In this problem
The theorem derives Pompeiu failure from its own Schiffer witness through Green’s identity. It is a related conclusion, not a third geometric construction.
Formal proofs
- Star-shaped C² Pompeiu counterexample ↗Complete formal proof reported externally
Sources
Conditional implications 1
- ProvedFrom boundary data to vanishing domain averagesJaume de Dios Pont & Cao-Labora
The implication needs its stated boundary regularity and field assumptions.
Theorem · Conditional implication
ProvedJaume de Dios Pont & Cao-LaboraFrom boundary data to vanishing domain averages
For any bounded planar domain Ω with C² boundary, if a global C² real field u satisfies −Δu = u in Ω, u = 1 and ∇u = 0 on ∂Ω, then there exists a continuous real f, not identically zero, with integral zero over every rigid-motion image of Ω.Assumptions
- C² boundary in the defining-function sense of the cited formal source.
- Planar Lebesgue integration and all affine isometries; the global C² field satisfies the normalized equation.
In this problem
The implication needs its stated boundary regularity and field assumptions. It does not classify every domain failing the Pompeiu property or assert an equivalence for rough domains.
Sources
Variants and analogues 1
- DisprovedThe planar Pompeiu property questionColbrook & Stepaniants 2026
A related rigidity formulation through domain integrals.
Conjecture · Different statement · related variant
DisprovedColbrook & Stepaniants 2026The planar Pompeiu property question
Every bounded simply connected planar non-disk Ω with smooth boundary has the Pompeiu property: if a continuous real f has integral zero over every rigid-motion image of Ω, then f is identically zero.Assumptions
- Rigid motions include translations and orthogonal transformations.
- Integration is with respect to planar Lebesgue measure.
In this problem
A related rigidity formulation through domain integrals. Its counterexample evidence is linked to the specific constructions.
Sources
Background 1
- ProvedThe normalized C² formal statementJaume de Dios Pont & Cao-LaboraFormalized
The linked formal statement uses eigenvalue one after dilation and a vanishing full boundary gradient.
Theorem · Supporting result
ProvedJaume de Dios Pont & Cao-LaboraThe normalized C² formal statement
There exist a nonempty bounded star-shaped planar non-disk Ω with C² boundary and a global real C² field u such that in Ω, u = 1 and on ∂Ω.Assumptions
- C² boundary is specified by a global C² defining function with nonzero gradient on its zero set.
- Star-shaped about the origin; hence the domain is contractible and simply connected.
- Geometry
- Nonempty bounded star-shaped non-disk
- Boundary / field
- C² boundary; global real C² field
- Numerical input
- Eigenvalue one after dilation; full boundary gradient zero
- Evidence scope
- Complete formal proof reported for this normalized C² statement
In this problem
The linked formal statement uses eigenvalue one after dilation and a vanishing full boundary gradient. It does not claim the analytic frequency interval or the manuscript’s C∞ regularity.
Formal proofs
- Star-shaped C² Schiffer counterexample ↗Complete formal proof reported externally
Sources
Compare statements · 3
Each row is a separate assertion. Its assumptions determine which question it answers.
| Statement | Geometry | Boundary / field | Numerical input | Evidence scope |
|---|---|---|---|---|
| An analytic tenfold counterexample → Proved Exact statement & sources | Simply connected non-disk; tenfold symmetry | Real-analytic Jordan boundary; classical real field | k ∈ (31.967007261,31.967007293); eigenvalue λ = k² | Numerical certificate and separately linked complete formal proof; the latter uses coarser exact bounds at the same dyadic centre |
| Infinitely many smooth symmetry orders → Proved Exact statement & sources | Star-shaped non-disks for infinitely many N ≥ 2 | C∞ boundary and field on the closure | Uniform bifurcation argument; no numerical certificate | Smooth manuscript family; its exact infinite-family scope is not claimed by the C² formal statement |
| The normalized C² formal statement → Proved Exact statement & sources | Nonempty bounded star-shaped non-disk | C² boundary; global real C² field | Eigenvalue one after dilation; full boundary gradient zero | Complete formal proof reported for this normalized C² statement |
Infinitely many smooth symmetry orders →
The normalized C² formal statement →
Connections
Analogues and related questions 1
The normalized C² formal statement related to A formal non-disk failing the Pompeiu property.
Scope comparisonThe project derives a nonzero test function with vanishing rigid-domain integrals from the normalized Schiffer field using Green’s identity.
Limit This records the source’s construction-specific implication; it is not an equivalence for arbitrary rough domains.
Sources & review
- Lean proof of the star-shaped Schiffer/Pompeiu construction ↗Schiffer.Comparator.Schiffer_Star_Shaped and Pompeiu_Star_Shaped; simply-connected corollaries
Independent relationship review: not recorded. Link to this connection
Consequences 1
Assuming The normalized C² formal statementProved
From boundary data to vanishing domain averages
Under stated assumptionsFor any bounded planar domain Ω with C² boundary, if a global C² real field u satisfies −Δu = u in Ω, u = 1 and ∇u = 0 on ∂Ω, then there exists a continuous real f, not identically zero, with integral zero over every rigid-motion image of Ω.
Limit The implication needs its stated boundary regularity and field assumptions. It does not classify every domain failing the Pompeiu property or assert an equivalence for rough domains.
Sources & review
- Lean proof of the star-shaped Schiffer/Pompeiu construction ↗Schiffer.Comparator.Schiffer_Star_Shaped and Pompeiu_Star_Shaped; simply-connected corollaries
Source-grounded explanation · independent explanation review: pending.
Approaches
How the problem is attacked, and what each line of attack cannot yet reach.
One boundary with two conditions
Constant boundary value and zero normal derivative overdetermine the Helmholtz equation. The constructions arrange noncircular geometry while satisfying both.
Cannot yet reach The domain must remain simply connected; examples on annuli would not refute this question.
- Planar disk rigidity for overdetermined Helmholtz data (Disproved)
- An analytic tenfold counterexample (Proved)
- Infinitely many smooth symmetry orders (Proved)
Sources & review
Supporting statements
- Planar disk rigidity for overdetermined Helmholtz data →
- An analytic tenfold counterexample →
- Infinitely many smooth symmetry orders →
- A computer-assisted counterexample to the planar Pompeiu and Schiffer conjectures ↗Main theorem, computational certificate appendix and AI declaration
- Counterexamples to Schiffer’s Conjecture ↗Theorem 1.1, Corollary 1.2 and AI/Lean acknowledgement
Source-grounded explanation · independent explanation review: pending.
Timeline
The analytic certificate receives a public Lean replayFormalization
The verification record reports a standard-kernel statement comparison after a complete Lean build.
This formal project belongs to Colbrook–Stepaniants’ analytic construction, separately from de Dios Pont’s C² bifurcation project.
- Lean proof of the analytic tenfold construction ↗PompeiuSchiffer.Numerics.UnconditionalCounterexamples.exists_common_domain; Comparator definitions and verification record
An infinite family by uniform bifurcationRelated result
Cao-Labora and de Dios Pont publish smooth star-shaped counterexamples for infinitely many symmetry orders.
The linked earlier-draft Lean statement asserts C² regularity and follows a modified analytic path.
- Counterexamples to Schiffer’s Conjecture ↗Theorem 1.1, Corollary 1.2 and AI/Lean acknowledgement
- Lean proof of the star-shaped Schiffer/Pompeiu construction ↗Schiffer.Comparator.Schiffer_Star_Shaped and Pompeiu_Star_Shaped; simply-connected corollaries
An analytic computer-assisted constructionRelated result
Colbrook and Stepaniants publish the tenfold counterexample and a certificate archive.
Rigorous interval and tail estimates certify an exact domain; a floating-point drawing alone would not do so.
- A computer-assisted counterexample to the planar Pompeiu and Schiffer conjectures ↗Main theorem, computational certificate appendix and AI declaration
- Numerical certificate and reproduction report ↗REPRODUCTION_REPORT.md; validation archive; Zenodo DOI 10.5281/zenodo.21765287
Pompeiu asks whether domain averages determine a functionFoundation
The cited papers trace the integral-geometric question to Pompeiu.
Topology and boundary regularity must be fixed when stating the disk-rigidity conjecture.
- A computer-assisted counterexample to the planar Pompeiu and Schiffer conjectures ↗Main theorem, computational certificate appendix and AI declaration
- Counterexamples to Schiffer’s Conjecture ↗Theorem 1.1, Corollary 1.2 and AI/Lean acknowledgement
Evidence
| Literature | Status OpenMath assessment · Oct 13, 2026.
|
|---|---|
| Formal | Reported in sources: Pinned formal statements and the computational archive are linked to their own targets. External build reports and independent mathematical assessment remain separate from OpenMath execution. |
| Computation | None recorded |
| Review | Not yet reviewed OpenMath assessment: The cited August papers give two distinct planar non-disk constructions: a certified analytic tenfold witness and an infinite smooth bifurcation family. Their formal and computational evidence have different exact scopes. Source comparison and reader curation; independent mathematical assessment remains pending. OpenMath pilot collection · OpenMath source curation · assessed Oct 13, 2026 · review due Jan 13, 2027 Collection last checked Oct 13, 2026. |
Formalizations
The normalized C² formal statement →
Star-shaped C² Schiffer counterexampleComplete formal proof reported externally
Complete formal proof reported externally
Exact global C² normalized statement. Smoothness, the tenfold analytic frequency interval and every symmetry order are not attributed to this declaration.
Statement match: Linked by OpenMath · independent review separate · checked Oct 13, 2026
Declaration & revision
Schiffer.Comparator.Schiffer_Star_ShapedCommit 2938e277969c329caf154e48a3d8823f3635c7f1
A formal non-disk failing the Pompeiu property →
Star-shaped C² Pompeiu counterexampleComplete formal proof reported externally
Complete formal proof reported externally
A continuous nonzero real test function has zero integral over every rigid copy of the formal domain. The simply-connected corollary follows from contractibility.
Statement match: Linked by OpenMath · independent review separate · checked Oct 13, 2026
Declaration & revision
Schiffer.Comparator.Pompeiu_Star_ShapedCommit 2938e277969c329caf154e48a3d8823f3635c7f1
An analytic tenfold counterexample →
Analytic tenfold Schiffer and Pompeiu counterexampleComplete formal proof reported externally
Complete formal proof reported externally
The full statement includes real-analytic Jordan boundary, tenfold dihedral symmetry, the published frequency interval, a real analytic classical Schiffer field and Pompeiu failure. The formal proof checks its own coarser exact numerical bounds using the same dyadic centre as the interval certificate.
Statement match: Linked by OpenMath · independent review separate · checked Oct 13, 2026
Declaration & revision
PompeiuSchiffer.Numerics.UnconditionalCounterexamples.exists_common_domainCommit 2fb3f2ecafd3233dbca390d73e764fe6e04a9c7d
External proof reports do not establish an OpenMath run, independent statement correspondence, or independent mathematical review.
Sources
Choose a starting point below. Each result links to its exact statement, cited passages and checks.
Start here
- Proof source
A computer-assisted counterexample to the planar Pompeiu and Schiffer conjectures →Read the mathematical argument; inspect its statement for assessment and scope.
- Proof source
Counterexamples to Schiffer’s Conjecture →Read the mathematical argument; inspect its statement for assessment and scope.
- Formal source
Lean proof of the star-shaped Schiffer/Pompeiu construction →Inspect the formal statement, assumptions and reported checks.
- Formal source
Lean proof of the analytic tenfold construction →Inspect the formal statement, assumptions and reported checks.
Bibliography 5
- A computer-assisted counterexample to the planar Pompeiu and Schiffer conjectures →
Matthew J. Colbrook · George Stepaniants · Preprint · Aug 3, 2026
Main theorem, computational certificate appendix and AI declaration
- Counterexamples to Schiffer’s Conjecture →
Gonzalo Cao-Labora · Jaume de Dios Pont · Preprint · Aug 5, 2026
Theorem 1.1, Corollary 1.2 and AI/Lean acknowledgement
- Lean proof of the star-shaped Schiffer/Pompeiu construction →
Jaume de Dios Pont · Gonzalo Cao-Labora · Project documentation
Schiffer.Comparator.Schiffer_Star_Shaped and Pompeiu_Star_Shaped; simply-connected corollaries
- Numerical certificate and reproduction report →
Matthew J. Colbrook · George Stepaniants · Project documentation
REPRODUCTION_REPORT.md; validation archive; Zenodo DOI 10.5281/zenodo.21765287
- Lean proof of the analytic tenfold construction →
Matthew J. Colbrook · George Stepaniants · Project documentation
PompeiuSchiffer.Numerics.UnconditionalCounterexamples.exists_common_domain; Comparator definitions and verification record
Research activity · 1 entry
Formalization
Compare the two evidence routes
The analytic witness has frozen numerical input data and a certificate; the bifurcation construction has a separate C² formal theorem.
Neither external project has been executed by OpenMath.
Related statements · context, not additional proved progress
Numerical certificate and reproduction report · sources & artifacts →
Lean proof of the star-shaped Schiffer/Pompeiu construction · sources & artifacts →
Lean proof of the analytic tenfold construction · sources & artifacts →
Selected literature; source observations and coverage limits are retained in the publication details.
Contributors
Colbrook and George Stepaniants own the analytic construction; Cao-Labora and Jaume de Dios Pont own the smooth family. Their AI disclosures describe different roles. The formal Pompeiu statement credits Himanshu Gupta and Moritz Firsching’s Google DeepMind Formal Conjectures statement; this is statement provenance, not discovery credit.
Authors & roles
A computer-assisted counterexample to the planar Pompeiu and Schiffer conjectures →
Matthew J. Colbrook · George Stepaniants
The paper credits GPT-5.5 Codex for debugging early computational code, checked line by line by the authors. The authors own the mathematical argument and certificate.
Counterexamples to Schiffer’s Conjecture →
Gonzalo Cao-Labora · Jaume de Dios Pont
The authors credit GPT-5.5/5.6 and Claude Opus 4.8/Fable 5 for exploration, checks and exposition; GPT-5.6 assisted the early-draft Lean verification. The authors retain responsibility.
Lean proof of the star-shaped Schiffer/Pompeiu construction →
Jaume de Dios Pont · Gonzalo Cao-Labora
The repository attributes formalization to OpenAI Codex. Its metadata reports agent review rather than independent human peer review. The formal path and C² scope differ from the later smooth manuscript.
Numerical certificate and reproduction report →
Matthew J. Colbrook · George Stepaniants
No specific AI contribution is attributed by this source record.
Lean proof of the analytic tenfold construction →
Matthew J. Colbrook · George Stepaniants
No specific AI contribution is attributed by this source record.
These are source credits; they do not imply OpenMath accounts, endorsements or independent mathematical review.
Record details
- Record version
- 5
- Classification
- MSC2020 35P05 / 35N25
- Prerequisite level
- graduate