Papers With

← All papers
First page of Formal Proof of an Anisotropic Calderón Uniqueness Theorem

Formal Proof of an Anisotropic Calderón Uniqueness Theorem

Cătălin I. Cârstea, Lauri Oksanen

math.AP Nov 7, 2026 · v1
formalization autoformalization mathlib analysis
Read PDF arXiv abstract Code
TL;DR
Formalizes in Lean 4, using Mathlib and Tau Ceti, a special case of the anisotropic Calderón uniqueness theorem, checked via a comparator challenge.
Abstract
We announce a Lean 4 formal proof of a special case of the smooth anisotropic Calderón uniqueness theorem released by OpenAI on October 6, 2026. We consider smooth Riemannian metrics on the three-dimensional unit ball, with full boundary measurements and Euclidean extensions outside the ball. OpenAI's release did not include a Lean proof of their uniqueness result. Our formalization uses results from Mathlib and Tau Ceti, and it is given as a solution to a Lean comparator challenge whose check permits only the standard axioms of Lean. The Lean proof is not a line-by-line translation of the OpenAI manuscript.
Problem

OpenAI announced uniqueness for the smooth anisotropic Calderón inverse problem but did not release a Lean proof of it. The authors seek a machine-checked proof of a restricted case: smooth metrics on the 3D unit ball that are Euclidean outside the ball, with full boundary measurements.

Approach

Boundary measurements are encoded through the minimized Dirichlet energy (the DN-map quadratic form), so no separately defined DN map is needed. The theorem is stated as a comparator challenge (OAI.AnisotropicCalderon.main), and an AI-assisted autoformalization (OpenAI Codex, Claude Code) produced a solution that uses Mathlib and 96 Tau Ceti modules. The proof is not a line-by-line translation of the manuscript, and its prerequisites are formalized as well.

Results

The Lean proof shows that equal Dirichlet energies imply the metrics agree up to a smooth diffeomorphism fixing the exterior. The comparator replays the proof in Lean's kernel and confirms that only the standard axioms (propext, Classical.choice, Quot.sound) are used. The repository is public.