Plectis Atlas
Search

↑ and ↓ move, Enter opens, Esc closes.

Lean statement

Uniform ground-state condensation in the dilute hard-sphere gas

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.

Theorem selected for verification: OAI.HardSphere.condensation_with_mixed

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

See the candidate theoremWho ran the proof-verification programReport 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 condensation_with_mixed :    ∃ε₀ c₀ : ℝ,0<ε₀ ∧ 0<c₀ ∧    ∀a ρ : ℝ,0<a → 0<ρ → ρ*a^3<ε₀ →    ∀(N : ℕ→ℕ) (L : ℕ→Length) (hN : ∀k,0<N k),      Tendsto N atTop atTop → Tendsto (fun k ↦ (L k).val) atTop atTop →      Tendsto (fun k ↦ (N k:ℝ)/(L k).val^3) atTop (𝓝 ρ) →      (∀Ψ : (k : ℕ)→Jet (N k) (L k),        (∀k,IsGroundVector (N k) (L k) a (Ψ k)) →        c₀≤liminf (fun k ↦ occupation (hN k) (Ψ k).1) atTop) ∧      (∀T : (k : ℕ)→Density.Operator (ScalarL2 (N k) (L k)),        (∀k,GroundSupported a (T k)) →        c₀≤liminf (fun k ↦ mixedOccupation (hN k) (T k)) atTop) := 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.HardSphere.Length line 17

    abbrev Length := {L : ℝ // 0 < L}

  • abbreviation OAI.HardSphere.Torus line 21

    abbrev Torus (L : Length) := Fin 3 → AddCircle L.val

  • abbreviation OAI.HardSphere.Configuration line 23

    abbrev Configuration (N : ℕ) (L : Length) := Fin N → Torus L

  • abbreviation OAI.HardSphere.LiftedConfiguration line 25

    abbrev LiftedConfiguration (N : ℕ) := Fin N → Fin 3 → ℝ

  • abbreviation OAI.HardSphere.Direction line 27

    abbrev Direction (N : ℕ) := Fin N × Fin 3

  • definition OAI.HardSphere.torusDistance line 29

    def torusDistance (L : Length) (x y : Torus L) : ℝ :=  Real.sqrt (∑ j : Fin 3, dist (x j) (y j) ^ 2)

  • definition OAI.HardSphere.allowed line 32

    def allowed (N : ℕ) (L : Length) (a : ℝ) : Set (Configuration N L) :=  {X | ∀ i j : Fin N, i < j → a < torusDistance L (X i) (X j)}

  • definition OAI.HardSphere.project line 35

    def project (N : ℕ) (L : Length) (X : LiftedConfiguration N) : Configuration N L :=  fun i j ↦ (X i j : AddCircle L.val)

  • definition OAI.HardSphere.representative line 38

    def representative (N : ℕ) (L : Length) (X : Configuration N L) : LiftedConfiguration N :=  fun i j ↦ (AddCircle.equivIco L.val 0 (X i j)).val

  • definition OAI.HardSphere.coordDerivative line 41

    def coordDerivative (N : ℕ) (L : Length) (f : Configuration N L → ℂ)    (p : Direction N) (X : Configuration N L) : ℂ :=  fderiv ℝ (fun Y : LiftedConfiguration N ↦ f (project N L Y))    (representative N L X) (Pi.single p.1 (Pi.single p.2 1))

  • abbreviation OAI.HardSphere.ScalarL2 line 46

    abbrev ScalarL2 (N : ℕ) (L : Length) : Type :=  Lp ℂ 2 (volume : Measure (Configuration N L))

  • abbreviation OAI.HardSphere.Jet line 49

    abbrev Jet (N : ℕ) (L : Length) :=  ScalarL2 N L × (Direction N → ScalarL2 N L)

  • structure OAI.HardSphere.SmoothTest line 52

    structure SmoothTest (N : ℕ) (L : Length) (a : ℝ) where  toFun : Configuration N L → ℂ  smooth : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (fun X : LiftedConfiguration N ↦ toFun (project N L X))  compact : HasCompactSupport toFun  support_allowed : tsupport toFun ⊆ allowed N L a  memLp : MemLp toFun (2 : ℕ) (volume : Measure (Configuration N L))  partial_memLp : ∀ p : Direction N, MemLp (coordDerivative N L toFun p) (2 : ℕ) volume

  • definition OAI.HardSphere.SmoothTest.jet line 60

    def SmoothTest.jet {N : ℕ} {L : Length} {a : ℝ} (f : SmoothTest N L a) : Jet N L :=  (f.memLp.toLp f.toFun, fun p ↦ (f.partial_memLp p).toLp (coordDerivative N L f.toFun p))

  • definition OAI.HardSphere.dirichletDomain line 63

    def dirichletDomain (N : ℕ) (L : Length) (a : ℝ) : Set (Jet N L) :=  closure (Set.range (SmoothTest.jet (N := N) (L := L) (a := a)))

  • definition OAI.HardSphere.energy line 66

    def energy {N : ℕ} {L : Length} (u : Jet N L) : ℝ :=  ∑ p : Direction N, ‖u.2 p‖ ^ 2

  • definition OAI.HardSphere.bosonic line 69

    def bosonic {N : ℕ} {L : Length} (ψ : ScalarL2 N L) : Prop :=  ∀ σ : Equiv.Perm (Fin N),    (fun X : Configuration N L ↦ ψ (fun i ↦ X (σ i))) =ᵐ[volume] ψ

  • definition OAI.HardSphere.IsGroundVector line 73

    def IsGroundVector (N : ℕ) (L : Length) (a : ℝ) (u : Jet N L) : Prop :=  u ∈ dirichletDomain N L a ∧ bosonic u.1 ∧ ‖u.1‖ = 1 ∧    ∀ v ∈ dirichletDomain N L a, bosonic v.1 → ‖v.1‖ = 1 → energy u ≤ energy v

  • definition OAI.HardSphere.insertFirst line 77

    def insertFirst {N : ℕ} (hN : 0 < N) {L : Length}    (x : Torus L) (Y : Configuration (N - 1) L) : Configuration N L :=  fun i ↦ Fin.cons (α := fun _ ↦ Torus L) x Y (Fin.cast (Nat.sub_add_cancel (Nat.succ_le_of_lt hN)).symm i)

  • definition OAI.HardSphere.occupation line 81

    def occupation {N : ℕ} (hN : 0 < N) {L : Length} (ψ : ScalarL2 N L) : ℝ :=  (L.val ^ 3)⁻¹ * ∫ Y : Configuration (N - 1) L,    ‖∫ x : Torus L, ψ (insertFirst hN x Y)‖ ^ 2

  • definition OAI.HardSphere.Density.basisSet line 88

    def basisSet : Set H := (exists_hilbertBasis (𝕜:=ℂ) (E:=H)).choose

  • definition OAI.HardSphere.Density.basis line 90

    def basis : HilbertBasis (basisSet H) ℂ H :=  (exists_hilbertBasis (𝕜:=ℂ) (E:=H)).choose_spec.choose

  • structure OAI.HardSphere.Density.Operator line 93

    structure Operator where  toCLM : H →L[ℂ] H  positive : 0≤toCLM  trace_one : HasSum (fun i : basisSet H ↦ (inner ℂ (basis H i) (toCLM (basis H i))).re) 1

  • definition OAI.HardSphere.Density.Operator.compressionTrace line 101

    def Operator.compressionTrace (T : Operator H) (A : H →L[ℂ] K) : ℝ :=  let adjoint := DFunLike.coe (F := (H →L[ℂ] K) ≃ₗᵢ⋆[ℂ] K →L[ℂ] H)    (β := fun _ ↦ K →L[ℂ] H) ContinuousLinearMap.adjoint A  ∑' j : basisSet K,(inner ℂ (adjoint (basis K j)) (T.toCLM (adjoint (basis K j)))).re

5 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: absolute, condensation, constants, ground, hard, normalized, sequence, sphere and one more.

Statements in Ground-state condensation in the dilute hard-sphere gas come first because the release lists only that paper for this Lean statement.

Theorem 1.1 of Ground-state condensation in the dilute hard-sphere gas

Theorem (Condensation in every ground state)

There are absolute constants \varepsilon_0,c_0>0 with the following property. Fix a,\rho>0 satisfying \rho a^3<\varepsilon_0. For every sequence of particle numbers N_k and lengths L_k such that

N_k\longrightarrow\infty,\qquad L_k\longrightarrow\infty, \qquad \frac{N_k}{L_k^3}\longrightarrow\rho,

and every choice of normalized, possibly complex, bosonic ground eigenvectors \Psi_k of the hard-sphere Hamiltonians,

\liminf_{k\to\infty} B(\Psi_k)\ge c_0.
Section 1, Introduction Read it in the paper TeX source, line 48
Show the TeX
There are absolute constants $\varepsilon_0,c_0>0$ with the following
property. Fix $a,\rho>0$ satisfying $\rho a^3<\varepsilon_0$.
For every sequence of particle numbers $N_k$ and lengths $L_k$ such that
\[
 N_k\longrightarrow\infty,\qquad L_k\longrightarrow\infty,
 \qquad \frac{N_k}{L_k^3}\longrightarrow\rho,
\]
and every choice of normalized, possibly complex, bosonic ground
eigenvectors $\Psi_k$ of the hard-sphere Hamiltonians,
\begin{equation}
 \liminf_{k\to\infty} B(\Psi_k)\ge c_0.
\end{equation}

Other possible paper matches, closest wording first

  • Corollary 1.2 of Ground-state condensation in the dilute hard-sphere gas. Words of the Lean statement, its names split into words, that also appear in the theorem: space, operators, supported, bosonic, pi, density and two more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: sequence and states.
  • Proposition 10.1 of Ground-state condensation in the dilute hard-sphere gas. Words of the Lean statement, its names split into words, that also appear in the theorem: compact, ranges, complex, integer, vector, bosonic and two more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: absolute and constants.
  • Proposition 4.1 of Quantum Depletion and Momentum Distribution in the Dilute Hard-Sphere Bose Gas. Words of the Lean statement, its names split into words, that also appear in the theorem: lengths, zero, first, complex, energy, vectors and four more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: along, thermodynamic, sequence, limit and uniform.
  • Proposition 9.4 of Ground-state condensation in the dilute hard-sphere gas. Words of the Lean statement, its names split into words, that also appear in the theorem: slice, vector, volume, one and ground. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: whenever, absolute, constants and uniform.
  • Theorem 1.1 of A density-uniform condensate bound for dilute Bose gases. Words of the Lean statement, its names split into words, that also appear in the theorem: integer, property and density. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: condensate, fraction, sequence, least, limiting, rho and one more.
  • Theorem 1.1 of Quantum Depletion and Momentum Distribution in the Dilute Hard-Sphere Bose Gas. Words of the Lean statement, its names split into words, that also appear in the theorem: real, continuous, sqrt, property, pi and function. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: sequence and rho.

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; MathVet. 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

MathVet

How they ran it, in their words

An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge. Its protocol describes a planned error-rate study; this import does not establish that the study has been completed.

  • Accepted Their term: “comparator-sandboxed-pass”.

    Re-run through Comparator in a sandboxed virtual machine: accepted.

    Reported 8 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 267’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.

Neither group finds that the Lean statements express or imply the whole advertised result. They describe what the statements express in different terms.

  • MathVet

    Finds part of it stated, or a narrower or weaker statement Their term: “weaker-statement”.

    The challenge statements do not imply the headline claim: they state a nontrivially weaker statement. Their record

    Their note: condensation_with_mixed : ∃ ε₀ c₀ > 0, ∀ a ρ, ρ a^3 < ε₀ → ∀ thermodynamic sequences (N_k, L_k), (∀ pure ground vectors Ψ_k, c₀ ≤ liminf occupation Ψ_k) ∧ (∀ density operators supported on the ground space, c₀ ≤ liminf mixedOccupation) is ZERO-temperature ground-state condensation of the hard-sphere gas with a non-sharp lower bound c₀ (docs: 'concerns ground states, without a positive-temperature assertion'). The summary's headline claims are not stated: BEC for the exact canonical Gibbs state at a strictly positive volume-independent temperature, and the sharp Bogoliubov leading quantum-depletion law (thermodynamic limit before dilute limit) for hard spheres and bounded finite-range potentials.

    Definitions the group asks readers to compare with the paper: Hand-built hard-sphere gas: Dirichlet form domain dirichletDomain N L a := closure (range SmoothTest.jet) (smooth compactly supported functions vanishing on d(x_i,x_j) ≤ a on the torus AddCircle L ^3), energy u := Σ ‖∇_p u‖² (no 1/2), bosonic, IsGroundVector, occupation ψ := L^{-3} ∫_Y |∫_x ψ(x,Y)|² and a custom trace-class Density.Operator; the zero-mode occupation fraction matches the standard condensate fraction, but all objects are hand-written.

  • Carlos Toledo’s cert-machine

    Finds part of it stated, or a narrower or weaker statement Their term: “NARROWER — UNLINKED”.

    The challenge statements state less than the headline; the missing part comes from a paper the Lean note does not link. Their record

    Their note: Neither headline claim is stated. What is stated — ground-state condensation with a uniform positive lower bound c₀ on the condensate fraction in the dilute hard-sphere gas (the 'Ground-state condensation' manuscript) — is weaker than the zero-temperature depletion law (sentence 2) and says nothing at positive temperature (sentence 1). The positive-temperature omission is declared; the depletion-law omission (hard spheres and bounded potentials) is not.

Read the complete assessments on the family page.

OpenAI’s own note on what this Lean statement covers

“There are absolute constants $\varepsilon_0,c_0>0$ such that, whenever the density $\rho$ and hard-sphere radius $a$ satisfy $\rho a^3<\varepsilon_0$, the condensate occupation fraction has limit inferior at least $c_0$ along every thermodynamic sequence with $N/L^3\to\rho$.”

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

386 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: 198 to its own declarations, 344 to Mathlib’s documentation. 32 declared names also link to the same declaration in OpenAI’s library. 1 identifier stays plain because it resolves to no single declaration: a variable Lean binds automatically, notation, or a name 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 Mathlib/-!# Ground-state condensation in the dilute hard-sphere gasThe main result covers all pure ground states and all density operators supported on the ground space. In particular it covers the normalized ground-space projection.Only the definitions needed to state this result are retained below.-/noncomputable sectionopen MeasureTheory Filter Setopen scoped ENNReal Topology BigOperators InnerProductSpace ComplexOrder NNRealnamespace OAI.HardSphereabbrev Length := {L : ℝ // 0 < L}instance lengthPositive (L : Length) : Fact (0 < L.val) := ⟨L.property⟩abbrev Torus (L : Length) := Fin 3 → AddCircle L.valabbrev Configuration (N : ℕ) (L : Length) := Fin N → Torus Labbrev LiftedConfiguration (N : ℕ) := Fin N → Fin 3 → ℝabbrev Direction (N : ℕ) := Fin N × Fin 3def torusDistance (L : Length) (x y : Torus L) : ℝ :=  Real.sqrt (∑ j : Fin 3, dist (x j) (y j) ^ 2)def allowed (N : ℕ) (L : Length) (a : ℝ) : Set (Configuration N L) :=  {X | ∀ i j : Fin N, i < j → a < torusDistance L (X i) (X j)}def project (N : ℕ) (L : Length) (X : LiftedConfiguration N) : Configuration N L :=  fun i j ↦ (X i j : AddCircle L.val)def representative (N : ℕ) (L : Length) (X : Configuration N L) : LiftedConfiguration N :=  fun i j ↦ (AddCircle.equivIco L.val 0 (X i j)).valdef coordDerivative (N : ℕ) (L : Length) (f : Configuration N L → ℂ)    (p : Direction N) (X : Configuration N L) : ℂ :=  fderiv ℝ (fun Y : LiftedConfiguration N ↦ f (project N L Y))    (representative N L X) (Pi.single p.1 (Pi.single p.2 1))abbrev ScalarL2 (N : ℕ) (L : Length) : Type :=  Lp ℂ 2 (volume : Measure (Configuration N L))abbrev Jet (N : ℕ) (L : Length) :=  ScalarL2 N L × (Direction N → ScalarL2 N L)structure SmoothTest (N : ℕ) (L : Length) (a : ℝ) where  toFun : Configuration N L → ℂ  smooth : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (fun X : LiftedConfiguration N ↦ toFun (project N L X))  compact : HasCompactSupport toFun  support_allowed : tsupport toFun ⊆ allowed N L a  memLp : MemLp toFun (2 : ℕ) (volume : Measure (Configuration N L))  partial_memLp : ∀ p : Direction N, MemLp (coordDerivative N L toFun p) (2 : ℕ) volumedef SmoothTest.jet {N : ℕ} {L : Length} {a : ℝ} (f : SmoothTest N L a) : Jet N L :=  (f.memLp.toLp f.toFun, fun p ↦ (f.partial_memLp p).toLp (coordDerivative N L f.toFun p))def dirichletDomain (N : ℕ) (L : Length) (a : ℝ) : Set (Jet N L) :=  closure (Set.range (SmoothTest.jet (N := N) (L := L) (a := a)))def energy {N : ℕ} {L : Length} (u : Jet N L) : ℝ :=  ∑ p : Direction N, ‖u.2 p‖ ^ 2def bosonic {N : ℕ} {L : Length} (ψ : ScalarL2 N L) : Prop :=  ∀ σ : Equiv.Perm (Fin N),    (fun X : Configuration N L ↦ ψ (fun i ↦ X (σ i))) =ᵐ[volume] ψdef IsGroundVector (N : ℕ) (L : Length) (a : ℝ) (u : Jet N L) : Prop :=  u ∈ dirichletDomain N L a ∧ bosonic u.1 ∧ ‖u.1‖ = 1 ∧    ∀ v ∈ dirichletDomain N L a, bosonic v.1 → ‖v.1‖ = 1 → energy u ≤ energy vdef insertFirst {N : ℕ} (hN : 0 < N) {L : Length}    (x : Torus L) (Y : Configuration (N - 1) L) : Configuration N L :=  fun i ↦ Fin.cons (α := fun _ ↦ Torus L) x Y (Fin.cast (Nat.sub_add_cancel (Nat.succ_le_of_lt hN)).symm i)def occupation {N : ℕ} (hN : 0 < N) {L : Length} (ψ : ScalarL2 N L) : ℝ :=  (L.val ^ 3)⁻¹ * ∫ Y : Configuration (N - 1) L,    ‖∫ x : Torus L, ψ (insertFirst hN x Y)‖ ^ 2namespace Densityvariable (H : Type*) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]def basisSet : Set H := (exists_hilbertBasis (𝕜:=ℂ) (E:=H)).choosedef basis : HilbertBasis (basisSet H) ℂ H :=  (exists_hilbertBasis (𝕜:=ℂ) (E:=H)).choose_spec.choosestructure Operator where  toCLM : H →L[ℂ] H  positive : 0≤toCLM  trace_one : HasSum (fun i : basisSet H ↦ (inner ℂ (basis H i) (toCLM (basis H i))).re) 1variable {H K : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]  [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]def Operator.compressionTrace (T : Operator H) (A : H →L[ℂ] K) : ℝ :=  let adjoint := DFunLike.coe (F := (H →L[ℂ] K) ≃ₗᵢ⋆[ℂ] K →L[ℂ] H)    (β := fun _ ↦ K →L[ℂ] H) ContinuousLinearMap.adjoint A  ∑' j : basisSet K,(inner ℂ (adjoint (basis K j)) (T.toCLM (adjoint (basis K j)))).reend Densitynamespace Orbitaldef sliceIntegral {N : ℕ} (hN : 0<N) {L : Length} (ψ : ScalarL2 N L) (Y : Configuration (N-1) L) : ℂ :=  (Real.sqrt (L.val^3))⁻¹ • ∫x : Torus L,ψ (insertFirst hN x Y)def map {N : ℕ} (hN : 0<N) {L : Length} (ψ : ScalarL2 N L) : ScalarL2 (N-1) L := by  have integral_mul_le_sqrt {X : Type} [MeasurableSpace X] {ν : Measure X} (f g : X → ℝ) (hf : MemLp f 2 ν) (hg : MemLp g 2 ν)      (hf0 : 0 ≤ᵐ[ν] f) (hg0 : 0 ≤ᵐ[ν] g) :      ∫ x, f x * g x ∂ν ≤ Real.sqrt (∫ x, f x ^ 2 ∂ν) *        Real.sqrt (∫ x, g x ^ 2 ∂ν) := by    have h := integral_mul_le_Lp_mul_Lq_of_nonneg      Real.HolderConjugate.two_two hf0 hg0 (by simpa using hf) (by simpa using hg)    simpa only [Real.rpow_two, ← Real.sqrt_eq_rpow] using h  have integral_norm_sq_le {X : Type} [MeasurableSpace X] {ν : Measure X} [IsFiniteMeasure ν] {f : X → ℂ} (hf : MemLp f 2 ν) :      (∫ x, ‖f x‖ ∂ν)^2 ≤ ν.real univ * ∫ x, ‖f x‖ ^ 2 ∂ν := by    have h := integral_mul_le_sqrt (fun _ : X ↦ 1) (fun x ↦ ‖f x‖)      (memLp_const (1 : ℝ)) hf.norm (Eventually.of_forall fun _ ↦ zero_le_one)      (Eventually.of_forall fun _ ↦ norm_nonneg _)    simp only [one_mul, one_pow, integral_const, smul_eq_mul, mul_one] at h    have ha : 0 ≤ ∫ x, ‖f x‖ ∂ν := integral_nonneg fun _ ↦ norm_nonneg _    have hm : 0 ≤ ∫ x, ‖f x‖^2 ∂ν := integral_nonneg fun _ ↦ sq_nonneg _    have hs := (sq_le_sq₀ ha (by positivity)).2 h    simpa only [mul_pow, Real.sq_sqrt (measureReal_nonneg), Real.sq_sqrt hm] using hs  have memLp_slices {X Y : Type} [MeasurableSpace X] [MeasurableSpace Y] {ν : Measure X} {μ : Measure Y} [IsFiniteMeasure ν] [IsFiniteMeasure μ] {f : Y × X → ℂ} (hf : MemLp f 2 (μ.prod ν)) :      ∀ᵐ y ∂μ, MemLp (fun x ↦ f (y,x)) 2 ν := by    filter_upwards [hf.aestronglyMeasurable.prodMk_left,      (hf.integrable_norm_pow (by norm_num : (2 : ℕ) ≠ 0)).prod_right_ae] with y hm hi    exact (memLp_two_iff_integrable_sq_norm hm).2 hi  have memLp_integral_norm {X Y : Type} [MeasurableSpace X] [MeasurableSpace Y] {ν : Measure X} {μ : Measure Y} [IsFiniteMeasure ν] [IsFiniteMeasure μ] {f : Y × X → ℂ} (hf : MemLp f 2 (μ.prod ν)) :      MemLp (fun y ↦ ∫ x, ‖f (y,x)‖ ∂ν) 2 μ := by    have hm := hf.aestronglyMeasurable.norm.integral_prod_right'    apply (memLp_two_iff_integrable_sq hm).2    have hi := (hf.integrable_norm_pow (by norm_num : (2 : ℕ) ≠ 0)).integral_prod_left    apply (hi.const_mul (ν.real univ)).mono' (hm.pow 2)    filter_upwards [memLp_slices hf] with y hy    change ‖(∫ x, ‖f (y,x)‖ ∂ν)^2‖ ≤ _    rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)]    exact integral_norm_sq_le hy  have cons_preserving {n : ℕ} (L : Length) :      MeasurePreserving (fun p : Configuration n L × Torus L ↦ Fin.cons (α:=fun _ ↦ Torus L) p.2 p.1)        (volume.prod volume) volume := by    have h := (volume_preserving_piFinSuccAbove (fun _ : Fin (n+1) ↦ Torus L) 0).symm    have hh := h.comp (Measure.measurePreserving_swap (μ:= (volume : Measure (Configuration n L))) (ν:=volume))    convert hh using 1; try rfl    funext p i    simp [MeasurableEquiv.piFinSuccAbove]  have insertFirst_preserving {N : ℕ} (hN : 0<N) (L : Length) :      MeasurePreserving (fun p : Torus L×Configuration (N-1) L ↦ insertFirst hN p.1 p.2)        ((volume : Measure (Torus L)).prod volume) volume := by    cases N with    | zero => omega    | succ n =>      unfold insertFirst      have h := (cons_preserving (n:=n) L).comp        (Measure.measurePreserving_swap (μ:=(volume : Measure (Torus L))) (ν:=volume))      convert h using 1 <;> simp [Function.comp_def]  have bathFirst_preserving {N : ℕ} (hN : 0<N) (L : Length) :      MeasurePreserving (fun p : Configuration (N-1) L×Torus L ↦ insertFirst hN p.2 p.1)        ((volume : Measure (Configuration (N-1) L)).prod volume) volume :=    (insertFirst_preserving hN L).comp (Measure.measurePreserving_swap)  have ground_slice_memLp {N : ℕ} (hN : 0<N) {L : Length} (ψ : ScalarL2 N L) :      MemLp (fun p : Configuration (N-1) L×Torus L ↦ ψ (insertFirst hN p.2 p.1)) 2        ((volume : Measure (Configuration (N-1) L)).prod volume) :=    (Lp.memLp ψ).comp_measurePreserving (bathFirst_preserving hN L)  have sliceIntegral_memLp {N : ℕ} (hN : 0<N) {L : Length} (ψ : ScalarL2 N L) : MemLp (sliceIntegral hN ψ) 2 volume := by    have hf := ground_slice_memLp hN ψ    have ha := memLp_integral_norm hf    have hh : MemLp (fun Y ↦ ∫x : Torus L,ψ (insertFirst hN x Y)) 2 volume := by      refine ha.mono' hf.aestronglyMeasurable.integral_prod_right' ?_      exact Eventually.of_forall fun Y ↦ norm_integral_le_integral_norm _    exact hh.const_smul ((Real.sqrt (L.val^3))⁻¹ : ℝ)  exact (sliceIntegral_memLp hN ψ).toLp (sliceIntegral hN ψ)def continuous {N : ℕ} (hN : 0<N) {L : Length} : ScalarL2 N L →L[ℂ] ScalarL2 (N-1) L := by  have scalar_norm_sq_integral {N : ℕ} {L : Length} (u : ScalarL2 N L) :      ‖u‖^2 = ∫ X, ‖u X‖^2 := by    rw [← real_inner_self_eq_norm_sq (F := ScalarL2 N L), L2.inner_def]    simp only [real_inner_self_eq_norm_sq]  have volume_torus (L : Length) : (volume : Measure (Torus L)) Set.univ = ENNReal.ofReal (L.val^3) := by    rw [volume_pi,Measure.pi_univ]    simp only [AddCircle.measure_univ,Finset.prod_const,Finset.card_univ,Fintype.card_fin,      ENNReal.ofReal_pow L.property.le]  have integral_mul_le_sqrt {X : Type} [MeasurableSpace X] {ν : Measure X} (f g : X → ℝ) (hf : MemLp f 2 ν) (hg : MemLp g 2 ν)      (hf0 : 0 ≤ᵐ[ν] f) (hg0 : 0 ≤ᵐ[ν] g) :      ∫ x, f x * g x ∂ν ≤ Real.sqrt (∫ x, f x ^ 2 ∂ν) *        Real.sqrt (∫ x, g x ^ 2 ∂ν) := by    have h := integral_mul_le_Lp_mul_Lq_of_nonneg      Real.HolderConjugate.two_two hf0 hg0 (by simpa using hf) (by simpa using hg)    simpa only [Real.rpow_two, ← Real.sqrt_eq_rpow] using h  have integral_norm_sq_le {X : Type} [MeasurableSpace X] {ν : Measure X} [IsFiniteMeasure ν] {f : X → ℂ} (hf : MemLp f 2 ν) :      (∫ x, ‖f x‖ ∂ν)^2 ≤ ν.real univ * ∫ x, ‖f x‖ ^ 2 ∂ν := by    have h := integral_mul_le_sqrt (fun _ : X ↦ 1) (fun x ↦ ‖f x‖)      (memLp_const (1 : ℝ)) hf.norm (Eventually.of_forall fun _ ↦ zero_le_one)      (Eventually.of_forall fun _ ↦ norm_nonneg _)    simp only [one_mul, one_pow, integral_const, smul_eq_mul, mul_one] at h    have ha : 0 ≤ ∫ x, ‖f x‖ ∂ν := integral_nonneg fun _ ↦ norm_nonneg _    have hm : 0 ≤ ∫ x, ‖f x‖^2 ∂ν := integral_nonneg fun _ ↦ sq_nonneg _    have hs := (sq_le_sq₀ ha (by positivity)).2 h    simpa only [mul_pow, Real.sq_sqrt (measureReal_nonneg), Real.sq_sqrt hm] using hs  have memLp_slices {X Y : Type} [MeasurableSpace X] [MeasurableSpace Y] {ν : Measure X} {μ : Measure Y} [IsFiniteMeasure ν] [IsFiniteMeasure μ] {f : Y × X → ℂ} (hf : MemLp f 2 (μ.prod ν)) :      ∀ᵐ y ∂μ, MemLp (fun x ↦ f (y,x)) 2 ν := by    filter_upwards [hf.aestronglyMeasurable.prodMk_left,      (hf.integrable_norm_pow (by norm_num : (2 : ℕ) ≠ 0)).prod_right_ae] with y hm hi    exact (memLp_two_iff_integrable_sq_norm hm).2 hi  have memLp_integral_norm {X Y : Type} [MeasurableSpace X] [MeasurableSpace Y] {ν : Measure X} {μ : Measure Y} [IsFiniteMeasure ν] [IsFiniteMeasure μ] {f : Y × X → ℂ} (hf : MemLp f 2 (μ.prod ν)) :      MemLp (fun y ↦ ∫ x, ‖f (y,x)‖ ∂ν) 2 μ := by    have hm := hf.aestronglyMeasurable.norm.integral_prod_right'    apply (memLp_two_iff_integrable_sq hm).2    have hi := (hf.integrable_norm_pow (by norm_num : (2 : ℕ) ≠ 0)).integral_prod_left    apply (hi.const_mul (ν.real univ)).mono' (hm.pow 2)    filter_upwards [memLp_slices hf] with y hy    change ‖(∫ x, ‖f (y,x)‖ ∂ν)^2‖ ≤ _    rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)]    exact integral_norm_sq_le hy  have cons_preserving {n : ℕ} (L : Length) :      MeasurePreserving (fun p : Configuration n L × Torus L ↦ Fin.cons (α:=fun _ ↦ Torus L) p.2 p.1)        (volume.prod volume) volume := by    have h := (volume_preserving_piFinSuccAbove (fun _ : Fin (n+1) ↦ Torus L) 0).symm    have hh := h.comp (Measure.measurePreserving_swap (μ:= (volume : Measure (Configuration n L))) (ν:=volume))    convert hh using 1; try rfl    funext p i    simp [MeasurableEquiv.piFinSuccAbove]  have insertFirst_preserving {N : ℕ} (hN : 0<N) (L : Length) :      MeasurePreserving (fun p : Torus L×Configuration (N-1) L ↦ insertFirst hN p.1 p.2)        ((volume : Measure (Torus L)).prod volume) volume := by    cases N with    | zero => omega    | succ n =>      unfold insertFirst      have h := (cons_preserving (n:=n) L).comp        (Measure.measurePreserving_swap (μ:=(volume : Measure (Torus L))) (ν:=volume))      convert h using 1 <;> simp [Function.comp_def]  have bathFirst_preserving {N : ℕ} (hN : 0<N) (L : Length) :      MeasurePreserving (fun p : Configuration (N-1) L×Torus L ↦ insertFirst hN p.2 p.1)        ((volume : Measure (Configuration (N-1) L)).prod volume) volume :=    (insertFirst_preserving hN L).comp (Measure.measurePreserving_swap)  have ground_slice_memLp {N : ℕ} (hN : 0<N) {L : Length} (ψ : ScalarL2 N L) :      MemLp (fun p : Configuration (N-1) L×Torus L ↦ ψ (insertFirst hN p.2 p.1)) 2        ((volume : Measure (Configuration (N-1) L)).prod volume) :=    (Lp.memLp ψ).comp_measurePreserving (bathFirst_preserving hN L)  have occupation_le_norm_sq {N : ℕ} (hN : 0<N) {L : Length} (ψ : ScalarL2 N L) :      occupation hN ψ≤‖ψ‖^2 := by    have hLp := L.property    let f := fun p : Configuration (N-1) L×Torus L ↦ ψ (insertFirst hN p.2 p.1)    have hf : MemLp f 2 (volume.prod volume) := ground_slice_memLp hN ψ    have ha := memLp_integral_norm hf    have hc : MemLp (fun Y ↦ ‖∫x,f (Y,x)‖) 2 volume := by      refine ha.mono' hf.aestronglyMeasurable.integral_prod_right'.norm ?_      exact Eventually.of_forall fun Y ↦ by        rw [Real.norm_eq_abs,abs_of_nonneg (norm_nonneg _)]        exact norm_integral_le_integral_norm _    have hi := (hf.integrable_norm_pow (by norm_num : (2:ℕ)≠0)).integral_prod_left    have hbound : (∫Y,‖∫x,f (Y,x)‖^2)≤(volume : Measure (Torus L)).real univ * ∫p,‖f p‖^2 ∂volume.prod volume := by      calc        _ ≤ ∫Y,(volume : Measure (Torus L)).real univ * ∫x,‖f (Y,x)‖^2 := by          apply integral_mono_ae hc.integrable_sq (hi.const_mul _)          filter_upwards [memLp_slices hf] with Y hY          exact (pow_le_pow_left₀ (norm_nonneg _) (norm_integral_le_integral_norm _) 2).trans            (integral_norm_sq_le hY)        _ = _ := by rw [integral_const_mul,←integral_prod _ (hf.integrable_norm_pow (by norm_num : (2:ℕ)≠0))]    have hm : (∫p,‖f p‖^2 ∂volume.prod volume)=‖ψ‖^2 := by      rw [scalar_norm_sq_integral]      exact (bathFirst_preserving hN L).integral_comp        (by          cases N with          | zero => omega          | succ n =>            convert (MeasurableEquiv.piFinSuccAbove (fun _ : Fin (n+1) ↦ Torus L) 0).symm.measurableEmbedding.comp              (MeasurableEquiv.prodComm (α:=Configuration n L) (β:=Torus L)).measurableEmbedding using 1 <;> try rfl            funext p i            simp [insertFirst,MeasurableEquiv.piFinSuccAbove,MeasurableEquiv.prodComm])        (fun X ↦ ‖ψ X‖^2)    rw [hm,Measure.real,volume_torus,ENNReal.toReal_ofReal (by positivity : 0≤L.val^3)] at hbound    unfold occupation    change (L.val^3)⁻¹*(∫Y,‖∫x,f (Y,x)‖^2)≤‖ψ‖^2    calc      _ ≤ (L.val^3)⁻¹*(L.val^3*‖ψ‖^2) := mul_le_mul_of_nonneg_left hbound (by positivity)      _ = _ := by rw [←mul_assoc,inv_mul_cancel₀ (pow_ne_zero _ L.property.ne'),one_mul]  have map_ae {N : ℕ} (hN : 0<N) {L : Length} (ψ : ScalarL2 N L) : (map hN ψ : Configuration (N-1) L→ℂ)=ᵐ[volume] sliceIntegral hN ψ := by    unfold map    exact MemLp.coeFn_toLp _  have map_add {N : ℕ} (hN : 0<N) {L : Length} (f g : ScalarL2 N L) : map hN (f+g)=map hN f+map hN g := by    apply Lp.ext    have hp := (bathFirst_preserving hN L).quasiMeasurePreserving.tendsto_ae.eventually (Lp.coeFn_add f g)    have hs := Measure.ae_ae_of_ae_prod hp    filter_upwards [map_ae hN (f+g),map_ae hN f,map_ae hN g,Lp.coeFn_add (map hN f) (map hN g),hs,      memLp_slices (ground_slice_memLp hN f),memLp_slices (ground_slice_memLp hN g)] with Y hh hf hg hsum hY hfi hgi    rw [hh,hsum]    change sliceIntegral hN (f+g) Y=(map hN f) Y+(map hN g) Y    rw [hf,hg]    unfold sliceIntegral    rw [←smul_add,←integral_add (hfi.integrable (by norm_num)) (hgi.integrable (by norm_num))]    congr 1    apply integral_congr_ae    exact hY  have map_smul {N : ℕ} (hN : 0<N) {L : Length} (c : ℂ) (f : ScalarL2 N L) : map hN (c • f)=c • map hN f := by    apply Lp.ext    have hp := (bathFirst_preserving hN L).quasiMeasurePreserving.tendsto_ae.eventually (Lp.coeFn_smul c f)    have hs := Measure.ae_ae_of_ae_prod hp    filter_upwards [map_ae hN (c•f),map_ae hN f,Lp.coeFn_smul c (map hN f),hs] with Y hh hf hc hY    rw [hh,hc]    change sliceIntegral hN (c•f) Y=c • (map hN f) Y    rw [hf]    change (Real.sqrt (L.val^3))⁻¹ • (∫x : Torus L,(c•f) (insertFirst hN x Y))=      c • ((Real.sqrt (L.val^3))⁻¹ • ∫x : Torus L,f (insertFirst hN x Y))    rw [integral_congr_ae hY]    simp only [Pi.smul_apply]    rw [integral_smul]    exact smul_comm _ _ _  have map_norm_sq {N : ℕ} (hN : 0<N) {L : Length} (ψ : ScalarL2 N L) : ‖map hN ψ‖^2=occupation hN ψ := by    have hLp := L.property    rw [scalar_norm_sq_integral]    have hsi := integral_congr_ae ((map_ae hN ψ).fun_comp fun x ↦ ‖x‖^2)    simp only [Function.comp_def] at hsi    rw [hsi]    unfold sliceIntegral occupation    simp only [norm_smul,Real.norm_eq_abs,mul_pow,sq_abs,inv_pow,      integral_const_mul,Real.sq_sqrt (by positivity : 0≤L.val^3)]  have map_norm_le {N : ℕ} (hN : 0<N) {L : Length} (ψ : ScalarL2 N L) : ‖map hN ψ‖≤‖ψ‖ := by    have hh := (map_norm_sq hN ψ).trans_le (occupation_le_norm_sq hN ψ)    nlinarith [norm_nonneg (map hN ψ),norm_nonneg ψ]  exact ({ toFun := map hN, map_add' := map_add hN, map_smul' := map_smul hN } : ScalarL2 N L →ₗ[ℂ] ScalarL2 (N-1) L).mkContinuous 1 (fun ψ ↦ by    change ‖map hN ψ‖ ≤ 1 * ‖ψ‖    simpa only [one_mul] using map_norm_le hN ψ)end Orbitallocal instance groundScalarL2Complete (N : ℕ) (L : Length) : CompleteSpace (ScalarL2 N L) :=  inferInstancedef GroundSupported {N : ℕ} {L : Length} (a : ℝ)    (T : Density.Operator (ScalarL2 N L)) : Prop :=  ∀ψ∈T.toCLM.kerᗮ,‖ψ‖=1 →    ∃u : Jet N L,u.1=ψ ∧ IsGroundVector N L a udef mixedOccupation {N : ℕ} (hN : 0<N) {L : Length}    (T : Density.Operator (ScalarL2 N L)) : ℝ :=  T.compressionTrace (Orbital.continuous hN)theorem condensation_with_mixed :    ∃ε₀ c₀ : ℝ,0<ε₀ ∧ 0<c₀ ∧    ∀a ρ : ℝ,0<a → 0<ρ → ρ*a^3<ε₀ →    ∀(N : ℕ→ℕ) (L : ℕ→Length) (hN : ∀k,0<N k),      Tendsto N atTop atTop → Tendsto (fun k ↦ (L k).val) atTop atTop →      Tendsto (fun k ↦ (N k:ℝ)/(L k).val^3) atTop (𝓝 ρ) →      (∀Ψ : (k : ℕ)→Jet (N k) (L k),        (∀k,IsGroundVector (N k) (L k) a (Ψ k)) →        c₀≤liminf (fun k ↦ occupation (hN k) (Ψ k).1) atTop) ∧      (∀T : (k : ℕ)→Density.Operator (ScalarL2 (N k) (L k)),        (∀k,GroundSupported a (T k)) →        c₀≤liminf (fun k ↦ mixedOccupation (hN k) (T k)) atTop) := by  sorryend OAI.HardSphere
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.

Ground-state condensation in the dilute hard-sphere gas

Theorem (Condensation in every ground state)

There are absolute constants \varepsilon_0,c_0>0 with the following property. Fix a,\rho>0 satisfying \rho a^3<\varepsilon_0. For every sequence of particle numbers N_k and lengths L_k such that

N_k\longrightarrow\infty,\qquad L_k\longrightarrow\infty, \qquad \frac{N_k}{L_k^3}\longrightarrow\rho,

and every choice of normalized, possibly complex, bosonic ground eigenvectors \Psi_k of the hard-sphere Hamiltonians,

\liminf_{k\to\infty} B(\Psi_k)\ge c_0.
Section 1, Introduction Read it in the paper TeX source, line 48
Show the TeX
There are absolute constants $\varepsilon_0,c_0>0$ with the following
property. Fix $a,\rho>0$ satisfying $\rho a^3<\varepsilon_0$.
For every sequence of particle numbers $N_k$ and lengths $L_k$ such that
\[
 N_k\longrightarrow\infty,\qquad L_k\longrightarrow\infty,
 \qquad \frac{N_k}{L_k^3}\longrightarrow\rho,
\]
and every choice of normalized, possibly complex, bosonic ground
eigenvectors $\Psi_k$ of the hard-sphere Hamiltonians,
\begin{equation}
 \liminf_{k\to\infty} B(\Psi_k)\ge c_0.
\end{equation}
Corollary (Ground-space states)

Under the hypotheses of Theorem main:theorem, the same lower bound holds for every sequence of density operators supported on the bosonic ground eigenspaces. In particular, it holds for the normalized ground-space projections \Pi_k/\Tr\Pi_k, and for every sequence of normalized nonnegative ground functions.

Section 1, Introduction Read it in the paper TeX source, line 69
Show the TeX
Under the hypotheses of Theorem~\ref{main:theorem}, the same lower
bound holds for every sequence of density operators supported on the
bosonic ground eigenspaces. In particular, it holds for the normalized
ground-space projections $\Pi_k/\Tr\Pi_k$, and for every sequence of
normalized nonnegative ground functions.
Configuration and file facts
OpenAI’s Lean catalogue
OpenAI’s Lean catalogue does not list this as a main result; the release’s Lean notes for family 267 link it.
Solution module
OAI.Analysis.HardSphere.Main
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
31 local vocabulary declarations
Lines of Lean, without comments or blank lines
301
Second proof-verification program (nanoda)
Off in OpenAI's configuration.

Statement comparison

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

Plectis Atlas

Uniform ground-state condensation in the dilute hard-sphere gas

Family 267: Positive-temperature Bose–Einstein condensation and exact quantum depletion

Candidate pairing

Theorem (Condensation in every ground state)

There are absolute constants \varepsilon_0,c_0>0 with the following property. Fix a,\rho>0 satisfying \rho a^3<\varepsilon_0. For every sequence of particle numbers N_k and lengths L_k such that

N_k\longrightarrow\infty,\qquad L_k\longrightarrow\infty, \qquad \frac{N_k}{L_k^3}\longrightarrow\rho,

and every choice of normalized, possibly complex, bosonic ground eigenvectors \Psi_k of the hard-sphere Hamiltonians,

\liminf_{k\to\infty} B(\Psi_k)\ge c_0.

Ground-state condensation in the dilute hard-sphere gas

TeX label main:theorem, build/sections/introduction.tex, line 48

The Lean statement says

theorem condensation_with_mixed :    ∃ε₀ c₀ : ℝ,0<ε₀ ∧ 0<c₀ ∧    ∀a ρ : ℝ,0<a → 0<ρ → ρ*a^3<ε₀ →    ∀(N : ℕ→ℕ) (L : ℕ→Length) (hN : ∀k,0<N k),      Tendsto N atTop atTop → Tendsto (fun k ↦ (L k).val) atTop atTop →      Tendsto (fun k ↦ (N k:ℝ)/(L k).val^3) atTop (𝓝 ρ) →      (∀Ψ : (k : ℕ)→Jet (N k) (L k),        (∀k,IsGroundVector (N k) (L k) a (Ψ k)) →        c₀≤liminf (fun k ↦ occupation (hN k) (Ψ k).1) atTop) ∧      (∀T : (k : ℕ)→Density.Operator (ScalarL2 (N k) (L k)),        (∀k,GroundSupported a (T k)) →        c₀≤liminf (fun k ↦ mixedOccupation (hN k) (T k)) atTop) := 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.

Atlas selected this possible match because the two statements share words. No review of whether they mean the same thing is recorded.two independent groups report that Comparator accepted runs for this file at the release version shown here.Statement review: none recorded

31 local vocabulary declarationsAllowed axioms: propext, Quot.sound, Classical.choiceopenai/math at fd4aeebwcook04.github.io/plectis-atlas/statements/HardSphere.html

Recorded comparisons with the paper

Atlas records no contributed comparison of this statement with the paper.

Contributed Comparator run reports

Atlas records no contributed report of running Comparator for this statement file.

Questions to resolve when comparing this statement with the paper

  • Both independent readers find this family's challenges state less than its headline, while the atlas's AI draft classes this file as stating a paper's theorem as the paper does; check which part of the headline it covers.

Compare this statement with the paperShare a Comparator run reportSuggest a change