The anisotropic Calderón problem
From OpenAI Aftermath
The anisotropic Calderón problem asks whether boundary measurements of the Dirichlet energy of harmonic functions determine a Riemannian metric on a compact manifold with boundary, up to the unavoidable change of interior coordinates that fixes the measured boundary. Three manuscripts in OpenAI's public mathematics collection (github.com/openai/math), dated 23 September to 5 October 2026, claim that in dimension at least three a smooth metric, and a smooth metric together with a unitary connection, are determined by measurements on any one open boundary patch, and that the scalar problem in three dimensions fails for bounded measurable conductivities. The nonuniqueness theorem has a Lean formalization. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper or a formal proof is not presented here as independent verification.
Background
- As recounted in the introductions of the manuscripts:
- Calderón formulated the inverse conductivity problem through boundary measurements of Dirichlet energy and proved injectivity of its linearization at constant conductivities. Sylvester and Uhlmann proved full-data uniqueness for smooth scalar conductivities in dimensions at least three; Haberman and Caro and Rogers lowered the regularity to W1,n in dimensions three and four and to Lipschitz conductivities, and in the plane Astala and Päivärinta proved uniqueness for bounded measurable conductivities.
- For anisotropic conductivities, Lee and Uhlmann proved boundary determination and real-analytic recovery, and Lassas and Uhlmann recovered a real-analytic manifold and metric from an arbitrary real-analytic boundary patch in dimensions at least three. Partial-data methods of Bukhgeim and Uhlmann, Kenig, Sjöstrand and Uhlmann, and Dos Santos Ferreira, Kenig, Salo and Uhlmann constrain the measurement regions or the background geometry. Recent full-data results by Lin and by Muñoz-Thon and Stefanov prove rigidity near the Euclidean metric and near conformally Euclidean metrics.
- Daudé, Kamran and Nicoleau combined Miller's nonunique-continuation construction with a conformal change to obtain anisotropic counterexamples with partial boundary data.
The original results
- Claim (smooth anisotropic uniqueness). Theorem 1.1 of Smooth anisotropic uniqueness in the Calderón problem from one boundary patch states that for n ≥ 3, if two smooth Riemannian metrics on a compact connected manifold with boundary have the same local Dirichlet-to-Neumann energy map on a nonempty proper open boundary patch, with both inputs and observations on that patch, then they differ by a smooth diffeomorphism that is the identity on the patch. Corollaries give full-boundary uniqueness and uniqueness of smooth scalar conductivities on Euclidean domains from one patch.
- Claim (metric and connection). The main theorem of Determination of a metric and a unitary connection from one boundary patch states that zero-frequency measurements on any nonempty open boundary patch determine a smooth metric and a smooth unitary connection on the trivial Hermitian rank-two bundle over a compact connected manifold of dimension at least three, up to a diffeomorphism and a unitary gauge that are the identity on the patch.
- Claim (scalar nonuniqueness). Theorem 1.1 of Nonuniqueness for bounded measurable scalar conductivities in three dimensions states that there are two scalar conductivities on the ball of radius 3 in ℝ3, bounded above and below by positive constants, equal to 1 near the boundary and different on a set of positive measure, with the same full Dirichlet-to-Neumann operator. A corollary gives 2m such conductivities on any bounded Lipschitz domain in ℝ3.
- Method, as described: for the smooth results, equal patch data first give equal boundary jets, and a small cap glued outside the patch makes the two Green kernels agree there. Harmonic functions with sources in the cap then label interior points, and the matched region is extended by moving harmonic functions across shrinking spheres, with an angular coercivity estimate as the central analytic step. The nonuniqueness construction uses a factor with a nonzero interior source and an annihilation identity, which changes the conductivity without changing any boundary measurement.
- Sources (openai/math repository, commit
7ef5c0c): Smooth anisotropic uniqueness in the Calderón problem from one boundary patch (24 September 2026); Determination of a metric and a unitary connection from one boundary patch (5 October 2026); Nonuniqueness for bounded measurable scalar conductivities in three dimensions (23 September 2026). - Formalization, as described by the repository. The scope note lean/docs/365.md covers only the nonuniqueness manuscript: two uniformly positive conductivities on the ball of radius 3 in ℝ3 differ on a set of positive volume, equal 1 near the boundary and have the same full weak Dirichlet-to-Neumann operator, with unique weak solutions for every boundary trace. The Comparator statement is
Conductivity.lean. The smooth uniqueness results are not formalized.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 30 October 2026) |
|---|---|---|---|---|
| 2026-10-06 | Metric and connection recovery from one boundary patch, an article of the Latent Seminar blog at lowrank.github.io | Reading (exposition) | Explains boundary energy measurements, smooth recovery and rough nonuniqueness, the gauge ambiguity, the proposed continuation mechanism, the matrix extension and the exact transformation behind rough nonuniqueness, with proof outlines. | Blog article; it states that its review covers statements, introductions and selected proof mechanisms and is not an independent verification of the complete proofs. |
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit 94c6630, 28 October 2026) |
Review (fidelity of the formal statements) | Rates this family "partial": the Lean statement covers only the scalar nonuniqueness claim on the ball, while the recovery of a metric and a unitary connection has no statement. It notes that the Sobolev spaces, the trace space and the Dirichlet-to-Neumann operator are hand-built. It records Comparator passes for Conductivity on its own machines and on cloud machines on 8 October 2026. |
MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-08 | L. Oksanen, l-oksanen/openai-calderon (GitHub, commit d1205fb) |
Formalization (challenge statement) | A Lean Comparator challenge for Theorem 1.1 of the smooth anisotropic manuscript, specialized to dimension three, the closed unit ball with full boundary data and metrics that are Euclidean outside the ball. The main statement is posed without proof, as a challenge; a test file proves the converse, that metrics related as in the conclusion have equal minimal Dirichlet energies. | Public repository; the challenge statement has no proof. |
| 2026-10-09 | C. I. Cârstea, T. Liimatainen, Y.-H. Lin and W. Trad, The conformal Poisson embedding method for the anisotropic Calderón problem with a potential (arXiv:2610.13592, v1) | Related (independent) | Proves that the local Dirichlet-to-Neumann map of Δg + q on an arbitrary open boundary set determines a compact connected real-analytic manifold of dimension at least three and a real-analytic potential, up to a diffeomorphism fixing the observed boundary and the conformal gauge. It cites the smooth anisotropic manuscript as an announcement, notes that the OpenAI results rest in part on the Poisson embedding and have no zeroth-order term, and states that the OpenAI preprints are not used and that its results do not follow from them. | arXiv preprint, version 1. |
| 2026-10-10 | cert-machine, openai/math lane K, run 38040214623 | Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept the Conductivity solution, in 2161 s. The project reports two-kernel certification of 398 of 416 challenges of the collection. |
Repository. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions does not list Conductivity, so it was accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-16 | J. Jardine, Lattice24, referee reviews rank_320 (smooth anisotropic manuscript) and rank_198 (metric and connection) in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995) | Review (AI-assisted audit) | Reports no gap in either manuscript, with minor notes that it states are not demonstrated gaps. For the smooth anisotropic manuscript: the parameter-dependent expansion of the moving-sphere Dirichlet-to-Neumann operator is only sketched, and the count of error terms in the angular coercivity estimate is argued by bookkeeping without a full expansion, which the reviewer names as the most likely place for a hidden failure. For the metric and connection manuscript: the reviewer notes that the result settles a well-known open problem, that its analytic weight rests on the angular coercivity estimate, and that some order and weight counts were only spot-checked. | Part of an audit that its README describes as complete for the collection's manuscripts without a Lean formalization. The reviews are published under CC BY 4.0. |
| 2026-10-19 | AI Proved What?, episode 365 One small patch sees everything?, remade version of 23 October 2026 | Reading (exposition) | Video explainer of the three claims. The episode states that stability, reconstruction, nonzero frequencies, smooth counterexamples and inputs and outputs on different patches are not claimed, and that specialists who cite the smooth papers describe them as an announcement, one of them noting that it is unclear whether they settle the linearized problem. | Web page and video; the site states that its scripts and animations are produced with AI assistance and that the narration is an AI-generated voice. Status record last checked 27 October 2026: posted as preprints: OpenAI, 50 + 43 + 33 pages, dated October 5, September 24 and September 23, 2026; under expert review: not yet; peer reviewed: not yet; checked in Lean: the rough nonuniqueness theorem only. The page states that it found no specialist verdict and no reported error. |
Notes
- The background summarizes the manuscripts' own account of earlier work.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
