Lean statement

Pressure and ground-state limits for invariant Ising models

Lean is a language for mathematical statements and proofs that a computer can verify. This page shows one statement file from OpenAI’s release, possible paper matches and independent reports. The code-like names below identify the definitions or theorems selected by the proof-verification settings.

Theorems selected for verification: OAI.InvariantIsing.limiting_pressure_of_extreme_limits_unconditional OAI.InvariantIsing.limiting_wasserstein_field_pressure_of_extreme_limits_unconditional OAI.InvariantIsing.positive_temperature_pressure_unconditional OAI.InvariantIsing.ground_state_limit_unconditional OAI.InvariantIsing.random_pressure_tendsto_in_measure_unconditional OAI.InvariantIsing.random_pressure_limit_unconditional OAI.InvariantIsing.random_pressure_tendsto_ae_unconditional OAI.InvariantIsing.random_field_pressure_tendsto_ae_unconditional OAI.InvariantIsing.gaussianPattern_pressure_limit_unconditional OAI.InvariantIsing.gaussianPattern_ground_limit_unconditional OAI.InvariantIsing.gaussianPattern_norm_limits_unconditional

Lean statement file: InvariantIsing.leanShow on the mapOpenAI’s Lean catalogue does not list this as a main result; the release’s Lean notes for family 234 link it.

See the candidate theorem Who ran the proof-verification program Report a comparison with the paper (GitHub issue)

The Lean statement

The lines of the Lean statement that state the theorem, then the definitions in the file that it uses.

theorem limiting_pressure_of_extreme_limits_unconditional :  ∀ {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]    (U : (N : ℕ) → Ω → Orthogonal N) (_hU : ∀ N, Measurable (U N))    (_hHaar : ∀ N, (P.map (U N)).IsMulRightInvariant)    (eig : (N : ℕ) → Fin N → ℝ) (ν : ProbabilityMeasure ℝ) (a b : ℝ)    (_hcompact : IsCompact (ν : Measure ℝ).support)    (_hbound : (ν : Measure ℝ).support ⊆ Icc a b)    (_ha : a∈(ν : Measure ℝ).support) (_hb : b∈(ν : Measure ℝ).support)    (_hmin : Tendsto (fun k => spectralMinimum (eig (k+1))) atTop (𝓝 a))    (_hmax : Tendsto (fun k => spectralMaximum (eig (k+1))) atTop (𝓝 b))    (_hweak : Tendsto (fun k => empiricalSpectralLaw (Nat.succ_pos k) (eig (k+1)))      atTop (𝓝 ν)),    Tendsto (fun N => ∫ ω, rotatedPressure (eig N) (matrixRotation (U N ω)⁻¹) (fun _ => 0) ∂P)      atTop (𝓝 (variationalFunctional (measureR (ν : Measure ℝ) b)).toReal) ∧    ∀ᵐ ω ∂P, Tendsto (fun N => rotatedPressure (eig N) (matrixRotation (U N ω)⁻¹) (fun _ => 0))      atTop (𝓝 (variationalFunctional (measureR (ν : Measure ℝ) b)).toReal) := by  sorry⋮theorem limiting_wasserstein_field_pressure_of_extreme_limits_unconditional :  ∀ {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]    (U : (N : ℕ) → Ω → Orthogonal N) (_hU : ∀ N, Measurable (U N))    (_hHaar : ∀ N, (P.map (U N)).IsMulRightInvariant)    (eig : (N : ℕ) → Fin N → ℝ) (ν : ProbabilityMeasure ℝ) (a b : ℝ)    (_hcompact : IsCompact (ν : Measure ℝ).support)    (_hbound : (ν : Measure ℝ).support ⊆ Icc a b)    (_ha : a∈(ν : Measure ℝ).support) (_hb : b∈(ν : Measure ℝ).support)    (_hmin : Tendsto (fun k => spectralMinimum (eig (k+1))) atTop (𝓝 a))    (_hmax : Tendsto (fun k => spectralMaximum (eig (k+1))) atTop (𝓝 b))    (_hweak : Tendsto (fun k => empiricalSpectralLaw (Nat.succ_pos k) (eig (k+1)))      atTop (𝓝 ν))    (field : (N : ℕ) → Fin N → ℝ) (ξ : ProbabilityMeasure ℝ)    (_hξ : Integrable (fun x : ℝ => x) (ξ : Measure ℝ))    (_hw : Tendsto (fun k => fieldWassersteinOne (empiricalSpectralLaw (Nat.succ_pos k) (field (k+1))) ξ)      atTop (𝓝 0)),    Tendsto (fun N => ∫ ω, rotatedPressure (eig N) (matrixRotation (U N ω)⁻¹) (field N) ∂P)      atTop (𝓝 (magneticFieldFunctional (ν : Measure ℝ) b ξ)) ∧    ∀ᵐ ω ∂P, Tendsto (fun N => rotatedPressure (eig N) (matrixRotation (U N ω)⁻¹) (field N))      atTop (𝓝 (magneticFieldFunctional (ν : Measure ℝ) b ξ)) := by  sorry⋮theorem positive_temperature_pressure_unconditional :  ∀ {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]    (U : (N : ℕ) → Ω → Orthogonal N) (_hU : ∀ N, Measurable (U N))    (_hHaar : ∀ N, (P.map (U N)).IsMulRightInvariant)    (eig : (N : ℕ) → Fin N → ℝ) (ν : ProbabilityMeasure ℝ) (a b : ℝ)    (_hbound : (ν : Measure ℝ).support ⊆ Icc a b)    (_ha : a∈(ν : Measure ℝ).support) (_hb : b∈(ν : Measure ℝ).support)    (_hno : ∀ ε : ℝ, 0 < ε → ∀ᶠ N in atTop, ∀ i, a-ε ≤ eig N i ∧ eig N i ≤ b+ε)    (β : ℝ) (_hβ : 0 < β)    (_hweak : Tendsto (fun k => empiricalSpectralLaw (Nat.succ_pos k) (eig (k+1)))      atTop (𝓝 ν)),    Tendsto (fun N => ∫ ω, rotatedPressure (fun i => β*eig N i) (matrixRotation (U N ω)⁻¹) (fun _ => 0) ∂P)      atTop (𝓝 (variationalFunctional (measureR (scaledSpectralLaw ν β : Measure ℝ) (β*b))).toReal) ∧    ∀ᵐ ω ∂P, Tendsto (fun N => rotatedPressure (fun i => β*eig N i) (matrixRotation (U N ω)⁻¹) (fun _ => 0))      atTop (𝓝 (variationalFunctional (measureR (scaledSpectralLaw ν β : Measure ℝ) (β*b))).toReal) := by  sorry⋮theorem ground_state_limit_unconditional :  ∀ {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]    (U : (N : ℕ) → Ω → Orthogonal N) (_hU : ∀ N, Measurable (U N))    (_hHaar : ∀ N, (P.map (U N)).IsMulRightInvariant)    (eig : (N : ℕ) → Fin N → ℝ) (ν : ProbabilityMeasure ℝ) (a b : ℝ)    (_hbound : (ν : Measure ℝ).support ⊆ Icc a b)    (_ha : a∈(ν : Measure ℝ).support) (_hb : b∈(ν : Measure ℝ).support)    (_hno : ∀ ε : ℝ, 0 < ε → ∀ᶠ N in atTop, ∀ i, a-ε ≤ eig N i ∧ eig N i ≤ b+ε)    (_hweak : Tendsto (fun k => empiricalSpectralLaw (Nat.succ_pos k) (eig (k+1)))      atTop (𝓝 ν)),    ∃ M : ℝ,      Tendsto (fun N => ∫ ω, groundStateEnergy (eig N) (matrixRotation (U N ω)⁻¹) ∂P)        atTop (𝓝 M) ∧      (∀ᵐ ω ∂P, Tendsto (fun N => groundStateEnergy (eig N) (matrixRotation (U N ω)⁻¹))        atTop (𝓝 M)) ∧      Tendsto (thermalVariationalValue ν b) atTop (𝓝 M) := by  sorry⋮theorem random_pressure_tendsto_in_measure_unconditional    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]    (eig : (N : ℕ) → Ω → Fin N → ℝ) (Y : ℕ → Ω → ℝ)    (heig : ∀ N, Measurable (eig N)) (hY : ∀ N, Measurable (Y N))    (H : (N : ℕ) → Measure (Orthogonal N)) [∀ N, IsProbabilityMeasure (H N)]    [∀ N, (H N).IsMulRightInvariant]    (hlaw : ∀ N, ConditionalFieldOrbitLaw P (fun ω => (eig N ω,fun _ => 0)) (Y N) (H N))    (ν : ProbabilityMeasure ℝ) (a b : ℝ)    (hcompact : IsCompact (ν : Measure ℝ).support)    (hbound : (ν : Measure ℝ).support ⊆ Icc a b)    (ha : a∈(ν : Measure ℝ).support) (hb : b∈(ν : Measure ℝ).support)    (hweak : TendstoInMeasure P (fun k ω => LevyProkhorov.ofMeasure      (empiricalSpectralLaw (Nat.succ_pos k) (eig (k+1) ω))) atTop      (fun _ => LevyProkhorov.ofMeasure ν))    (hexcess : TendstoInMeasure P (fun k ω => spectralExcess (eig (k+1) ω) a b)      atTop (fun _ => 0)) :    TendstoInMeasure P (fun k => Y (k+1)) atTop      (fun _ => (variationalFunctional (measureR (ν : Measure ℝ) b)).toReal) := by  sorry⋮theorem random_pressure_limit_unconditional :  ∀ {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]    (eig : (N : ℕ) → Ω → Fin N → ℝ) (Y : ℕ → Ω → ℝ)    (_heig : ∀ N, Measurable (eig N)) (_hY : ∀ N, Measurable (Y N))    (H : (N : ℕ) → Measure (Orthogonal N)) [∀ N, IsProbabilityMeasure (H N)]    [∀ N, (H N).IsMulRightInvariant]    (_hlaw : ∀ N, ConditionalFieldOrbitLaw P (fun ω => (eig N ω,fun _ => 0)) (Y N) (H N))    (ν : ProbabilityMeasure ℝ) (a b : ℝ)    (_hcompact : IsCompact (ν : Measure ℝ).support)    (_hbound : (ν : Measure ℝ).support ⊆ Icc a b)    (_ha : a∈(ν : Measure ℝ).support) (_hb : b∈(ν : Measure ℝ).support)    (_hweak : TendstoInMeasure P (fun k ω => LevyProkhorov.ofMeasure      (empiricalSpectralLaw (Nat.succ_pos k) (eig (k+1) ω))) atTop      (fun _ => LevyProkhorov.ofMeasure ν))    (_hexcess : TendstoInMeasure P (fun k ω => spectralExcess (eig (k+1) ω) a b)      atTop (fun _ => 0))    (_hUI : UniformIntegrable (fun k => Y (k+1)) 1 P),    TendstoInMeasure P (fun k => Y (k+1)) atTop      (fun _ => (variationalFunctional (measureR (ν : Measure ℝ) b)).toReal) ∧    Tendsto (fun k => eLpNorm (fun ω => Y (k+1) ω-      (variationalFunctional (measureR (ν : Measure ℝ) b)).toReal) 1 P) atTop (𝓝 0) ∧    Tendsto (fun k => ∫ ω, Y (k+1) ω ∂P) atTop      (𝓝 (variationalFunctional (measureR (ν : Measure ℝ) b)).toReal) := by  sorry⋮theorem random_pressure_tendsto_ae_unconditional :  ∀ {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]    (eig : (N : ℕ) → Ω → Fin N → ℝ) (Y : ℕ → Ω → ℝ)    (_heig : ∀ N, Measurable (eig N)) (_hY : ∀ N, Measurable (Y N))    (H : (N : ℕ) → Measure (Orthogonal N)) [∀ N, IsProbabilityMeasure (H N)]    [∀ N, (H N).IsMulRightInvariant]    (_hlaw : ∀ N, ConditionalFieldOrbitLaw P (fun ω => (eig N ω,fun _ => 0)) (Y N) (H N))    (ν : ProbabilityMeasure ℝ) (a b : ℝ)    (_hcompact : IsCompact (ν : Measure ℝ).support)    (_hbound : (ν : Measure ℝ).support ⊆ Icc a b)    (_ha : a∈(ν : Measure ℝ).support) (_hb : b∈(ν : Measure ℝ).support)    (_hno : ∀ᵐ ω ∂P, ∀ ε : ℝ, 0 < ε → ∀ᶠ N in atTop,      ∀ i, a-ε ≤ eig N ω i ∧ eig N ω i ≤ b+ε)    (_hweak : ∀ᵐ ω ∂P, Tendsto (fun k =>      empiricalSpectralLaw (Nat.succ_pos k) (eig (k+1) ω)) atTop (𝓝 ν)),    ∀ᵐ ω ∂P, Tendsto (fun N => Y N ω) atTop      (𝓝 (variationalFunctional (measureR (ν : Measure ℝ) b)).toReal) := by  sorry⋮theorem random_field_pressure_tendsto_ae_unconditional :  ∀ {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]    (d : (N : ℕ) → Ω → FieldSpectralData N) (Y : ℕ → Ω → ℝ)    (_hd : ∀ N, Measurable (d N)) (_hY : ∀ N, Measurable (Y N))    (H : (N : ℕ) → Measure (Orthogonal N)) [∀ N, IsProbabilityMeasure (H N)]    [∀ N, (H N).IsMulRightInvariant]    (_hlaw : ∀ N, ConditionalFieldOrbitLaw P (d N) (Y N) (H N))    (ν : ProbabilityMeasure ℝ) (a b : ℝ)    (_hcompact : IsCompact (ν : Measure ℝ).support)    (_hbound : (ν : Measure ℝ).support ⊆ Icc a b)    (_ha : a∈(ν : Measure ℝ).support) (_hb : b∈(ν : Measure ℝ).support)    (_hno : ∀ᵐ ω ∂P, ∀ ε : ℝ, 0 < ε → ∀ᶠ N in atTop,      ∀ i, a-ε ≤ (d N ω).1 i ∧ (d N ω).1 i ≤ b+ε)    (_hweak : ∀ᵐ ω ∂P, Tendsto (fun k =>      empiricalSpectralLaw (Nat.succ_pos k) (d (k+1) ω).1) atTop (𝓝 ν))    (ξ : ProbabilityMeasure ℝ) (_hξ : Integrable (fun x : ℝ => x) (ξ : Measure ℝ))    (_hw : ∀ᵐ ω ∂P, Tendsto (fun k => fieldWassersteinOne      (empiricalSpectralLaw (Nat.succ_pos k) (d (k+1) ω).2) ξ) atTop (𝓝 0)),    ∀ᵐ ω ∂P, Tendsto (fun N => Y N ω) atTop      (𝓝 (magneticFieldFunctional (ν : Measure ℝ) b ξ)) := by  sorry⋮theorem gaussianPattern_pressure_limit_unconditional :  ∀ (α : ℝ) (_hα : 0 < α)    {Ω : Type u} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]    (Z : (N : ℕ) → Ω → EuclideanSpace ℝ (Fin N × Fin (gaussianPatternCount α N)))    (_hZ : ∀ N, Measurable (Z N)) (_hlaw : ∀ N, HasLaw (Z N) (stdGaussian _) P)    (c : ℝ),    TendstoInMeasure P (fun k ω => gaussianPatternPressure (N := k+1) (m := gaussianPatternCount α (k+1)) c (Z (k+1) ω)) atTop      (fun _ => gaussianPatternLimit α c) ∧    Tendsto (fun k => eLpNorm (fun ω => gaussianPatternPressure (N := k+1) (m := gaussianPatternCount α (k+1)) c (Z (k+1) ω)-      gaussianPatternLimit α c) 1 P) atTop (𝓝 0) ∧    Tendsto (fun k => ∫ ω, gaussianPatternPressure (N := k+1) (m := gaussianPatternCount α (k+1)) c (Z (k+1) ω) ∂P) atTop      (𝓝 (gaussianPatternLimit α c)) := by  sorry⋮theorem gaussianPattern_ground_limit_unconditional :  ∀ (α : ℝ) (_hα : 0 < α)    {Ω : Type u} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]    (Z : (N : ℕ) → Ω → EuclideanSpace ℝ (Fin N × Fin (gaussianPatternCount α N)))    (_hZ : ∀ N, Measurable (Z N)) (_hlaw : ∀ N, HasLaw (Z N) (stdGaussian _) P)    (ε : ℝ),    ∃ e : ℝ,      TendstoInMeasure P (fun k ω => gaussianPatternGroundEnergy ε (Z (k+1) ω)) atTop (fun _ => e) ∧      Tendsto (fun k => eLpNorm (fun ω => gaussianPatternGroundEnergy ε (Z (k+1) ω)-e) 1 P)        atTop (𝓝 0) ∧      Tendsto (fun k => ∫ ω, gaussianPatternGroundEnergy ε (Z (k+1) ω) ∂P) atTop (𝓝 e) ∧      Tendsto (fun β => gaussianPatternLimit α (ε*β)/β) atTop (𝓝 e) := by  sorry⋮theorem gaussianPattern_norm_limits_unconditional :  ∀ (α : ℝ) (_hα : 0 < α)    {Ω : Type u} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]    (Z : (N : ℕ) → Ω → EuclideanSpace ℝ (Fin N × Fin (gaussianPatternCount α N)))    (_hZ : ∀ N, Measurable (Z N)) (_hlaw : ∀ N, HasLaw (Z N) (stdGaussian _) P),    ∃ eplus eminus : ℝ, 0 ≤ eplus ∧ eminus ≤ 0 ∧      Tendsto (fun β => gaussianPatternLimit α β/β) atTop (𝓝 eplus) ∧      Tendsto (fun β => gaussianPatternLimit α (-β)/β) atTop (𝓝 eminus) ∧      (TendstoInMeasure P (fun k ω => ‖gaussianPatternOperator (Z (k+1) ω)‖/(k+1)) atTop        (fun _ => Real.sqrt (2*eplus)) ∧       Tendsto (fun k => eLpNorm (fun ω => ‖gaussianPatternOperator (Z (k+1) ω)‖/(k+1)-        Real.sqrt (2*eplus)) 1 P) atTop (𝓝 0)) ∧      (TendstoInMeasure P (fun k ω =>        (Finset.univ.inf' Finset.univ_nonempty (fun σ : Spin (k+1) => ‖gaussianPatternSum (Z (k+1) ω) σ‖))/(k+1))        atTop (fun _ => Real.sqrt (-2*eminus)) ∧       Tendsto (fun k => eLpNorm (fun ω =>        (Finset.univ.inf' Finset.univ_nonempty (fun σ : Spin (k+1) => ‖gaussianPatternSum (Z (k+1) ω) σ‖))/(k+1)-          Real.sqrt (-2*eminus)) 1 P) atTop (𝓝 0)) := by  sorry

A Lean statement states the theorem and leaves its proof as sorry on purpose. OpenAI’s proof is in a separate solution module, and a program called Comparator checks that proof against this statement.

Definitions needed to read it

Local definitions the statement names, followed through the definitions they name in turn. The match is by name in the source text, so a name reached only through notation can be missed; the full file is below.

abbreviation OAI.InvariantIsing.Spin line 14
```
abbrev Spin (N : ℕ) := Fin N → Bool
```

definition OAI.InvariantIsing.spinValue line 16

def spinValue (b : Bool) : ℝ := if b then 1 else -1

definition OAI.InvariantIsing.logPartition line 18

def logPartition {X : Type*} [Fintype X] (H : X → ℝ) : ℝ :=  Real.log ((Fintype.card X : ℝ)⁻¹ * ∑ x, Real.exp (H x))

definition OAI.InvariantIsing.fieldEnergy line 21

def fieldEnergy {N : ℕ} (c : Fin N → ℝ) (σ : Spin N) : ℝ :=  ∑ i, c i * spinValue (σ i)

abbreviation OAI.InvariantIsing.Rotation line 24

abbrev Rotation (N : ℕ) :=  EuclideanSpace ℝ (Fin N) ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin N)

abbreviation OAI.InvariantIsing.Orthogonal line 27

abbrev Orthogonal (N : ℕ) := Matrix.orthogonalGroup (Fin N) ℝ

definition OAI.InvariantIsing.spinVector line 29

def spinVector {N : ℕ} (σ : Spin N) : EuclideanSpace ℝ (Fin N) :=  WithLp.toLp 2 (fun i => spinValue (σ i))

definition OAI.InvariantIsing.rotatedEnergy line 32

def rotatedEnergy {N : ℕ} (eig : Fin N → ℝ) (U : Rotation N) (σ : Spin N) : ℝ :=  (1 / 2 : ℝ) * ∑ i, eig i * (U (spinVector σ) i) ^ 2

definition OAI.InvariantIsing.rotatedPressure line 35

def rotatedPressure {N : ℕ} (eig : Fin N → ℝ) (U : Rotation N)    (c : Fin N → ℝ) : ℝ :=  (N : ℝ)⁻¹ * logPartition (fun σ => rotatedEnergy eig U σ + fieldEnergy c σ)run_cmd Lean.modifyEnv fun env => Lean.Meta.auxLemmasExt.setState env {}

definition OAI.InvariantIsing.matrixRotation line 54

def matrixRotation {N : ℕ} (U : Orthogonal N) : Rotation N :=  { ((WithLp.linearEquiv 2 ℝ (Fin N → ℝ)).trans      (Matrix.UnitaryGroup.toLinearEquiv U)).trans      (WithLp.linearEquiv 2 ℝ (Fin N → ℝ)).symm with    norm_map' := fun v => (sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _)).mp      (orthogonal_mulVec_norm_sq U v) }

structure OAI.InvariantIsing.OverlapPath line 61

structure OverlapPath where  val : ℝ → ℝ  monotone : Monotone val  nonneg : ∀ s, 0 ≤ val s  le_one : ∀ s, val s ≤ 1

definition OAI.InvariantIsing.pathMeasure line 69

def pathMeasure : Measure ℝ := volume.restrict (Ioo (0 : ℝ) 1)

definition OAI.InvariantIsing.deficit line 71

def deficit (p : OverlapPath) (r : ℝ) : ℝ :=  1 - r - ∫ s, max (p s - r) 0 ∂pathMeasurerun_cmd Lean.modifyEnv fun env => Lean.Meta.auxLemmasExt.setState env {}

definition OAI.InvariantIsing.gaussianOperator line 76

def gaussianOperator (a v : ℝ) (f : ℝ → ℝ) (z : ℝ) : ℝ :=  if a = 0 then ∫ g, f (z + Real.sqrt v * g) ∂gaussianReal 0 1  else a⁻¹ * Real.log (∫ g, Real.exp (a * f (z + Real.sqrt v * g)) ∂gaussianReal 0 1)

structure OAI.InvariantIsing.FieldStep line 80

structure FieldStep where  depth : ℕ  cut : Fin (depth + 2) → ℝ  ordered_cut : StrictMono cut  first : cut 0 = 0  last : cut (Fin.last (depth + 1)) = 1  height : Fin (depth + 1) → ℝ  nonneg : ∀ i, 0 ≤ height i  ordered_height : Monotone height

definition OAI.InvariantIsing.fieldFunction line 90

def fieldFunction (h : FieldStep) (s : ℝ) : ℝ :=  ∑ i : Fin (h.depth + 1),    if h.cut i.castSucc < s ∧ s < h.cut i.succ then h.height i else 0

definition OAI.InvariantIsing.fieldIncrement line 94

def fieldIncrement (h : FieldStep) (i : Fin (h.depth + 1)) : ℝ × ℝ :=  (h.cut i.castSucc, h.height i -    if hi : i.val = 0 then 0 else h.height ⟨i.val - 1, by omega⟩)

definition OAI.InvariantIsing.fieldValue line 98

def fieldValue (h : FieldStep) (b : ℝ) : ℝ :=  ((List.ofFn (fieldIncrement h)).foldr    (fun av f => gaussianOperator av.1 av.2 f) (fun z => Real.log (Real.cosh z))) b -    h.height (Fin.last h.depth) / 2

definition OAI.InvariantIsing.fieldPairing line 103

def fieldPairing (p : OverlapPath) (h : FieldStep) : ℝ :=  ∫ s, p s * fieldFunction h s ∂pathMeasure

definition OAI.InvariantIsing.entropyFunctional line 106

def entropyFunctional (p : OverlapPath) : EReal :=  ⨆ h : FieldStep, ((fieldValue h 0 + fieldPairing p h / 2 : ℝ) : EReal)

definition OAI.InvariantIsing.spectralFunctional line 109

def spectralFunctional (R : ℝ → ℝ) (p : OverlapPath) : ℝ :=  (1 / 2 : ℝ) * ∫ r, R (deficit p r) ∂pathMeasure

definition OAI.InvariantIsing.variationalFunctional line 112

def variationalFunctional (R : ℝ → ℝ) : EReal :=  ⨅ p : OverlapPath, entropyFunctional p + (spectralFunctional R p : EReal)

definition OAI.InvariantIsing.measureResolvent line 115

def measureResolvent (μ : Measure ℝ) (b : ℝ) : ℝ := ∫ y, 1 / (b - y) ∂μ

definition OAI.InvariantIsing.measureInverse line 117

def measureInverse (μ : Measure ℝ) (e x : ℝ) : ℝ :=  if h : ∃ b, e < b ∧ measureResolvent μ b = x then h.choose else e

40 more definitions are reached the same way; the full file lists them.

Possible paper match, with no recorded review

No paper statement clearly matched the Lean wording. Statement Map, the program that collects Atlas’s source records, selected this possible match using words in OpenAI’s catalogue and Lean note. No review of whether the statements mean the same thing is recorded.

Shared with the catalogue’s wording or OpenAI’s note, none of them matched in the Lean text: almost, compactly, converge, eigenvalues, empirical, haar, limit, limiting and five more.

Theorem 1.1 of All-temperature pressure for orthogonally invariant Ising spin glasses

Theorem (Limiting pressure)

Let \Lambda_N be deterministic real diagonal matrices whose empirical spectral measures converge weakly to a compactly supported probability law \mu. Assume that their smallest and largest eigenvalues converge to the respective edges of \supp\mu. Let U_N be Haar distributed on O(N), and define P_N using the uniform spin probability in Equation (eq:pressure). With S and G_1 as in Equations (eq:S)–(eq:G),

\lim_{N\to\infty}\E P_N =\lim_{N\to\infty}P_N =\mathcal F(\mu) :=\inf_{p\in\cP}\{S(p)+G_1(p)\},

where the second limit holds almost surely. No independence of the matrices U_N across dimensions is required.

Section 1, Introduction Read it in the paper TeX source, line 186

Show the TeX

Let $\Lambda_N$ be deterministic real diagonal matrices whose empirical
spectral measures converge weakly to a compactly supported probability
law $\mu$. Assume that their smallest and largest eigenvalues converge
to the respective edges of $\supp\mu$. Let $U_N$ be Haar distributed
on $O(N)$, and define $P_N$ using the uniform spin probability in
Equation~\eqref{eq:pressure}. With $S$ and $G_1$ as in
Equations~\eqref{eq:S}--\eqref{eq:G},
\begin{equation}
 \lim_{N\to\infty}\E P_N
 =\lim_{N\to\infty}P_N
 =\mathcal F(\mu)
 :=\inf_{p\in\cP}\{S(p)+G_1(p)\},
 
\end{equation}
where the second limit holds almost surely. No independence of the
matrices $U_N$ across dimensions is required.

Other possible paper matches, closest wording first

Proposition 7.4 of All-temperature pressure for orthogonally invariant Ising spin glasses. Words of the Lean statement, its names split into words, that also appear in the theorem: orbit, edge, last, integrable, excesses, orthogonal and 14 more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: convergence, whose, compactly, converge, eigenvalues, almost and one more.
Corollary 7.6 of All-temperature pressure for orthogonally invariant Ising spin glasses. Words of the Lean statement, its names split into words, that also appear in the theorem: patterns, sqrt, operator, gaussian, temperature, norms and three more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: expectation.
Proposition 4.2 of All-temperature pressure for orthogonally invariant Ising spin glasses. Words of the Lean statement, its names split into words, that also appear in the theorem: choose, compact, range, partition, properties, minimum and twelve more.
Proposition 8.3 of All-temperature pressure for orthogonally invariant Ising spin glasses. Words of the Lean statement, its names split into words, that also appear in the theorem: constrained, functional, bias, data, strict, weights and five more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: distance.
Theorem 8.1 of All-temperature pressure for orthogonally invariant Ising spin glasses. Words of the Lean statement, its names split into words, that also appear in the theorem: first, magnetic, rational, field, positive, empirical and seven more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: convergence, assume, compactly, converge, expectation, almost and one more.
Corollary 7.5 of All-temperature pressure for orthogonally invariant Ising spin glasses. Words of the Lean statement, its names split into words, that also appear in the theorem: maximum, energy, image, max, spin, spectral and two more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: expectation, surely and almost.

How Atlas selects possible matches: it compares words in the Lean statement with every statement in the family. It also splits Lean names into words. The release’s label and note receive less weight; a main theorem wins a close match. If the Lean wording yields no clear match, Atlas uses the catalogue description. This selects passages to compare; it does not establish that they mean the same thing.

Reported Comparator runs

two independent groups report that Comparator accepted runs for this Lean statement file: Carlos Toledo’s cert-machine; Neal McBurnett’s openai-math-lean-tooling. Each group reports its own Comparator run for this statement file. Atlas has not repeated the runs.

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

Carlos Toledo’s cert-machine

How they ran it, in their words

Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule; every family’s challenge statements read against OpenAI’s headline, clause by clause. Decider: Comparator (leanprover/comparator d03acab1 = tag v4.34.0, built with the release’s toolchain v4.34.1), lean4export 076e8e57, landrun 811cfff5, nanoda_lib 3a240721 — on GitHub’s Linux runners (.github/workflows/openai-math-kernel.yml), one j…

Accepted Their term: “CERTIFIED”.
Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.
Reported 10 October 2026, at the release version shown here. Original verification report

Neal McBurnett’s openai-math-lean-tooling

How they ran it, in their words

Each challenge’s solution is built and checked by Comparator at the pinned release, on Lean leanprover/lean4:v4.34.1, recording the verdict, the check time and the peak memory; the run was still in progress at this snapshot (192 accepted, 224 pending).

Accepted Their term: “accepted”.
Re-run through Comparator with Lean’s kernel: accepted (the check took 580 s; peak memory 7.3 GiB).
Reported 10 October 2026, at the release version shown here. Original verification report

What an accepted Comparator run would establish

If Comparator is run under this configuration and accepts, the solution proves the configured theorem using only the allowed axioms, and the Lean kernel accepts every step.

This configuration lists no definition holes, so every definition the statement uses is compared as it is written in this file.

Allowed axioms: propext, Quot.sound, Classical.choice

Acceptance leaves open whether the Lean statement means the same thing as the paper’s theorem, whether the paper’s other claims are correct, and whether the result is new. Those questions require comparing the definitions and statements, reviewing the paper’s arguments, and reading the earlier literature.

Do family 234’s Lean statements express the advertised result?

These assessments compare all the family’s Lean statements with the whole result OpenAI describes in its catalogue. They do not assess this statement alone. Each group uses its own published rules.

MathVet and cert-machine agree on how much of the advertised result the Lean statements express.

MathVet
Finds the whole advertised result stated or implied Their term: “full”.
The challenge statements imply the headline claim after unpacking definitions or one routine step. Their record
Their note: limiting_pressure_of_extreme_limits_unconditional: for Haar-distributed orthogonal U N ((P.map (U N)).IsMulRightInvariant), deterministic spectra eig N with empiricalSpectralLaw → ν (compact support, extreme eigenvalues → a, b), ∫ rotatedPressure .. ∂P → (variationalFunctional (measureR ν b)).toReal and the same almost surely; positive_temperature_pressure_unconditional (all β > 0 via scaledSpectralLaw), ground_state_limit_unconditional (Tendsto (thermalVariationalValue ν b) atTop (𝓝 M) with M the ground-state limit), plus magnetic-field, random-spectrum and Gaussian-pattern variants. All summary claims are stated.
Definitions the group asks readers to compare with the paper: Custom 'free energy': logPartition H := log ((card X)⁻¹ * Σ_x exp(H x)) (normalized by 2^{-N}, i.e. pressure minus log 2), rotatedPressure, the Parisi-type variationalFunctional R := ⨅ p : OverlapPath, entropyFunctional p + spectralFunctional R p (EReal) and measureR μ e x (R-transform via a h.choose inverse of the resolvent on (e, ∞)); hand-written variational formulas, with the final value taken via .toReal of an EReal (junk if infinite).
Carlos Toledo’s cert-machine
Finds the whole advertised result stated or implied Their term: “MATCHES”.
The challenge statements state the headline as OpenAI wrote it. Their record

Read the complete assessments on the family page.

OpenAI’s own note on what this Lean statement covers

“The formalization gives variational limits for orthogonally invariant Ising spin glasses whose eigenvectors have Haar law and whose empirical eigenvalue distributions converge to a compactly supported law with the stated control of extreme eigenvalues. The pressure converges both in expectation and almost surely to an explicit functional of the limiting spectral law. A version with external fields assumes convergence of their empirical laws in Wasserstein distance and gives the corresponding magnetic-field functional.”
Quoted from OpenAI’s Lean note for this family

An AI agent drafted an interpretation of that note, classifying this statement as “states a paper’s theorem as the paper does”. No human review of the draft is recorded.

Supporting material

The complete Lean statement file

495 lines, copied from release version fd4aeeb. A name defined in this file links to its line; pointing at the name shows its definition.

Declared in this fileOpenAI’s library at fd4aeebOther linked names open the current documentation for Mathlib, Lean’s mathematical library.

Links in the file: 196 to its own declarations, 489 to Mathlib’s documentation. 79 declared names also link to the same declaration in OpenAI’s library. 34 identifiers stay plain because they resolve to no single declaration: variables Lean binds automatically, notation, or names the scan of the pinned sources did not find. OpenAI uses Mathlib version d13f23b. The linked documentation describes the current version, so names that have since changed may be missing there.

import Mathlibnamespace OAI/-! All-temperature invariant Ising pressure and its magnetic, random-spectral,ground-state, and Gaussian-pattern extensions. -/noncomputable sectionopen MeasureTheory ProbabilityTheory Filter Setopen scoped BigOperators Topology Matrix Classical ENNRealuniverse unamespace InvariantIsingabbrev Spin (N : ℕ) := Fin N → Booldef spinValue (b : Bool) : ℝ := if b then 1 else -1def logPartition {X : Type*} [Fintype X] (H : X → ℝ) : ℝ :=  Real.log ((Fintype.card X : ℝ)⁻¹ * ∑ x, Real.exp (H x))def fieldEnergy {N : ℕ} (c : Fin N → ℝ) (σ : Spin N) : ℝ :=  ∑ i, c i * spinValue (σ i)abbrev Rotation (N : ℕ) :=  EuclideanSpace ℝ (Fin N) ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin N)abbrev Orthogonal (N : ℕ) := Matrix.orthogonalGroup (Fin N) ℝdef spinVector {N : ℕ} (σ : Spin N) : EuclideanSpace ℝ (Fin N) :=  WithLp.toLp 2 (fun i => spinValue (σ i))def rotatedEnergy {N : ℕ} (eig : Fin N → ℝ) (U : Rotation N) (σ : Spin N) : ℝ :=  (1 / 2 : ℝ) * ∑ i, eig i * (U (spinVector σ) i) ^ 2def rotatedPressure {N : ℕ} (eig : Fin N → ℝ) (U : Rotation N)    (c : Fin N → ℝ) : ℝ :=  (N : ℝ)⁻¹ * logPartition (fun σ => rotatedEnergy eig U σ + fieldEnergy c σ)run_cmd Lean.modifyEnv fun env => Lean.Meta.auxLemmasExt.setState env {}lemma orthogonal_mulVec_norm_sq {N : ℕ} (U : Orthogonal N)    (v : EuclideanSpace ℝ (Fin N)) :    ‖WithLp.toLp 2 ((U : Matrix (Fin N) (Fin N) ℝ) *ᵥ v.ofLp)‖ ^ 2 = ‖v‖ ^ 2 := by  have hU : (U : Matrix (Fin N) (Fin N) ℝ)ᵀ *      (U : Matrix (Fin N) (Fin N) ℝ) = 1 :=    (Matrix.mem_orthogonalGroup_iff' (Fin N) ℝ).mp U.property  rw [EuclideanSpace.real_norm_sq_eq, EuclideanSpace.real_norm_sq_eq]  simp only [pow_two]  change ((U : Matrix (Fin N) (Fin N) ℝ) *ᵥ v.ofLp) ⬝ᵥ      ((U : Matrix (Fin N) (Fin N) ℝ) *ᵥ v.ofLp) = v.ofLp ⬝ᵥ v.ofLp  rw [← Matrix.dotProduct_transpose_mulVec, Matrix.mulVec_mulVec, hU,    Matrix.one_mulVec]def matrixRotation {N : ℕ} (U : Orthogonal N) : Rotation N :=  { ((WithLp.linearEquiv 2 ℝ (Fin N → ℝ)).trans      (Matrix.UnitaryGroup.toLinearEquiv U)).trans      (WithLp.linearEquiv 2 ℝ (Fin N → ℝ)).symm with    norm_map' := fun v => (sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _)).mp      (orthogonal_mulVec_norm_sq U v) }structure OverlapPath where  val : ℝ → ℝ  monotone : Monotone val  nonneg : ∀ s, 0 ≤ val s  le_one : ∀ s, val s ≤ 1instance : CoeFun OverlapPath (fun _ => ℝ → ℝ) := ⟨OverlapPath.val⟩def pathMeasure : Measure ℝ := volume.restrict (Ioo (0 : ℝ) 1)def deficit (p : OverlapPath) (r : ℝ) : ℝ :=  1 - r - ∫ s, max (p s - r) 0 ∂pathMeasurerun_cmd Lean.modifyEnv fun env => Lean.Meta.auxLemmasExt.setState env {}def gaussianOperator (a v : ℝ) (f : ℝ → ℝ) (z : ℝ) : ℝ :=  if a = 0 then ∫ g, f (z + Real.sqrt v * g) ∂gaussianReal 0 1  else a⁻¹ * Real.log (∫ g, Real.exp (a * f (z + Real.sqrt v * g)) ∂gaussianReal 0 1)structure FieldStep where  depth : ℕ  cut : Fin (depth + 2) → ℝ  ordered_cut : StrictMono cut  first : cut 0 = 0  last : cut (Fin.last (depth + 1)) = 1  height : Fin (depth + 1) → ℝ  nonneg : ∀ i, 0 ≤ height i  ordered_height : Monotone heightdef fieldFunction (h : FieldStep) (s : ℝ) : ℝ :=  ∑ i : Fin (h.depth + 1),    if h.cut i.castSucc < s ∧ s < h.cut i.succ then h.height i else 0def fieldIncrement (h : FieldStep) (i : Fin (h.depth + 1)) : ℝ × ℝ :=  (h.cut i.castSucc, h.height i -    if hi : i.val = 0 then 0 else h.height ⟨i.val - 1, by omega⟩)def fieldValue (h : FieldStep) (b : ℝ) : ℝ :=  ((List.ofFn (fieldIncrement h)).foldr    (fun av f => gaussianOperator av.1 av.2 f) (fun z => Real.log (Real.cosh z))) b -    h.height (Fin.last h.depth) / 2def fieldPairing (p : OverlapPath) (h : FieldStep) : ℝ :=  ∫ s, p s * fieldFunction h s ∂pathMeasuredef entropyFunctional (p : OverlapPath) : EReal :=  ⨆ h : FieldStep, ((fieldValue h 0 + fieldPairing p h / 2 : ℝ) : EReal)def spectralFunctional (R : ℝ → ℝ) (p : OverlapPath) : ℝ :=  (1 / 2 : ℝ) * ∫ r, R (deficit p r) ∂pathMeasuredef variationalFunctional (R : ℝ → ℝ) : EReal :=  ⨅ p : OverlapPath, entropyFunctional p + (spectralFunctional R p : EReal)def measureResolvent (μ : Measure ℝ) (b : ℝ) : ℝ := ∫ y, 1 / (b - y) ∂μdef measureInverse (μ : Measure ℝ) (e x : ℝ) : ℝ :=  if h : ∃ b, e < b ∧ measureResolvent μ b = x then h.choose else edef measureR (μ : Measure ℝ) (e x : ℝ) : ℝ :=  if 0 < x then measureInverse μ e x - 1 / x else ∫ y, y ∂μdef finiteSpectralMeasure {ι : Type*} (ρ eig : ι → ℝ) : Measure ℝ :=  Measure.sum fun a => ENNReal.ofReal (ρ a) • Measure.dirac (eig a)theorem finiteSpectralMeasure_probability {ι : Type*} [Fintype ι] (ρ eig : ι → ℝ)    (hρ : ∀ a, 0 ≤ ρ a) (hsum : ∑ a, ρ a = 1) :    IsProbabilityMeasure (finiteSpectralMeasure ρ eig) := by  apply HasSum.isProbabilityMeasure_sum_dirac hρ  simpa only [hsum] using hasSum_fintype ρrun_cmd Lean.modifyEnv fun env => Lean.Meta.auxLemmasExt.setState env {}lemma empiricalSpectralWeight_sum {N : ℕ} (hN : 0 < N) :    ∑ _i : Fin N, (1 : ℝ)/N=1 := by  simp only [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]  field_simpdef empiricalSpectralLaw {N : ℕ} (hN : 0 < N) (eig : Fin N → ℝ) : ProbabilityMeasure ℝ :=  ⟨finiteSpectralMeasure (fun _ => (1 : ℝ)/N) eig,    finiteSpectralMeasure_probability _ _ (fun _ => by positivity) (empiricalSpectralWeight_sum hN)⟩def spectralMinimum {n : ℕ} (eig : Fin (n+1) → ℝ) : ℝ :=  (Finset.univ.image eig).min' (Finset.image_nonempty.mpr Finset.univ_nonempty)def spectralMaximum {n : ℕ} (eig : Fin (n+1) → ℝ) : ℝ :=  (Finset.univ.image eig).max' (Finset.image_nonempty.mpr Finset.univ_nonempty)def magneticBiasObjective (h : FieldStep) (s b : ℝ) : ℝ := fieldValue h b - b * sdef constrainedFieldValue (h : FieldStep) (s : ℝ) : ℝ :=  sInf (range (magneticBiasObjective h s))def magneticGroupValue {A : Type*} [Fintype A] (γ m : A → ℝ) (h : FieldStep) : ℝ :=  ∑ a, γ a * constrainedFieldValue h (m a)run_cmd Lean.modifyEnv fun env => Lean.Meta.auxLemmasExt.setState env {}def magneticEntropyFunctional {A : Type*} [Fintype A] (γ m : A → ℝ)    (p : OverlapPath) : EReal :=  ⨆ h : FieldStep, ((magneticGroupValue γ m h + fieldPairing p h / 2 : ℝ) : EReal)def magneticVariationalFunctional {A : Type*} [Fintype A] (R : ℝ → ℝ) (γ m : A → ℝ) : EReal :=  ⨅ p : OverlapPath, magneticEntropyFunctional γ m p + (spectralFunctional R p : EReal)def RationalMagnetization (A : Type*) := {m : A → ℚ // ∀ a, |(m a : ℝ)| < 1}def finiteMagneticFunctional {A : Type*} [Fintype A] (R : ℝ → ℝ) (γ c : A → ℝ) : EReal :=  ⨆ m : RationalMagnetization A,    ((∑ a, γ a * c a * (m.val a : ℝ) : ℝ) : EReal) +      magneticVariationalFunctional R γ (fun a => (m.val a : ℝ))def finiteIndexWeight {Ω A : Type*} [MeasurableSpace Ω]    (P : Measure Ω) (g : Ω → A) (a : A) : ℝ := P.real (g ⁻¹' {a})def simpleFieldIndex {Ω : Type*} [MeasurableSpace Ω] (s : SimpleFunc Ω ℝ) (x : Ω) : s.range :=  ⟨s x,s.mem_range_self x⟩def simpleFieldWeight {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) (s : SimpleFunc Ω ℝ) :=  finiteIndexWeight P (simpleFieldIndex s)abbrev SimpleFieldPositive {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) (s : SimpleFunc Ω ℝ) :=  {i : s.range // 0 < simpleFieldWeight P s i}def simpleFieldValue {Ω : Type*} [MeasurableSpace Ω]    (P : Measure Ω) [IsProbabilityMeasure P] (s : SimpleFunc Ω ℝ) (R : ℝ → ℝ) : ℝ :=  (finiteMagneticFunctional R (fun i : SimpleFieldPositive P s => simpleFieldWeight P s i)    (fun i => i.val.val)).toRealdef fieldSimpleApproximation (n : ℕ) : SimpleFunc ℝ ℝ :=  SimpleFunc.approxOn id measurable_id (range (id : ℝ → ℝ) ∪ {0}) 0 (by simp) ndef magneticFieldFunctional (spectral : Measure ℝ) (edge : ℝ) (field : ProbabilityMeasure ℝ) : ℝ :=  limUnder atTop (fun n => simpleFieldValue (field : Measure ℝ) (fieldSimpleApproximation n)    (measureR spectral edge))structure FieldLawCoupling (μ ν : ProbabilityMeasure ℝ) where  law : ProbabilityMeasure (ℝ × ℝ)  fst : (law : Measure (ℝ × ℝ)).map Prod.fst = (μ : Measure ℝ)  snd : (law : Measure (ℝ × ℝ)).map Prod.snd = (ν : Measure ℝ)def FieldLawCoupling.cost {μ ν : ProbabilityMeasure ℝ} (p : FieldLawCoupling μ ν) : ℝ≥0∞ :=  ∫⁻ xy, ENNReal.ofReal |xy.1-xy.2| ∂(p.law : Measure (ℝ × ℝ))def fieldWassersteinOne (μ ν : ProbabilityMeasure ℝ) : ℝ≥0∞ :=  ⨅ p : FieldLawCoupling μ ν, p.costdef scaledSpectralLaw (ν : ProbabilityMeasure ℝ) (β : ℝ) : ProbabilityMeasure ℝ :=  ν.map (fun x => β*x)def groundStateEnergy {N : ℕ} (eig : Fin N → ℝ) (U : Rotation N) : ℝ :=  (N : ℝ)⁻¹ * Finset.univ.sup' Finset.univ_nonempty (rotatedEnergy eig U)def thermalVariationalValue (ν : ProbabilityMeasure ℝ) (b β : ℝ) : ℝ :=  (variationalFunctional (measureR (scaledSpectralLaw ν β : Measure ℝ) (β*b))).toReal/βabbrev FieldSpectralData (N : ℕ) := (Fin N → ℝ) × (Fin N → ℝ)def dataPhysicalPressure {N : ℕ} (d : FieldSpectralData N) (U : Orthogonal N) : ℝ :=  rotatedPressure d.1 (matrixRotation U⁻¹) d.2def ConditionalFieldOrbitLaw {Ω : Type*} [MeasurableSpace Ω] {N : ℕ}    (P : Measure Ω) (d : Ω → FieldSpectralData N) (pressure : Ω → ℝ)    (H : Measure (Orthogonal N)) : Prop :=  P.map (fun ω => (d ω,pressure ω)) =    ((P.map d).prod H).map (fun z => (z.1,dataPhysicalPressure z.1 z.2))def spectralExcess {N : ℕ} (eig : Fin N → ℝ) (a b : ℝ) : ℝ :=  (insert 0 (Finset.univ.image (fun i => max (a-eig i) (eig i-b)))).max'    (Finset.insert_nonempty 0 _)run_cmd Lean.modifyEnv fun env => Lean.Meta.auxLemmasExt.setState env {}@[irreducible] def gaussianPatternCount (α : ℝ) (N : ℕ) : ℕ := ⌊α*N⌋₊def marchenkoPasturA (α : ℝ) : ℝ := (1-Real.sqrt α)^2def marchenkoPasturB (α : ℝ) : ℝ := (1+Real.sqrt α)^2def marchenkoPasturLower (α : ℝ) : ℝ := if α ≤ 1 then 0 else marchenkoPasturA αdef marchenkoPasturMeasure (α : ℝ) : Measure ℝ :=  ENNReal.ofReal (max (1-α) 0) • Measure.dirac 0 +    volume.withDensity ((Icc (marchenkoPasturA α) (marchenkoPasturB α)).indicator      (fun x => ENNReal.ofReal        (Real.sqrt ((marchenkoPasturB α-x)*(x-marchenkoPasturA α))/(2*Real.pi*x))))def gaussianPatternLimit (α c : ℝ) : ℝ :=  (variationalFunctional (measureR ((marchenkoPasturMeasure α).map (fun x => c*x))    (max (c*marchenkoPasturLower α) (c*marchenkoPasturB α)))).toRealrun_cmd Lean.modifyEnv fun env => Lean.Meta.auxLemmasExt.setState env {}def gaussianPatternArray {N m : ℕ} (z : EuclideanSpace ℝ (Fin N × Fin m)) :    Matrix (Fin N) (Fin m) ℝ := fun i j => z (i,j)def gaussianPatternSum {N m : ℕ} (z : EuclideanSpace ℝ (Fin N × Fin m)) (σ : Spin N) :    EuclideanSpace ℝ (Fin m) :=  WithLp.toLp 2 ((gaussianPatternArray z)ᵀ *ᵥ (fun i => spinValue (σ i)))def gaussianPatternPressure {N m : ℕ} (c : ℝ)    (z : EuclideanSpace ℝ (Fin N × Fin m)) : ℝ :=  (N : ℝ)⁻¹*logPartition (fun σ : Spin N => c/(2*N)*‖gaussianPatternSum z σ‖^2)run_cmd Lean.modifyEnv fun env => Lean.Meta.auxLemmasExt.setState env {}def gaussianPatternGroundEnergy {N m : ℕ} (ε : ℝ)    (z : EuclideanSpace ℝ (Fin N × Fin m)) : ℝ :=  (N : ℝ)⁻¹*Finset.univ.sup' Finset.univ_nonempty    (fun σ : Spin N => ε/(2*N)*‖gaussianPatternSum z σ‖^2)run_cmd Lean.modifyEnv fun env => Lean.Meta.auxLemmasExt.setState env {}def gaussianPatternColumn {N m : ℕ} (z : EuclideanSpace ℝ (Fin N × Fin m))    (i : Fin N) : EuclideanSpace ℝ (Fin m) := WithLp.toLp 2 (fun j => z (i,j))def gaussianPatternOperator {N m : ℕ} (z : EuclideanSpace ℝ (Fin N × Fin m)) :    (Fin N → ℝ) →L[ℝ] EuclideanSpace ℝ (Fin m) :=  (PiLp.continuousLinearEquiv 2 ℝ (fun _ : Fin m => ℝ)).symm.toContinuousLinearMap.comp    ((gaussianPatternArray z)ᵀ.mulVecLin.toContinuousLinearMap)theorem limiting_pressure_of_extreme_limits_unconditional :  ∀ {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]    (U : (N : ℕ) → Ω → Orthogonal N) (_hU : ∀ N, Measurable (U N))    (_hHaar : ∀ N, (P.map (U N)).IsMulRightInvariant)    (eig : (N : ℕ) → Fin N → ℝ) (ν : ProbabilityMeasure ℝ) (a b : ℝ)    (_hcompact : IsCompact (ν : Measure ℝ).support)    (_hbound : (ν : Measure ℝ).support ⊆ Icc a b)    (_ha : a∈(ν : Measure ℝ).support) (_hb : b∈(ν : Measure ℝ).support)    (_hmin : Tendsto (fun k => spectralMinimum (eig (k+1))) atTop (𝓝 a))    (_hmax : Tendsto (fun k => spectralMaximum (eig (k+1))) atTop (𝓝 b))    (_hweak : Tendsto (fun k => empiricalSpectralLaw (Nat.succ_pos k) (eig (k+1)))      atTop (𝓝 ν)),    Tendsto (fun N => ∫ ω, rotatedPressure (eig N) (matrixRotation (U N ω)⁻¹) (fun _ => 0) ∂P)      atTop (𝓝 (variationalFunctional (measureR (ν : Measure ℝ) b)).toReal) ∧    ∀ᵐ ω ∂P, Tendsto (fun N => rotatedPressure (eig N) (matrixRotation (U N ω)⁻¹) (fun _ => 0))      atTop (𝓝 (variationalFunctional (measureR (ν : Measure ℝ) b)).toReal) := by  sorrytheorem limiting_wasserstein_field_pressure_of_extreme_limits_unconditional :  ∀ {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]    (U : (N : ℕ) → Ω → Orthogonal N) (_hU : ∀ N, Measurable (U N))    (_hHaar : ∀ N, (P.map (U N)).IsMulRightInvariant)    (eig : (N : ℕ) → Fin N → ℝ) (ν : ProbabilityMeasure ℝ) (a b : ℝ)    (_hcompact : IsCompact (ν : Measure ℝ).support)    (_hbound : (ν : Measure ℝ).support ⊆ Icc a b)    (_ha : a∈(ν : Measure ℝ).support) (_hb : b∈(ν : Measure ℝ).support)    (_hmin : Tendsto (fun k => spectralMinimum (eig (k+1))) atTop (𝓝 a))    (_hmax : Tendsto (fun k => spectralMaximum (eig (k+1))) atTop (𝓝 b))    (_hweak : Tendsto (fun k => empiricalSpectralLaw (Nat.succ_pos k) (eig (k+1)))      atTop (𝓝 ν))    (field : (N : ℕ) → Fin N → ℝ) (ξ : ProbabilityMeasure ℝ)    (_hξ : Integrable (fun x : ℝ => x) (ξ : Measure ℝ))    (_hw : Tendsto (fun k => fieldWassersteinOne (empiricalSpectralLaw (Nat.succ_pos k) (field (k+1))) ξ)      atTop (𝓝 0)),    Tendsto (fun N => ∫ ω, rotatedPressure (eig N) (matrixRotation (U N ω)⁻¹) (field N) ∂P)      atTop (𝓝 (magneticFieldFunctional (ν : Measure ℝ) b ξ)) ∧    ∀ᵐ ω ∂P, Tendsto (fun N => rotatedPressure (eig N) (matrixRotation (U N ω)⁻¹) (field N))      atTop (𝓝 (magneticFieldFunctional (ν : Measure ℝ) b ξ)) := by  sorrytheorem positive_temperature_pressure_unconditional :  ∀ {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]    (U : (N : ℕ) → Ω → Orthogonal N) (_hU : ∀ N, Measurable (U N))    (_hHaar : ∀ N, (P.map (U N)).IsMulRightInvariant)    (eig : (N : ℕ) → Fin N → ℝ) (ν : ProbabilityMeasure ℝ) (a b : ℝ)    (_hbound : (ν : Measure ℝ).support ⊆ Icc a b)    (_ha : a∈(ν : Measure ℝ).support) (_hb : b∈(ν : Measure ℝ).support)    (_hno : ∀ ε : ℝ, 0 < ε → ∀ᶠ N in atTop, ∀ i, a-ε ≤ eig N i ∧ eig N i ≤ b+ε)    (β : ℝ) (_hβ : 0 < β)    (_hweak : Tendsto (fun k => empiricalSpectralLaw (Nat.succ_pos k) (eig (k+1)))      atTop (𝓝 ν)),    Tendsto (fun N => ∫ ω, rotatedPressure (fun i => β*eig N i) (matrixRotation (U N ω)⁻¹) (fun _ => 0) ∂P)      atTop (𝓝 (variationalFunctional (measureR (scaledSpectralLaw ν β : Measure ℝ) (β*b))).toReal) ∧    ∀ᵐ ω ∂P, Tendsto (fun N => rotatedPressure (fun i => β*eig N i) (matrixRotation (U N ω)⁻¹) (fun _ => 0))      atTop (𝓝 (variationalFunctional (measureR (scaledSpectralLaw ν β : Measure ℝ) (β*b))).toReal) := by  sorrytheorem ground_state_limit_unconditional :  ∀ {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]    (U : (N : ℕ) → Ω → Orthogonal N) (_hU : ∀ N, Measurable (U N))    (_hHaar : ∀ N, (P.map (U N)).IsMulRightInvariant)    (eig : (N : ℕ) → Fin N → ℝ) (ν : ProbabilityMeasure ℝ) (a b : ℝ)    (_hbound : (ν : Measure ℝ).support ⊆ Icc a b)    (_ha : a∈(ν : Measure ℝ).support) (_hb : b∈(ν : Measure ℝ).support)    (_hno : ∀ ε : ℝ, 0 < ε → ∀ᶠ N in atTop, ∀ i, a-ε ≤ eig N i ∧ eig N i ≤ b+ε)    (_hweak : Tendsto (fun k => empiricalSpectralLaw (Nat.succ_pos k) (eig (k+1)))      atTop (𝓝 ν)),    ∃ M : ℝ,      Tendsto (fun N => ∫ ω, groundStateEnergy (eig N) (matrixRotation (U N ω)⁻¹) ∂P)        atTop (𝓝 M) ∧      (∀ᵐ ω ∂P, Tendsto (fun N => groundStateEnergy (eig N) (matrixRotation (U N ω)⁻¹))        atTop (𝓝 M)) ∧      Tendsto (thermalVariationalValue ν b) atTop (𝓝 M) := by  sorrytheorem random_pressure_tendsto_in_measure_unconditional    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]    (eig : (N : ℕ) → Ω → Fin N → ℝ) (Y : ℕ → Ω → ℝ)    (heig : ∀ N, Measurable (eig N)) (hY : ∀ N, Measurable (Y N))    (H : (N : ℕ) → Measure (Orthogonal N)) [∀ N, IsProbabilityMeasure (H N)]    [∀ N, (H N).IsMulRightInvariant]    (hlaw : ∀ N, ConditionalFieldOrbitLaw P (fun ω => (eig N ω,fun _ => 0)) (Y N) (H N))    (ν : ProbabilityMeasure ℝ) (a b : ℝ)    (hcompact : IsCompact (ν : Measure ℝ).support)    (hbound : (ν : Measure ℝ).support ⊆ Icc a b)    (ha : a∈(ν : Measure ℝ).support) (hb : b∈(ν : Measure ℝ).support)    (hweak : TendstoInMeasure P (fun k ω => LevyProkhorov.ofMeasure      (empiricalSpectralLaw (Nat.succ_pos k) (eig (k+1) ω))) atTop      (fun _ => LevyProkhorov.ofMeasure ν))    (hexcess : TendstoInMeasure P (fun k ω => spectralExcess (eig (k+1) ω) a b)      atTop (fun _ => 0)) :    TendstoInMeasure P (fun k => Y (k+1)) atTop      (fun _ => (variationalFunctional (measureR (ν : Measure ℝ) b)).toReal) := by  sorrytheorem random_pressure_limit_unconditional :  ∀ {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]    (eig : (N : ℕ) → Ω → Fin N → ℝ) (Y : ℕ → Ω → ℝ)    (_heig : ∀ N, Measurable (eig N)) (_hY : ∀ N, Measurable (Y N))    (H : (N : ℕ) → Measure (Orthogonal N)) [∀ N, IsProbabilityMeasure (H N)]    [∀ N, (H N).IsMulRightInvariant]    (_hlaw : ∀ N, ConditionalFieldOrbitLaw P (fun ω => (eig N ω,fun _ => 0)) (Y N) (H N))    (ν : ProbabilityMeasure ℝ) (a b : ℝ)    (_hcompact : IsCompact (ν : Measure ℝ).support)    (_hbound : (ν : Measure ℝ).support ⊆ Icc a b)    (_ha : a∈(ν : Measure ℝ).support) (_hb : b∈(ν : Measure ℝ).support)    (_hweak : TendstoInMeasure P (fun k ω => LevyProkhorov.ofMeasure      (empiricalSpectralLaw (Nat.succ_pos k) (eig (k+1) ω))) atTop      (fun _ => LevyProkhorov.ofMeasure ν))    (_hexcess : TendstoInMeasure P (fun k ω => spectralExcess (eig (k+1) ω) a b)      atTop (fun _ => 0))    (_hUI : UniformIntegrable (fun k => Y (k+1)) 1 P),    TendstoInMeasure P (fun k => Y (k+1)) atTop      (fun _ => (variationalFunctional (measureR (ν : Measure ℝ) b)).toReal) ∧    Tendsto (fun k => eLpNorm (fun ω => Y (k+1) ω-      (variationalFunctional (measureR (ν : Measure ℝ) b)).toReal) 1 P) atTop (𝓝 0) ∧    Tendsto (fun k => ∫ ω, Y (k+1) ω ∂P) atTop      (𝓝 (variationalFunctional (measureR (ν : Measure ℝ) b)).toReal) := by  sorrytheorem random_pressure_tendsto_ae_unconditional :  ∀ {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]    (eig : (N : ℕ) → Ω → Fin N → ℝ) (Y : ℕ → Ω → ℝ)    (_heig : ∀ N, Measurable (eig N)) (_hY : ∀ N, Measurable (Y N))    (H : (N : ℕ) → Measure (Orthogonal N)) [∀ N, IsProbabilityMeasure (H N)]    [∀ N, (H N).IsMulRightInvariant]    (_hlaw : ∀ N, ConditionalFieldOrbitLaw P (fun ω => (eig N ω,fun _ => 0)) (Y N) (H N))    (ν : ProbabilityMeasure ℝ) (a b : ℝ)    (_hcompact : IsCompact (ν : Measure ℝ).support)    (_hbound : (ν : Measure ℝ).support ⊆ Icc a b)    (_ha : a∈(ν : Measure ℝ).support) (_hb : b∈(ν : Measure ℝ).support)    (_hno : ∀ᵐ ω ∂P, ∀ ε : ℝ, 0 < ε → ∀ᶠ N in atTop,      ∀ i, a-ε ≤ eig N ω i ∧ eig N ω i ≤ b+ε)    (_hweak : ∀ᵐ ω ∂P, Tendsto (fun k =>      empiricalSpectralLaw (Nat.succ_pos k) (eig (k+1) ω)) atTop (𝓝 ν)),    ∀ᵐ ω ∂P, Tendsto (fun N => Y N ω) atTop      (𝓝 (variationalFunctional (measureR (ν : Measure ℝ) b)).toReal) := by  sorrytheorem random_field_pressure_tendsto_ae_unconditional :  ∀ {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]    (d : (N : ℕ) → Ω → FieldSpectralData N) (Y : ℕ → Ω → ℝ)    (_hd : ∀ N, Measurable (d N)) (_hY : ∀ N, Measurable (Y N))    (H : (N : ℕ) → Measure (Orthogonal N)) [∀ N, IsProbabilityMeasure (H N)]    [∀ N, (H N).IsMulRightInvariant]    (_hlaw : ∀ N, ConditionalFieldOrbitLaw P (d N) (Y N) (H N))    (ν : ProbabilityMeasure ℝ) (a b : ℝ)    (_hcompact : IsCompact (ν : Measure ℝ).support)    (_hbound : (ν : Measure ℝ).support ⊆ Icc a b)    (_ha : a∈(ν : Measure ℝ).support) (_hb : b∈(ν : Measure ℝ).support)    (_hno : ∀ᵐ ω ∂P, ∀ ε : ℝ, 0 < ε → ∀ᶠ N in atTop,      ∀ i, a-ε ≤ (d N ω).1 i ∧ (d N ω).1 i ≤ b+ε)    (_hweak : ∀ᵐ ω ∂P, Tendsto (fun k =>      empiricalSpectralLaw (Nat.succ_pos k) (d (k+1) ω).1) atTop (𝓝 ν))    (ξ : ProbabilityMeasure ℝ) (_hξ : Integrable (fun x : ℝ => x) (ξ : Measure ℝ))    (_hw : ∀ᵐ ω ∂P, Tendsto (fun k => fieldWassersteinOne      (empiricalSpectralLaw (Nat.succ_pos k) (d (k+1) ω).2) ξ) atTop (𝓝 0)),    ∀ᵐ ω ∂P, Tendsto (fun N => Y N ω) atTop      (𝓝 (magneticFieldFunctional (ν : Measure ℝ) b ξ)) := by  sorrytheorem gaussianPattern_pressure_limit_unconditional :  ∀ (α : ℝ) (_hα : 0 < α)    {Ω : Type u} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]    (Z : (N : ℕ) → Ω → EuclideanSpace ℝ (Fin N × Fin (gaussianPatternCount α N)))    (_hZ : ∀ N, Measurable (Z N)) (_hlaw : ∀ N, HasLaw (Z N) (stdGaussian _) P)    (c : ℝ),    TendstoInMeasure P (fun k ω => gaussianPatternPressure (N := k+1) (m := gaussianPatternCount α (k+1)) c (Z (k+1) ω)) atTop      (fun _ => gaussianPatternLimit α c) ∧    Tendsto (fun k => eLpNorm (fun ω => gaussianPatternPressure (N := k+1) (m := gaussianPatternCount α (k+1)) c (Z (k+1) ω)-      gaussianPatternLimit α c) 1 P) atTop (𝓝 0) ∧    Tendsto (fun k => ∫ ω, gaussianPatternPressure (N := k+1) (m := gaussianPatternCount α (k+1)) c (Z (k+1) ω) ∂P) atTop      (𝓝 (gaussianPatternLimit α c)) := by  sorrytheorem gaussianPattern_ground_limit_unconditional :  ∀ (α : ℝ) (_hα : 0 < α)    {Ω : Type u} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]    (Z : (N : ℕ) → Ω → EuclideanSpace ℝ (Fin N × Fin (gaussianPatternCount α N)))    (_hZ : ∀ N, Measurable (Z N)) (_hlaw : ∀ N, HasLaw (Z N) (stdGaussian _) P)    (ε : ℝ),    ∃ e : ℝ,      TendstoInMeasure P (fun k ω => gaussianPatternGroundEnergy ε (Z (k+1) ω)) atTop (fun _ => e) ∧      Tendsto (fun k => eLpNorm (fun ω => gaussianPatternGroundEnergy ε (Z (k+1) ω)-e) 1 P)        atTop (𝓝 0) ∧      Tendsto (fun k => ∫ ω, gaussianPatternGroundEnergy ε (Z (k+1) ω) ∂P) atTop (𝓝 e) ∧      Tendsto (fun β => gaussianPatternLimit α (ε*β)/β) atTop (𝓝 e) := by  sorrytheorem gaussianPattern_norm_limits_unconditional :  ∀ (α : ℝ) (_hα : 0 < α)    {Ω : Type u} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]    (Z : (N : ℕ) → Ω → EuclideanSpace ℝ (Fin N × Fin (gaussianPatternCount α N)))    (_hZ : ∀ N, Measurable (Z N)) (_hlaw : ∀ N, HasLaw (Z N) (stdGaussian _) P),    ∃ eplus eminus : ℝ, 0 ≤ eplus ∧ eminus ≤ 0 ∧      Tendsto (fun β => gaussianPatternLimit α β/β) atTop (𝓝 eplus) ∧      Tendsto (fun β => gaussianPatternLimit α (-β)/β) atTop (𝓝 eminus) ∧      (TendstoInMeasure P (fun k ω => ‖gaussianPatternOperator (Z (k+1) ω)‖/(k+1)) atTop        (fun _ => Real.sqrt (2*eplus)) ∧       Tendsto (fun k => eLpNorm (fun ω => ‖gaussianPatternOperator (Z (k+1) ω)‖/(k+1)-        Real.sqrt (2*eplus)) 1 P) atTop (𝓝 0)) ∧      (TendstoInMeasure P (fun k ω =>        (Finset.univ.inf' Finset.univ_nonempty (fun σ : Spin (k+1) => ‖gaussianPatternSum (Z (k+1) ω) σ‖))/(k+1))        atTop (fun _ => Real.sqrt (-2*eminus)) ∧       Tendsto (fun k => eLpNorm (fun ω =>        (Finset.univ.inf' Finset.univ_nonempty (fun σ : Spin (k+1) => ‖gaussianPatternSum (Z (k+1) ω) σ‖))/(k+1)-          Real.sqrt (-2*eminus)) 1 P) atTop (𝓝 0)) := by  sorryend InvariantIsingendend OAI

Every extracted statement of the accompanying papers

The statements the atlas extracted automatically from each accompanying paper’s TeX source, with links to the full sources.

All-temperature pressure for orthogonally invariant Ising spin glasses

Theorem (Limiting pressure)

\lim_{N\to\infty}\E P_N =\lim_{N\to\infty}P_N =\mathcal F(\mu) :=\inf_{p\in\cP}\{S(p)+G_1(p)\},

where the second limit holds almost surely. No independence of the matrices U_N across dimensions is required.

Section 1, Introduction Read it in the paper TeX source, line 186

Show the TeX

Let $\Lambda_N$ be deterministic real diagonal matrices whose empirical
spectral measures converge weakly to a compactly supported probability
law $\mu$. Assume that their smallest and largest eigenvalues converge
to the respective edges of $\supp\mu$. Let $U_N$ be Haar distributed
on $O(N)$, and define $P_N$ using the uniform spin probability in
Equation~\eqref{eq:pressure}. With $S$ and $G_1$ as in
Equations~\eqref{eq:S}--\eqref{eq:G},
\begin{equation}
 \lim_{N\to\infty}\E P_N
 =\lim_{N\to\infty}P_N
 =\mathcal F(\mu)
 :=\inf_{p\in\cP}\{S(p)+G_1(p)\},
 
\end{equation}
where the second limit holds almost surely. No independence of the
matrices $U_N$ across dimensions is required.

Configuration and file facts

File: lean/ComparatorChallenges/InvariantIsing.lean
OpenAI’s Lean catalogue: OpenAI’s Lean catalogue does not list this as a main result; the release’s Lean notes for family 234 link it.
Solution module: OAI.Probability.InvariantIsing.Unconditional
Allowed axioms: propext, Quot.sound, Classical.choiceThe axioms this configuration allows a proof to use. A replay shows which of them a proof uses.
Imports: Mathlib
Imports from outside Mathlib: None
Local vocabulary: 66 local vocabulary declarations
Lines of Lean, without comments or blank lines: 389
Second proof-verification program (nanoda): Off in OpenAI's configuration.

A shareable summary of this page: the proposed paper match, what the Lean statement expresses, and which reviews are recorded.

Plectis Atlas