Plectis Atlas
Search

↑ and ↓ move, Enter opens, Esc closes.

Show on the map

Continuum phase transitions for radial pair potentials

OpenAI groups related papers into a “family”. OpenAI’s catalogue describes this one:

Constructs stable distance-dependent pair interactions for three-dimensional classical particles with a first-order phase transition: the canonical free energy has a derivative jump at one inverse temperature throughout an open density interval. One potential has a divergent repulsive core; another is bounded and continuous with an integrable power-law tail, realizing the type of transition sought in Simon’s continuum problem. (OpenAI’s Lean note)

Lean is a language for mathematical statements and proofs that a computer can verify. The assessments below ask whether those statements express the result OpenAI describes here.

Both independent assessments find that the Lean statements express or imply the whole result described above. Read the assessments

What the papers state

Theorem 1.1

In A continuum temperature singularity for a radial pair potential

Possible match to OpenAI’s description, selected from the papers’ main statements because it shares the most wording. No review confirming the selection is recorded.

There exist an admissible radial difference-only pair potential \Phi(x)=\phi(|x|) on \R^3, a nonempty open interval I\subset(0,\infty), and one \beta_c\in(1/2,3/2) with the following properties. The potential satisfies \phi(r)=o(r^{-3}) as r\to\infty. The free-cube limit (1.3) exists and is finite for every \beta>0 and every density \rho>0. For every \rho\in I, the finite one-sided derivatives at the same critical point satisfy

D_\beta^- f_\Phi(\beta_c,\rho) >D_\beta^+ f_\Phi(\beta_c,\rho).

Thus one potential and one critical inverse temperature give a strict canonical temperature singularity throughout I.

Theorem 1.1

In A radial continuum phase transition with algebraic decay

The paper’s main theorem is shown as a possible match to OpenAI’s description. No review confirming the selection is recorded.

There is a bounded continuous function \phi:[0,\infty)\to\R and finite constants B,C>0 such that

\sum_{i<j}\phi(\abs{x_i-x_j})\ge-BN, \qquad \abs{\phi(r)}\le C r^{-3-1/32}\quad(r\ge1).

There are an open interval I\subset(0,\infty) centered at 5p/3 and a common inverse temperature \beta_c\in[7/8,9/8] such that, for every \rho\in I, the canonical free energy

f(\beta,\rho)= -\lim_{L\to\infty}\frac1{\beta L^3} \log Z^\phi_{L,\lfloor\rho L^3\rfloor}(\beta)

exists and is finite for every \beta>0. Its finite one-sided derivatives at \beta_c satisfy

f'_-(\beta_c,\rho)>f'_+(\beta_c,\rho).

In particular, f(\,\cdot\,,\rho) is not differentiable at \beta_c.

The release does not say which paper theorem its catalogue describes. Both statements above are shown whole, the closer match to the description’s wording first. The atlas has not reviewed either choice.

Reported proof verification
Three Lean statements in the release; independent groups report that Comparator accepted runs for all these files at the version shown here.
Papers and explanations
Two current papers, each readable here as a page beside its PDF.

Papers

Each paper opens as a reading page in the browser, with the PDF beside it. The statements each paper opens with are on its reading page.

A continuum temperature singularity for a radial pair potential

Undated, current edition.

Read it herePDF

We construct a stable radial pair potential in three dimensions whose canonical free energy has a strict downward derivative jump at one common finite positive inverse temperature throughout an open interval of positive densities. The potential has a divergent repulsive core, a nontrivial attractive interval, and an integrable tail satisfying \(\phi(r)=o(r^{-3})\). Its free-cube canonical free energy is finite at every positive inverse temperature and density.

A radial continuum phase transition with algebraic decay

Undated, current edition.

Read it herePDF

We construct a bounded, continuous, stable radial pair potential in three dimensions with \(|\phi(r)|\le Cr^{-3-1/32}\) for r ≥ 1. Throughout an open interval of positive densities, its canonical thermodynamic free energy is finite at every positive inverse temperature and has a strict downward derivative jump at one common finite positive inverse temperature.

Three Lean statements in this family

Choose one to see it beside the paper theorem it is paired with.

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

ContinuumTransition

The paper states

Theorem 1.1

In A continuum temperature singularity for a radial pair potential

There exist an admissible radial difference-only pair potential \Phi(x)=\phi(|x|) on \R^3, a nonempty open interval I\subset(0,\infty), and one \beta_c\in(1/2,3/2) with the following properties. The potential satisfies \phi(r)=o(r^{-3}) as r\to\infty. The free-cube limit (1.3) exists and is finite for every \beta>0 and every density \rho>0. For every \rho\in I, the finite one-sided derivatives at the same critical point satisfy

D_\beta^- f_\Phi(\beta_c,\rho) >D_\beta^+ f_\Phi(\beta_c,\rho).

Thus one potential and one critical inverse temperature give a strict canonical temperature singularity throughout I.

The words they share: 1/2, 3/2, radial, free, energy, admissible, nonempty, canonical, potential, cube, strict, singularity, derivatives, temperature, inverse, sided, interval, pair, one, density, finite, beta.

Possible Lean counterpart

Selected from shared wording. No review of whether the statements mean the same thing is recorded.

Temperature singularity over a density interval

ContinuumTransition.lean, the release lists it as a main result.

def MainStatement : Prop :=  ∃ (φ : ℝ → ℝ) (f : ℝ → ℝ → ℝ) (I : Set ℝ) (βc : ℝ),    Admissible φ ∧    Asymptotics.IsLittleO atTop φ (fun r : ℝ => r ^ (-3 : ℤ)) ∧    HasCanonicalFreeEnergy φ f ∧    IsOpen I ∧ OrdConnected I ∧ I.Nonempty ∧ I ⊆ Ioi 0 ∧    βc ∈ Ioo (1 / 2 : ℝ) (3 / 2 : ℝ) ∧    ∀ ρ ∈ I, ∃ dminus dplus : ℝ,      HasDerivWithinAt (fun β => f β ρ) dminus (Iic βc) βc ∧      HasDerivWithinAt (fun β => f β ρ) dplus (Ici βc) βc ∧      dplus < dminustheorem main_theorem : MainStatement := by  sorry

This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.

two independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet. Who ran the proof-verification program

  • cert-machine records it as “CERTIFIED”.
  • MathVet records it as “comparator-sandboxed-pass”.

Read the complete Lean statement

RadialDensityInterval

The paper states

Theorem 1.1

In A radial continuum phase transition with algebraic decay

There is a bounded continuous function \phi:[0,\infty)\to\R and finite constants B,C>0 such that

\sum_{i<j}\phi(\abs{x_i-x_j})\ge-BN, \qquad \abs{\phi(r)}\le C r^{-3-1/32}\quad(r\ge1).

There are an open interval I\subset(0,\infty) centered at 5p/3 and a common inverse temperature \beta_c\in[7/8,9/8] such that, for every \rho\in I, the canonical free energy

f(\beta,\rho)= -\lim_{L\to\infty}\frac1{\beta L^3} \log Z^\phi_{L,\lfloor\rho L^3\rfloor}(\beta)

exists and is finite for every \beta>0. Its finite one-sided derivatives at \beta_c satisfy

f'_-(\beta_c,\rho)>f'_+(\beta_c,\rho).

In particular, f(\,\cdot\,,\rho) is not differentiable at \beta_c.

The words they share: 5p/3, 7/8, 9/8, differentiable, 1/32, temperature, free, energy, continuous, interval, canonical, log, bounded, algebraic, decay, derivatives, inverse, phi, common, one, beta.

Possible Lean counterpart

Selected from shared wording. No review of whether the statements mean the same thing is recorded.

A common radial phase transition over a density interval

RadialDensityInterval.lean, the release lists it as a supporting statement.

theorem densityInterval :    ∃ (p : ℝ) (φ : Potential) (B C η βc : ℝ) (f : ℝ → ℝ → ℝ),      0 < p ∧ IsPackingDensity p ∧      IsBoundedPotential φ ∧ Continuous φ ∧      0 < B ∧ 0 < C ∧ StableWith φ B ∧ AlgebraicDecayWith φ C ∧      0 < η ∧ Ioo (5*p/3 - η) (5*p/3 + η) ⊆ Ioi 0 ∧      βc ∈ Icc (7/8:ℝ) (9/8) ∧      ∀ ρ ∈ Ioo (5*p/3 - η) (5*p/3 + η),        IsCanonicalFreeEnergy φ ρ (fun β => f β ρ) ∧        StrictTemperatureCorner (fun β => f β ρ) βc := by  sorry

This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.

two independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet. Who ran the proof-verification program

  • cert-machine records it as “CERTIFIED”.
  • MathVet records it as “comparator-sandboxed-pass”.

Read the complete Lean statement

RadialTransition

The paper states

Theorem 1.1

In A radial continuum phase transition with algebraic decay

There is a bounded continuous function \phi:[0,\infty)\to\R and finite constants B,C>0 such that

\sum_{i<j}\phi(\abs{x_i-x_j})\ge-BN, \qquad \abs{\phi(r)}\le C r^{-3-1/32}\quad(r\ge1).

There are an open interval I\subset(0,\infty) centered at 5p/3 and a common inverse temperature \beta_c\in[7/8,9/8] such that, for every \rho\in I, the canonical free energy

f(\beta,\rho)= -\lim_{L\to\infty}\frac1{\beta L^3} \log Z^\phi_{L,\lfloor\rho L^3\rfloor}(\beta)

exists and is finite for every \beta>0. Its finite one-sided derivatives at \beta_c satisfy

f'_-(\beta_c,\rho)>f'_+(\beta_c,\rho).

In particular, f(\,\cdot\,,\rho) is not differentiable at \beta_c.

The words they share: 5p/3, 7/8, 9/8, differentiable, 1/32, temperature, free, energy, continuous, canonical, log, bounded, algebraic, decay, derivatives, inverse.

Possible Lean counterpart

Selected from shared wording. No review of whether the statements mean the same thing is recorded.

Fixed-density radial continuum phase transition

RadialTransition.lean, the release lists it as a main result.

theorem main :    ∃ (p : ℝ) (φ : Potential) (B C : ℝ) (f : ℝ → ℝ) (βc : ℝ),      0 < p ∧ IsPackingDensity p ∧      IsBoundedPotential φ ∧ Continuous φ ∧      0 < B ∧ 0 < C ∧ StableWith φ B ∧ AlgebraicDecayWith φ C ∧      IsCanonicalFreeEnergy φ (5*p/3) f ∧      βc ∈ Icc (7/8:ℝ) (9/8) ∧ StrictTemperatureCorner f βc := by  sorry

This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.

two independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet. Who ran the proof-verification program

  • cert-machine records it as “CERTIFIED”.
  • MathVet records it as “comparator-sandboxed-pass”.

Read the complete Lean statement

Other mathematical statements in OpenAI’s Lean library

Atlas found these propositions by scanning the text of the project’s Model.lean file. Each name links to its definition, with any associated statement file beside it. This list does not record running Lean to interpret or verify those definitions.

Independent comparisons and proof-verification reports

Does the Lean express the advertised result?

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

MathVet and Carlos Toledo’s cert-machine independently assessed whether this family’s Lean statements express the whole result OpenAI describes in its catalogue. These are assessments of the family as a whole, not of each paper theorem separately.

MathVet finds that the Lean statements express or imply the whole advertised result (their term: “full”).

Their note: ContinuumTemperature.main_theorem : ∃ φ f I βc, Admissible φ ∧ φ = o(r^{-3}) ∧ HasCanonicalFreeEnergy φ f ∧ I open interval ⊆ (0,∞) ∧ βc ∈ (1/2, 3/2) ∧ ∀ ρ ∈ I, dplus < dminus (Admissible = stable, φ → +∞ at 0 (divergent core), integrable tail) and RadialTransition.densityInterval (bounded continuous φ, |φ r| ≤ C r^(-3-1/32), stable, a nonempty open density interval around 5p/3, common βc ∈ [7/8, 9/8], StrictTemperatureCorner); both potentials of the summary and the density-interval statement are covered.

Definitions the group asks readers to compare with the paper: Custom ‘free energy’: HasCanonicalFreeEnergy φ f := ∀ β ρ > 0, Tendsto (L^{-3} log Z(β, L, ⌊ρL^3⌋)) atTop (𝓝 (-β f β ρ)) / IsCanonicalFreeEnergy with explicit partition φ β L N := (N!)^{-1} ∫_{cube^N} exp(-β energy) and energy in EReal (⊤ at coincident points) for the first potential; standard thermodynamic-limit definitions, free boundary conditions.

“full”, in their words: The challenge statements imply the headline claim after unpacking definitions or one routine step.

Their method: 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.

Read the original assessment Read MathVet’s method

cert-machine finds that the Lean statements express or imply the whole advertised result (their term: “MATCHES”).

“MATCHES”, in their words: The challenge statements state the headline as OpenAI wrote it.

Their method: Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule.

Read the original assessment Read cert-machine’s method

OpenAI’s own note on what its Lean covers

The formalization constructs one stable radial pair potential in three-dimensional continuum space with a divergent repulsive core and an integrable tail that is $o(r^{-3})$. Its canonical free energy exists for every positive inverse temperature and density. At one inverse temperature $\beta_c\in(1/2,3/2)$, the free energy has a strict finite jump between its one-sided derivatives with respect to inverse temperature, for every density in one nonempty open interval.

The formalization constructs a bounded continuous stable radial pair potential in $\mathbb R^3$ satisfying $|\phi(r)|\le Cr^{-3-1/32}$ for $r\ge1$. There is a nonempty open interval of positive densities around $5p/3$, where $p$ is the unit-separated packing-density limit, on which the canonical free energy exists at every positive inverse temperature and has a strict downward derivative jump at one common $\beta_c\in[7/8,9/8]$. The earlier fixed-density statement at $5p/3$ is also retained. Both statements concern the derivative with respect to inverse temperature.

AI-drafted comparisons, with no recorded human review

  • Temperature singularity over a density interval ContinuumTransition

    Unreviewed AI draft: states a paper’s theorem as the paper does. States the main theorem: a stable radial potential in R³ with divergent core and o(r^{-3}) tail whose free energy has a derivative jump at one β_c for every density in an open interval.

  • A common radial phase transition over a density interval RadialDensityInterval

    Unreviewed AI draft: states a paper’s theorem as the paper does. States the main theorem of the algebraic-decay paper: a bounded continuous stable potential with |φ(r)| ≤ Cr^{-3-1/32} and a common derivative jump at β_c in [7/8, 9/8] for every density in an open interval around 5p/3.

  • Fixed-density radial continuum phase transition RadialTransition

    Unreviewed AI draft: states a weaker form of a paper’s theorem. States the earlier fixed-density statement at the single density 5p/3, whereas the main theorem gives a common transition temperature for every density in an open interval; the interval version is RadialDensityInterval.

Who ran the proof-verification program?

These groups report running Comparator with the release’s Lean statement files. For a configured theorem, it verifies OpenAI’s separate proof against the exact statement; some files instead configure definitions for comparison by name and type. Each row is the named group’s report. Atlas has not repeated the runs.

These reports do not list the software versions, proof-verification programs, axioms, time or memory in separate fields. Any such details in a report’s prose are reproduced below.

Temperature singularity over a density interval ContinuumTransition

Two reports, all at the release’s recorded version.

Reported byTheir wordTheir accountDateOriginal report
cert-machine“CERTIFIED”Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.10 October 2026Original report
MathVet“comparator-sandboxed-pass”Re-run through Comparator in a sandboxed virtual machine: accepted.8 October 2026Original report

A common radial phase transition over a density interval RadialDensityInterval

Two reports, all at the release’s recorded version.

Reported byTheir wordTheir accountDateOriginal report
cert-machine“CERTIFIED”Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.10 October 2026Original report
MathVet“comparator-sandboxed-pass”Re-run through Comparator in a sandboxed virtual machine: accepted.8 October 2026Original report

Fixed-density radial continuum phase transition RadialTransition

Two reports, all at the release’s recorded version.

Reported byTheir wordTheir accountDateOriginal report
cert-machine“CERTIFIED”Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.10 October 2026Original report
MathVet“comparator-sandboxed-pass”Re-run through Comparator in a sandboxed virtual machine: accepted.8 October 2026Original report

What these papers cite in the release, and what cites them

These links come from the papers’ bibliographies. A citation records that one paper cites another; how each cited result is used has not been examined here.

Within this family

Papers elsewhere in the release that this family’s papers cite

This family’s papers cite no paper elsewhere in the release.

Papers elsewhere in the release that cite this family’s papers

No paper elsewhere in the release cites this family’s papers.

References outside the release

Each paper’s outside references are listed with it on its reading page, where each citation is placed. Every outside work cited in the release: References outside the release

Explain a result, compare statements or propose a correction

Atlas has no contributed explanation for this family yet. You can offer one with a GitHub account. You receive named credit and disclose any AI assistance.

Each button opens a GitHub form with this page and its source version filled in. Opening the form does not reserve the work.

Offer to write an explanationCompare one Lean statement with its paper: ContinuumTransition, RadialTransition, RadialDensityIntervalSuggest a source attributionSuggest a change

What people have said

Commentary on this family by others, dated and credited. It is commentary, not a finding.

  • An unsigned public tier list, the OpenAI Math Tier List, classes it as a construction and rates its significance, if it holds up, as “Solid publication, could lead to tenure”. The page says that nothing on it is verified.

    Author not stated. Source

Questions awaiting review

Each item identifies a statement, definition or report that needs further review. Its link opens a GitHub form with the source version already recorded.

Read the Lean statement against the paper

  • An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded. Open the form
  • An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded. Open the form
  • An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded. Open the form

Identify the theorem the catalogue describes

  • Family 228 The theorem shown was selected from shared wording with OpenAI’s description. Atlas records no review confirming that it is the theorem the description means. Open the form

Address a question raised in an independent assessment

Compare the proposed paper and Lean matches

  • Family 228 Atlas records no review of whether each linked Lean statement and paper theorem mean the same thing. Open the form