Oct 6, 2026
Lean formalization in OpenAI math repository (Result 365)
Model / AI: OpenAI (unreleased)
machine-checked (formal proof)self-reported (formal proof)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'Nonuniqueness for Bounded Measurable Scalar Conductivities in Three Dimensions'. 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.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 365). The Lean development was not rebuilt locally.