∑math20

Partial differential equations · Result 365

Joint metric and connection recovery from one boundary patch

3 papersLean

Zero-frequency measurements on any nonempty open boundary patch determine a smooth metric and smooth unitary connection on a trivial Hermitian rank-two bundle over a compact connected manifold of dimension at least three, up to diffeomorphism and gauge fixed on that patch. Inputs and observations use the same patch. In contrast, distinct uniformly positive bounded measurable scalar conductivities on a three-dimensional ball can have identical full-boundary data.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 3

First page of Determination of a metric and a unitary connection from one boundary patch

Determination of a metric and a unitary connection from one boundary patch

OpenAI · October 5, 2026

We prove that zero-frequency boundary measurements on any nonempty open boundary patch determine both a smooth Riemannian metric and a smooth unitary connection on the trivial Hermitian rank-two bundle over a compact connected smooth manifold of dimension at least three with smooth boundary. Both inputs and observations are restricted to the same patch. The metric and connection are determined up to a diffeomorphism and a unitary gauge that restrict to the identity on the measured patch.

Read PDF Download Source

Cite
@misc{OAI:Determination-of-a-metric-and-a-unitary-connection-from-one-boundary-patch-October-5-2026,
  author = {{OpenAI}},
  title = {{Determination of a metric and a unitary connection from one boundary patch}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Determination-of-a-metric-and-a-unitary-connection-from-one-boundary-patch-October-5-2026/paper.pdf}{OAI:Determination-of-a-metric-and-a-unitary-connection-from-one-boundary-patch-October-5-2026}},
  year = {2026}
}
First page of Smooth anisotropic uniqueness in the Calderón problem from one boundary patch

Smooth anisotropic uniqueness in the Calderón problem from one boundary patch

OpenAI · September 24, 2026

We resolve the smooth anisotropic Calderón uniqueness problem with arbitrary same-patch measurements. A smooth Riemannian metric on a compact connected manifold of dimension at least three is determined, up to a diffeomorphism fixing the measured patch, by its zero-frequency Dirichlet-to-Neumann energy form with both input and observation on any nonempty open boundary patch.

Read PDF Download Source

Cite
@misc{OAI:Smooth-Anisotropic-Uniqueness-in-the-Calderon-Problem-from-One-Boundary-Patch-September-24-2026,
  author = {{OpenAI}},
  title = {{Smooth anisotropic uniqueness in the Calder\'on problem from one boundary patch}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Smooth-Anisotropic-Uniqueness-in-the-Calderon-Problem-from-One-Boundary-Patch-September-24-2026/paper.pdf}{OAI:Smooth-Anisotropic-Uniqueness-in-the-Calderon-Problem-from-One-Boundary-Patch-September-24-2026}},
  year = {2026}
}
First page of Nonuniqueness for bounded measurable scalar conductivities in three dimensions

Nonuniqueness for bounded measurable scalar conductivities in three dimensions

OpenAI · September 23, 2026

We construct two distinct uniformly positive bounded measurable scalar conductivities on a ball in ℝ3 with the same full Dirichlet-to-Neumann operator. Both conductivities equal one near the boundary. This gives nonuniqueness in the scalar Calderón problem at bounded measurable regularity.

Read PDF Download Source

Cite
@misc{OAI:Nonuniqueness-for-Bounded-Measurable-Scalar-Conductivities-in-Three-Dimensions-September-23-2026,
  author = {{OpenAI}},
  title = {{Nonuniqueness for Bounded Measurable Scalar Conductivities in Three Dimensions}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Nonuniqueness-for-Bounded-Measurable-Scalar-Conductivities-in-Three-Dimensions-September-23-2026/paper.pdf}{OAI:Nonuniqueness-for-Bounded-Measurable-Scalar-Conductivities-in-Three-Dimensions-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The Calderón inverse problem asks whether boundary measurements determine an interior conductivity. The formalized result gives nonuniqueness for bounded measurable scalar conductivities on the ball \(B(0,3)\subset\mathbb R^3\): two uniformly positive conductivities differ on a set of positive volume, equal \(1\) near the boundary, and have the same full weak Dirichlet-to-Neumann operator. Weak solutions exist uniquely for every boundary trace.

Comparator links

ResultComparator statement
Scalar conductivity nonuniquenessConductivity.lean

Scope note on GitHub →