openmath.dev
Esc

Loading…

↑ ↓ to move↵ to open

Appearance
Appearance
← Problems

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
Frontier 1 report →
Cite & export
Open this versionExport record · JSONRecord detailsReport a correction
Use with an agent

Earlier version 2 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.

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.

−101Re−101ImScopethe unit circle, for comparisonProveda non-disk with overdeterminedHelmholtz data

Dataset schiffer-tenfold-domain v1 · The 31 shape coefficients of the certificate centre (pinned commit 2fb3f2e, data/center_L60_S40_R30.hex, sha256 a30353f2…3d29) are read as binary64; φ is evaluated at 360 equally spaced points of the unit circle. Σj≥1 |p_j/p_0| = 0.6492 (certificate bound 0.65). Software: python 3.12.13. binary64 evaluation of the published centre; a plot, not a proof. SHA-256 3a50ff388f8c… · Download JSON

Data
LayerStatus
Scope: the unit circle, for comparisonscope
Proved: a non-disk with overdetermined Helmholtz dataproved

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.

A noncircular domain with overdetermined boundary dataA noncircular outline surrounds an interior Helmholtz label. Two labels identify constant boundary value and zero normal derivative. The drawing has no hole.ΩΔu + λu = 0u = 1∂νu = 0Simply connected · no holes
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.

Text version

A noncircular outline surrounds an interior Helmholtz label. Two labels identify constant boundary value and zero normal derivative. The drawing has no hole.

Positive eigenvalue; constant boundary value normalized to one. The picture is a schematic, not a computed eigenfunction or certified domain.

  1. Read the disk-rigidity statement

    Disproved

    Planar disk rigidity for overdetermined Helmholtz data

    The positive rigidity assertion is refuted by the analytic and smooth constructions. The C² Lean construction has a separately stated regularity scope.

    Planar disk rigidity for overdetermined Helmholtz data →

  2. Inspect the analytic construction

    Proved

    An analytic tenfold counterexample

    The narrow k interval belongs to the numerical certificate. The corresponding eigenvalue is k², not k.

    An analytic tenfold counterexample →

  3. Inspect the smooth family

    Proved

    Infinitely many smooth symmetry orders

    Cao-Labora–de Dios Pont’s uniform bifurcation theorem supplies an infinite family without a numerical certificate.

    Infinitely many smooth symmetry orders →

Sources & review

Authored by OpenMath source curation on 2026-10-13 (AI-assisted curation). Independent review of this visual explanation is pending; linked assertions and relationships have their own assessments.

Results

The question 1

Counterexamples 3

  • Proved
    An analytic tenfold counterexample

    The narrow k interval belongs to the numerical certificate.

    Colbrook & Stepaniants 2026Formalized
  • Proved
    Infinitely many smooth symmetry orders

    Cao-Labora–de Dios Pont’s uniform bifurcation theorem supplies an infinite family without a numerical certificate.

    Cao-Labora & Jaume de Dios Pont 2026
  • Proved
    A formal non-disk failing the Pompeiu property

    The theorem derives Pompeiu failure from its own Schiffer witness through Green’s identity.

    Jaume de Dios Pont & Cao-LaboraFormalized

Conditional implications 1

  • Proved
    From boundary data to vanishing domain averages

    The implication needs its stated boundary regularity and field assumptions.

    Jaume de Dios Pont & Cao-Labora

Variants and analogues 1

Background 1

  • Proved
    The normalized C² formal statement

    The formal comparator uses eigenvalue one after dilation and a vanishing full boundary gradient.

    Jaume de Dios Pont & Cao-LaboraFormalized

Connections

Analogues and related questions 1

Consequences 1

Assuming The normalized C² formal statementProved

  • From boundary data to vanishing domain averages

    Under stated assumptions

    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 Ω.

    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

    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.

Sources & review

Supporting statements

Source-grounded explanation · independent explanation review: pending.

Timeline

  1. The analytic certificate receives a public Lean replayFormalization

    The verification record reports a standard Lean 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.

  2. 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.

  3. 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.

    Also on the Frontier: Planar Schiffer / Pompeiu rigidity

  4. 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.

Full history with sources →

Evidence

Literature

2 preprints · 3 projects

Status OpenMath assessment · Oct 13, 2026.

Formal

3 complete proofs

3 formalizations below ↓

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

Open formal source ↗

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_Shaped

Commit 2938e277969c329caf154e48a3d8823f3635c7f1

A formal non-disk failing the Pompeiu property →

Star-shaped C² Pompeiu counterexampleComplete formal proof reported externally

Open formal source ↗

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_Shaped

Commit 2938e277969c329caf154e48a3d8823f3635c7f1

An analytic tenfold counterexample →

Analytic tenfold Schiffer and Pompeiu counterexampleComplete formal proof reported externally

Open formal source ↗

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_domain

Commit 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

Bibliography 5

Research activity · 1 entry

Contributions

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 Pompeiu formal comparator credits Himanshu Gupta and Moritz Firsching’s Google DeepMind Formal Conjectures statement; this is statement provenance, not discovery credit.

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.

Record details
Record version
2
Classification
MSC2020 35P05 / 35N25
Prerequisite level
graduate
Source observations & version history →