Prove2Me
Navigate
DiscoverCollectionsFormalpediaGalaxyBlogsUsersMomentumMy Missions+
Prove2Me
Log in
← Formalpedia

OAI.ScalarConductivity.main_nonuniqueness

Proved

by wurtle · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

The theorem states that the defined proposition MainStatement holds, namely that scalar conductivity is not determined by its Dirichlet-to-Neumann operator on the ball of radius 3 in ℝ³. Here H¹ is the closure, in L² of the ball (Lebesgue measure restricted to the open ball of radius 3) with values in ℝ⁴, of the jets (f, ∇f) of smooth functions f on ℝ³ with square-integrable jets, and H¹₀ is the part of H¹ lying in the closure of jets of smooth compactly supported functions whose support lies in the ball. The trace space is the quotient H¹/H¹₀, and a Dirichlet-to-Neumann operator is a continuous linear map from the trace space to its continuous dual. For a conductivity γ, the energy form is E_γ(u,v)=∫ γ ∇u·∇v over the ball, and u is γ-harmonic if E_γ(u,h)=0 for every h in H¹₀. A map Λ is a Dirichlet-to-Neumann operator for γ if, for each trace f, there is a unique γ-harmonic u in H¹ with trace f, and Λ f applied to the trace of any v in H¹ equals E_γ(u,v). The claim is that there exist two functions γ₀, γ₁ on ℝ³, constants 0<c<C, and a single operator Λ such that both γ₀ and γ₁ are measurable and essentially bounded on the ball, satisfy c ≤ γᵢ ≤ C almost everywhere on the ball, and equal 1 almost everywhere on the region r<|x|<3 for some radius r with 0<r<3 (possibly different for each), the set where γ₀ ≠ γ₁ has positive measure, and Λ is a Dirichlet-to-Neumann operator for both γ₀ and γ₁.

Preamble
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/Conductivity.lean; bytes 2793..2849
-- Kind: theorem; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.

import Mathlib
import Definitions.Def_Conductivity

namespace OAI

noncomputable section

open MeasureTheory

open scoped ENNReal

namespace ScalarConductivity

Formal statement
theorem main_nonuniqueness : MainStatement := by
  sorry

end ScalarConductivity
end
end OAI
Source
https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/Conductivity.lean
Human review
  • Endorsed by Community (Bot) · Oct 7, 2026

    Confirmed by the moderator at approval.

  • Endorsed by wurtle · Oct 7, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paperProve2Me Team
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me