Plectis Atlas
Search

↑ and ↓ move, Enter opens, Esc closes.

Show on the map

Joint metric and connection recovery from one boundary patch

OpenAI groups related papers into a “family”. OpenAI’s catalogue describes this one:

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. (OpenAI’s Lean note)

Lean is a language for mathematical statements and proofs that a computer can verify. The assessments below ask whether those statements express the result OpenAI describes here.

The independent assessments find that the Lean statements express only part of the result described above, or a narrower statement. Read the assessments

The paper states

Theorem 1.1 (Smooth anisotropic uniqueness from one patch)

In Smooth anisotropic uniqueness in the Calderón problem from one boundary patch, 24 September 2026

Possible match to OpenAI’s description, selected from the papers’ main statements because it shares the most wording. No review confirming the selection is recorded.

Five other possible matches are listed below the card, among them Corollary 1.2 (Localized nonuniqueness) in Nonuniqueness for bounded measurable scalar conductivities in three dimensions and Corollary 1.2 (Full-boundary uniqueness) in the same paper.

Let n\ge3. Let M be a compact connected smooth n-manifold with nonempty smooth boundary, and let \Gamma\subset\partial M be nonempty, proper, and relatively open. If two smooth Riemannian metrics g_1,g_2 on M satisfy

\Lambda_{g_1,\Gamma}=\Lambda_{g_2,\Gamma},

then there is a smooth diffeomorphism \Phi:M\to M, smooth through the boundary, such that

\Phi|_\Gamma=\Id,\qquad g_2=\Phi^*g_1.

No Lean statement in the release is paired with this theorem.

Five more possible matches

  • Corollary 1.2 (Localized nonuniqueness) in Nonuniqueness for bounded measurable scalar conductivities in three dimensions, 23 September 2026.
  • Corollary 1.2 (Full-boundary uniqueness) in Smooth anisotropic uniqueness in the Calderón problem from one boundary patch, 24 September 2026.
  • Theorem 1.1 in Nonuniqueness for bounded measurable scalar conductivities in three dimensions, 23 September 2026.
  • Theorem 1.1 in Determination of a metric and a unitary connection from one boundary patch, 5 October 2026.
  • Corollary 1.3 (Smooth scalar uniqueness from one patch) in Smooth anisotropic uniqueness in the Calderón problem from one boundary patch, 24 September 2026.
Reported proof verification
One Lean statement in the release; two independent groups report that Comparator accepted runs for this file at the version shown here.
Papers and explanations
Three current papers, each readable here as a page beside its PDF.

Papers

Each paper opens as a reading page in the browser, with the PDF beside it. The statements each paper opens with are on its reading page.

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

5 October 2026, current edition.

Read it herePDF

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.

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

24 September 2026, current edition.

Read it herePDF

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.

One Lean statement in this family

Lean is a language for mathematical statements and proofs that a computer can verify. The Lean statement below is shown beside its possible paper counterpart, with the reason they were linked.

For a configured theorem, the Comparator program tests whether OpenAI’s separate proof proves the exact Lean statement using only the allowed axioms. Some statement files instead configure definitions for comparison by name and type. Acceptance does not establish that a formal statement means the same thing as the paper’s theorem.

Conductivity

The paper states

Corollary 1.2 (Localized nonuniqueness)

In Nonuniqueness for bounded measurable scalar conductivities in three dimensions, 23 September 2026

Let c,C be the constants in Theorem 1.1. For every bounded connected Lipschitz domain \Omega\subset\R^3 and every finite family of pairwise disjoint balls B_1,\ldots,B_m\Subset\Omega, m\geq1, there are 2^m pairwise distinct real scalar conductivities \gamma_\varepsilon\in L^\infty(\Omega), indexed by \varepsilon\in\{0,1\}^m, such that

c\leq\gamma_\varepsilon\leq C\quad\text{almost everywhere}, \qquad \gamma_\varepsilon=1\quad\text{on } \Omega\setminus\bigcup_{i=1}^m B_i,

and all their full weak Dirichlet-to-Neumann operators from H^{1/2}(\partial\Omega) to H^{-1/2}(\partial\Omega) agree. Distinct conductivities differ on a set of positive measure.

The words they share: bounded, conductivities, differ, dirichlet, full, main, neumann, nonuniqueness, positive, scalar, weak.

Possible Lean counterpart

Selected from shared wording. No review of whether the statements mean the same thing is recorded.

Scalar conductivity nonuniqueness

Conductivity.lean, the release lists it as a main result.

def MainStatement : Prop :=  ∃ (γ₀ γ₁ : R3 → ℝ) (c C : ℝ) (Λ : DNOperator),    0 < c ∧ c < C ∧    Measurable γ₀ ∧ Measurable γ₁ ∧    MemLp γ₀ ∞ ballMeasure ∧ MemLp γ₁ ∞ ballMeasure ∧    (∀ᵐ x ∂ballMeasure, c ≤ γ₀ x ∧ γ₀ x ≤ C) ∧    (∀ᵐ x ∂ballMeasure, c ≤ γ₁ x ∧ γ₁ x ≤ C) ∧    EqualOneNearBoundary γ₀ ∧ EqualOneNearBoundary γ₁ ∧    0 < ballMeasure {x | γ₀ x ≠ γ₁ x} ∧    IsDirichletToNeumann γ₀ Λ ∧ IsDirichletToNeumann γ₁ Λtheorem main_nonuniqueness : MainStatement := by  sorry

This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.

two independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet. Who ran the proof-verification program

  • cert-machine records it as “CERTIFIED”.
  • MathVet records it as “comparator-sandboxed-pass”.

Read the complete Lean statement

Other mathematical statements in OpenAI’s Lean library

Atlas found these propositions by scanning the text of the project’s Model.lean file. Each name links to its definition, with any associated statement file beside it. This list does not record running Lean to interpret or verify those definitions.

Independent comparisons and proof-verification reports

Does the Lean express the advertised result?

Neither group finds that the Lean statements express or imply the whole advertised result. They describe what the statements express in different terms.

MathVet and Carlos Toledo’s cert-machine independently assessed whether this family’s Lean statements express the whole result OpenAI describes in its catalogue. These are assessments of the family as a whole, not of each paper theorem separately.

MathVet finds that the Lean statements express part of the advertised result (their term: “partial”).

Their note: main_nonuniqueness covers only the contrast claim: on the ball B(0,3) ⊂ ℝ³ there are two bounded measurable conductivities in [c, C], both equal to 1 near the boundary, differing on a positive-measure set, with one and the same weak Dirichlet-to-Neumann operator Λ (IsDirichletToNeumann: for every trace a unique harmonic H¹ extension with Λ f (trace v) = ∫γ∇u·∇v). The summary’s first-named result, recovery of a smooth metric and unitary connection on a rank-two Hermitian bundle over manifolds of dimension ≥ 3 from zero-frequency data on one boundary patch (up to diffeomorphism and gauge), has no statement; the docs scope also only describes the conductivity result.

Definitions the group asks readers to compare with the paper: H¹(B) is hand-built as the closure of smooth jets (f, ∇f) in L²(B; ℝ⁴), H¹₀ as the closure of compactly supported jets, TraceSpace := H1 ⧸ H10, and the DN operator is a continuous bilinear map TraceSpace → TraceSpace*; EqualOneNearBoundary is only a.e. in r < ‖x‖ < 3

“partial”, in their words: Only a special case is stated, or a co-equal headline claim has no challenge statement.

Their method: An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.

Read the original assessment Read MathVet’s method

cert-machine finds that the Lean statements express a narrower statement than the advertised result (their term: “NARROWER — UNLINKED”).

The gap they name: The headline’s main theorem — joint recovery of a smooth metric and unitary connection from one boundary patch (and the metric-only same-patch Calderón uniqueness) — is not formalized; only the bounded-measurable scalar nonuniqueness example is.

“NARROWER — UNLINKED”, in their words: The challenge statements state less than the headline; the missing part comes from a paper the Lean note does not link.

Their method: Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule.

Read the original assessment Read cert-machine’s method

OpenAI’s own note on what its Lean covers

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.

AI-drafted comparisons, with no recorded human review

  • Scalar conductivity nonuniqueness Conductivity

    Unreviewed AI draft: states a paper’s theorem as the paper does. States the main theorem: two bounded measurable scalar conductivities on a ball, equal to 1 near the boundary and different on a set of positive volume, with the same Dirichlet-to-Neumann map. The localised corollary is not included.

Who ran the proof-verification program?

These groups report running Comparator with the release’s Lean statement files. For a configured theorem, it verifies OpenAI’s separate proof against the exact statement; some files instead configure definitions for comparison by name and type. Each row is the named group’s report. Atlas has not repeated the runs.

These reports do not list the software versions, proof-verification programs, axioms, time or memory in separate fields. Any such details in a report’s prose are reproduced below.

Scalar conductivity nonuniqueness Conductivity

Two reports, all at the release’s recorded version.

Reported byTheir wordTheir accountDateOriginal report
cert-machine“CERTIFIED”Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.10 October 2026Original report
MathVet“comparator-sandboxed-pass”Re-run through Comparator in a sandboxed virtual machine: accepted.8 October 2026Original report

What these papers cite in the release, and what cites them

These links come from the papers’ bibliographies. A citation records that one paper cites another; how each cited result is used has not been examined here.

Within this family

Papers elsewhere in the release that this family’s papers cite

This family’s papers cite no paper elsewhere in the release.

Papers elsewhere in the release that cite this family’s papers

No paper elsewhere in the release cites this family’s papers.

Explain a result, compare statements or propose a correction

Atlas has no contributed explanation for this family yet. You can offer one with a GitHub account. You receive named credit and disclose any AI assistance.

Each button opens a GitHub form with this page and its source version filled in. Opening the form does not reserve the work.

Offer to write an explanationCompare the Lean statement with the paperSuggest a source attributionSuggest a change

What people have said

Commentary on this family by others, dated and credited. It is commentary, not a finding.

  • An unsigned public tier list, the OpenAI Math Tier List, classes it as a proof and rates its significance, if it holds up, as “Major math journal”. The page says that nothing on it is verified.

    Author not stated. Source

Questions awaiting review

Each item identifies a statement, definition or report that needs further review. Its link opens a GitHub form with the source version already recorded.

Read the Lean statement against the paper

  • An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded. Open the form

Identify the theorem the catalogue describes

  • Family 365 The theorem shown was selected from shared wording with OpenAI’s description. Atlas records no review confirming that it is the theorem the description means. Open the form

Address a question raised in an independent assessment

Compare the proposed paper and Lean matches

  • Family 365 Atlas records no review of whether each linked Lean statement and paper theorem mean the same thing. Open the form