∑math20

Probability and statistical mechanics · Result 228

Continuum phase transitions for radial pair potentials

2 papersLean

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.

Watch

1

The problem

What is being asked, where it comes from, and why it is hard. No proof needed.

▶Introduction to the problemin preparation
2

The solution proposed by OpenAI

How the paper solves it, step by step.

Full explanation
▶The proposed solutionin preparation

Papers 2

First page of A continuum temperature singularity for a radial pair potential

A continuum temperature singularity for a radial pair potential

OpenAI · September 24, 2026

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.

Read PDF Download Source

Cite
@misc{OAI:A-continuum-temperature-singularity-for-a-radial-pair-potential-September-24-2026,
  author = {{OpenAI}},
  title = {{A continuum temperature singularity for a radial pair potential}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-continuum-temperature-singularity-for-a-radial-pair-potential-September-24-2026/paper.pdf}{OAI:A-continuum-temperature-singularity-for-a-radial-pair-potential-September-24-2026}},
  year = {2026}
}
First page of A radial continuum phase transition with algebraic decay

A radial continuum phase transition with algebraic decay

OpenAI · September 24, 2026

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.

Read PDF Download Source

Cite
@misc{OAI:A-radial-continuum-phase-transition-with-algebraic-decay-September-24-2026,
  author = {{OpenAI}},
  title = {{A radial continuum phase transition with algebraic decay}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-radial-continuum-phase-transition-with-algebraic-decay-September-24-2026/paper.pdf}{OAI:A-radial-continuum-phase-transition-with-algebraic-decay-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

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.

Comparator links

ResultComparator statement
Temperature singularity over a density intervalContinuumTransition.lean
Fixed-density radial continuum phase transitionRadialTransition.lean
A common radial phase transition over a density intervalRadialDensityInterval.lean

Scope note on GitHub →