All missions

Motivation

At its critical weight, a self-avoiding path on the honeycomb lattice can make long excursions without paying an exponential cost. A basic quantitative question is how much of its total weight reaches the far side of a strip of height $N$. Physics heuristics (Nienhuis's Coulomb gas and the conjectured $\mathrm{SLE}_{8/3}$ scaling limit with boundary exponent $5/8$) predict that this crossing mass decays like $N^{-1/4}$. Rigorous results so far showed only that it tends to zero, with a polynomial upper bound with a tiny exponent.

The OpenAI preprint behind this mission, dated September 26, 2026 (source), claims the predicted power with bounded-factor constants: the crossing mass is comparable to $N^{-1/4}$, and the first horizontal-displacement moment of paths returning to the starting side is comparable to $N^{3/4}$ (Theorem 1.1, p. 2). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

• 1982 — Nienhuis's Coulomb-gas analysis of the dilute $O(n)$ model predicts the honeycomb critical point $\sqrt{2+\sqrt2}$ and the planar self-avoiding-walk exponents, including $\nu=3/4$ (PRL 1982).
• 2004 — Lawler, Schramm and Werner describe the conjectural $\mathrm{SLE}_{8/3}$ scaling limit; the boundary exponent $5/8$ predicts a crossing power $-1/4$ for strips.
• 2012 — Duminil-Copin and Smirnov prove that the connective constant of the honeycomb lattice is $\sqrt{2+\sqrt2}$ using a parafermionic observable and a boundary identity (Annals 2012); their strip argument bounds the crossing mass between orders $1/N$ and $1$.
• 2014 — Beaton, Bousquet-Mélou, de Gier, Duminil-Copin and Guttmann prove that the critical bridge mass tends to zero (CMP 2014).
• 2020 — Glazman and Manolescu give a shorter proof and a quantitative bound along a subsequence of heights (AIHP 2020).
• 2026 — Krachun and Panagiotis prove a polynomial upper bound on the bridge mass and quantitative sub-ballisticity (Ann. Probab. 2026).
• September 2026 — A group of OpenAI preprints claims the strip crossing power $-1/4$ with bounded-factor constants (source), the bridge mean-length exponent $4/3$ (source), and spatial exponent $3/4$ for several laws of critical walks (source).

Setting

Use the honeycomb lattice dual to the equilateral triangular tiling of side one, with one edge direction horizontal; its vertices are the triangles up i j and down i j, where $j\ge0$ indexes the horizontal band. Let $S_N$ be the strip of $N$ bands. A path starts in the triangle up 0 0 (just above bottom port $0$), visits distinct triangles, moves between adjacent ones, and stays in bands $0,\dots,N-1$. Its length $|\gamma|$ is the number of visited triangles and its critical weight is $\rho^{|\gamma|}$ with $\rho=(2+\sqrt2)^{-1/2}$. An arch ends at up k 0 with $k\neq0$ (bottom port $k$); a bridge ends at a down triangle of the top band. Put $c=\cos(3\pi/8)$ and

$$K_N(k)=\sum_{\text{arches to }k}\rho^{|\gamma|},\quad A_N=\sum_{k\ne0}K_N(k),\quad B_N=\sum_{\text{bridges}}\rho^{|\gamma|},\quad m_N=\sum_{k\ge1}k\,K_N(k).$$

Write $f_N\asymp g_N$ if $\ell g_N\le f_N\le u g_N$ for all $N\ge1$ with fixed constants $\ell,u>0$.

Formalization targets

Goal: Theorem 1.1 (Critical strip mass, p. 2)

For every $N\ge1$ all sums above are finite, and with constants independent of $N$,

$$cA_N+B_N=1,\qquad m_{N+1}-m_N\asymp B_N,\qquad m_N\asymp N^{3/4},\qquad B_N\asymp N^{-1/4},$$

and $B_N$ is nonincreasing in $N$.

Significance

The result itself. It establishes the predicted crossing power $-1/4$ with uniform multiplicative constants, not just a logarithmic exponent, improving the qualitative decay of Beaton et al. and the polynomial upper bound of Krachun and Panagiotis. It is an input for the bridge-length and spatial-exponent results of companion preprints. The exponent of $m_N$ concerns an unnormalized displacement moment summed over all lengths; the fixed-length displacement conjecture and the scaling limit are different questions.

Formalizing it. The proof combines an exact boundary identity of Duminil-Copin–Smirnov type, finite-strip transfer matrices with integrable local relations, a Pfaffian that makes the stationary vector polynomial, and a comparison of the resulting positive integral with Bures–Laguerre ensembles. A formal proof would include the honeycomb boundary identity, the core of the connective-constant proof, which is itself a natural formalization target. No machine-checked honeycomb walk result of this kind is known.

Difficulty

The boundary identity $cA_N+B_N=1$ (Lemma 4.2, p. 15) does not determine the power: it only gives $B_N$ between orders $1/N$ and $1$. The preprint's route computes the arch moment $m_N$ first, as one coefficient of a ratio $p_{N+1}/p_N$ of Pfaffians (Proposition 4.1, p. 13), converts it into a positive $N$-fold integral with Bures-type interaction (Section 5), and estimates that integral uniformly in $N$ by comparison with Laguerre laws (Section 6). The crossing power then follows from monotonicity and $m_{N+1}-m_N\asymp B_N$. A degree bound on the polynomial vacuum (Lemma 3.2, p. 10) is essential, because it turns interpolation into an identity argument.

Formalization scope

• Triangles are ℤ × ℕ × Bool (column, band, up/down); adjacency joins an up triangle to the down triangles sharing an edge. Paths are Lists with Nodup, IsChain adjacent, head up 0 0, a prescribed last triangle, and all bands < N.
• Weights are rho ^ p.length on paths satisfying IsPath, and 0 otherwise; all masses are tsums over lists. The goal includes summability of each family, so the tsums are genuine sums.
• moment N = ∑' k : ℕ, (k+1) * K N (k+1), i.e. $\sum_{k\ge1}kK_N(k)$.
• Comparable f g asks for constants $0<\ell,u$ with $\ell g(N)\le f(N)\le ug(N)$ for every $N\ge1$; powers are real rpow.
• Monotonicity is $B_{N+1}\le B_N$ for $N\ge1$.

Reusable contributions: the honeycomb boundary (parafermionic) identity in finite domains, and summability of critical walk weights in strips.

Selected references

• OpenAI, Critical strip-crossing mass on the honeycomb lattice, OpenAI Math Release preprint, September 26, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Critical-strip-crossing-mass-on-the-honeycomb-lattice-September-26-2026/main.pdf
• G. F. Lawler, O. Schramm, W. Werner, On the scaling limit of planar self-avoiding walk, Proc. Sympos. Pure Math. 72, Part 2 (2004), 339–364.
• Y. Ikhlef, J. Cardy, Discretely holomorphic parafermions and integrable loop models, J. Phys. A 42 (2009), 102001. https://doi.org/10.1088/1751-8113/42/10/102001
• A. Glazman, Connective constant for a weighted self-avoiding walk on $\mathbb Z^2$, Electron. Commun. Probab. 20 (2015), paper 86. https://doi.org/10.1214/ECP.v20-3844
• B. Nienhuis, Exact critical point and critical exponents of O(n) models in two dimensions, Phys. Rev. Lett. 49 (1982), 1062–1065. https://doi.org/10.1103/PhysRevLett.49.1062
• H. Duminil-Copin, S. Smirnov, The connective constant of the honeycomb lattice equals $\sqrt{2+\sqrt2}$, Ann. of Math. 175 (2012), 1653–1665. https://doi.org/10.4007/annals.2012.175.3.14
• N. R. Beaton, M. Bousquet-Mélou, J. de Gier, H. Duminil-Copin, A. J. Guttmann, The critical fugacity for surface adsorption of self-avoiding walks on the honeycomb lattice is $1+\sqrt2$, Comm. Math. Phys. 326 (2014). https://doi.org/10.1007/s00220-014-1896-1
• A. Glazman, I. Manolescu, Self-avoiding walk on $\mathbb Z^2$ with Yang–Baxter weights: universality of critical fugacity and 2-point function, Ann. Inst. H. Poincaré Probab. Statist. 56 (2020). https://doi.org/10.1214/19-AIHP1024
• D. Krachun, C. Panagiotis, Quantitative sub-ballisticity of self-avoiding walk on the hexagonal lattice, Ann. Probab. 54 (2026), 1109–1125. https://doi.org/10.1214/24-AOP1730

Motivation

Random 3-SAT, a conjunction of random three-literal clauses on $n$ variables, is the classic test case for the typical behavior of satisfiability. Experiments placed the hardest instances near the density where half the formulas are satisfiable, and statistical physics predicts a sharp satisfiability threshold near $4.267$. Once a limiting threshold $\alpha_3$ is known to exist, a natural question is whether it is a computable real: is there an algorithm that, given $r$, outputs a rational within $2^{-r}$ of $\alpha_3$? Existence alone does not imply this, since limits of computable sequences need not be computable (Specker 1949). This mission asks for such an algorithm.

Timeline

• 1949. Specker constructs a bounded monotone computable sequence of rationals with a noncomputable limit.
• 1999. Friedgut, with an appendix by Bourgain, proves a sharp transition about a size-dependent location (doi:10.1090/S0894-0347-99-00305-7).
• 2003, 2006. Hajiaghayi and Sorkin, and Kaporis, Kirousis and Lalas, prove the lower bound $3.52$ (arXiv:math/0310193).
• 2002–2006. Mézard, Parisi and Zecchina develop the cavity/survey-propagation picture; Mertens, Mézard and Zecchina predict $\alpha_3\approx4.267$.
• 2009. Díaz, Kirousis, Mitsche and Pérez-Giménez prove the upper bound $4.4898$.
• 2013. Bayati, Gamarnik and Tetali prove limits for normalized optimization values via sparse interpolation (doi:10.1214/12-AOP816).
• 2022. Ding, Sly and Sun prove the satisfiability conjecture with the predicted value for all large $k$ (doi:10.4007/annals.2022.196.1.1).
• 2026. Carenini proves a polynomial scaling window and the existence of limiting thresholds for every fixed $k\ge3$ (ECCC TR26-229, made public October 5, 2026); priority for the satisfiability conjecture belongs to Carenini.

The source of this mission is an OpenAI preprint dated September 27, 2026. Its contribution is computability of $\alpha_3$, beyond existence.

Setting

For $n\ge3$, a proper random 3-clause chooses three distinct variables uniformly from $x_1,\dots,x_n$ and gives each an independent fair sign. Let $\Phi(n,m)$ be the conjunction of $m\ge0$ independent such clauses (sampled with replacement from the $8\binom n3$ possibilities; the empty formula is satisfiable) and

$$p(n,m)=\mathbb P\{\Phi(n,m)\ \text{is satisfiable}\}.$$

A real $\alpha$ is computable if a single algorithm, on input $r$, halts with a rational $q_r$ satisfying $|q_r-\alpha|\le2^{-r}$.

Formalization targets

Goal: Theorem 1.1

There is $\alpha_3\in(0,\infty)$ such that for every fixed real $a\ge0$

$$\lim_{n\to\infty}p(n,\lfloor an\rfloor)=\begin{cases}1,&a<\alpha_3,\\0,&a>\alpha_3,\end{cases}$$

and one finite deterministic Turing machine, on input $1^r$, halts with a rational $q_r$ with $|q_r-\alpha_3|\le2^{-r}$, using no oracle, advice, or noncomputable constant. Lean: OAI.FixedClauseThreshold.Computability.main, open on the platform.

Significance

The theorem makes the random 3-SAT threshold an effectively approximable constant: in principle its digits can be certified, although no efficiency bound is obtained. The method produces two families of finite certificates, rational lower bounds from a deletion estimate and rational upper bounds from finite hierarchical approximations of a soft pressure, and a fair search over them halts without any computable rate of finite-size convergence. The paper also gives a self-contained existence proof of $\alpha_3$ (Theorem 4.4) for the same proper-clause model.

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists.

Difficulty

Finite-size satisfiability probabilities are computable, but their convergence rate is unknown, so truncating at a finite $n$ certifies nothing. Lower certificates need an explicit bound on how far the finite-size centers can lie above the limit. Upper certificates are harder: one must show that above $\alpha_3$ some finite, checkable object witnesses unsatisfiability in the limit. This requires a variational (Parisi-type) description of the limiting pressure of the soft constraint model, approximated by finitely many rational parameters with a proof that the approximation is complete at every rational density above the threshold.

Formalization scope

• ProperClause n k is Fin n → Option Bool with exactly $k$ defined entries; Formula n k m := Fin m → ProperClause n k; properSATProbability n 3 m is the exact counting ratio, equal to $p(n,m)$.
• MainStatement asserts $\exists\,\alpha>0$ with the two strict-side limits at $m=\lfloor an\rfloor$, a sequence q : ℕ → ℚ with Computable (fun r => encode (q r)), a Nat.Partrec.Code c with c.eval r = some (encode (q r)), and $|q_r-\alpha|\le2^{-r}$ for all $r$.
• The input is a natural number rather than a unary string, which is equivalent for computability; the $r=0$ case is a harmless extra requirement.
• Nothing is asserted at $a=\alpha_3$.

Infrastructure: Mathlib's Computable/Nat.Partrec.Code, finite counting for random formulas, Poisson clause processes, interpolation bounds, and Ruelle cascades for the upper certificates. Formalizations of Lemma 2.1 (finite-certificate search, purely computability-theoretic and reusable), Theorem 4.4 and Theorem 8.4 are welcome.

Selected references

• OpenAI, Computing the Random 3-SAT Threshold, preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Computing-the-Random-3-SAT-Threshold-September-27-2026/article.pdf
• OpenAI, A Limiting Satisfiability Threshold for Every Fixed Clause Size, preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Limiting-Satisfiability-Threshold-for-Every-Fixed-Clause-Size-September-25-2026/article.pdf
• G. Carenini, A polynomial scaling window for random k-SAT and a proof of the satisfiability conjecture, ECCC TR26-229, 2026. https://eccc.weizmann.ac.il/report/2026/229/
• E. Friedgut (appendix by J. Bourgain), Sharp thresholds of graph properties, and the k-SAT problem, J. Amer. Math. Soc., 1999. https://doi.org/10.1090/S0894-0347-99-00305-7
• J. Ding, A. Sly, N. Sun, Proof of the satisfiability conjecture for large k, Ann. of Math., 2022. https://doi.org/10.4007/annals.2022.196.1.1
• M. Bayati, D. Gamarnik, P. Tetali, Combinatorial approach to the interpolation method and scaling limits in sparse random graphs, Ann. Probab., 2013. https://doi.org/10.1214/12-AOP816
• M. Hajiaghayi, G. B. Sorkin, The satisfiability threshold of random 3-SAT is at least 3.52, preprint, 2003. https://arxiv.org/abs/math/0310193
• D. Panchenko, The Parisi ultrametricity conjecture, Ann. of Math., 2013. https://doi.org/10.4007/annals.2013.177.1.8
• E. Specker, Nicht konstruktiv beweisbare Sätze der Analysis, J. Symbolic Logic, 1949.

Motivation

Add random clauses one at a time to a Boolean formula on $n$ variables until it first becomes unsatisfiable. The index $H_n$ of that first failure is the satisfiability hitting time of random $k$-SAT. Its mean, divided by $n$, converges to the satisfiability threshold; its variance measures the width of the transition window. Friedgut's sharp-threshold theorem shows the window is $o(n)$, but quantitative widths have remained far from the $\sqrt n$ scale suggested by lower bounds. This mission asks for the order of the variance of $H_n$ for every fixed $k\ge3$.

Timeline

• 1981. Efron and Stein prove their variance inequality, the basic tool for fluctuation bounds of functions of independent inputs (doi:10.1214/aos/1176345462).
• 1999. Friedgut, with an appendix by Bourgain, proves a sharp threshold sequence for each fixed $k$ (doi:10.1090/S0894-0347-99-00305-7).
• 2002. Wilson proves an $\Omega_k(\sqrt n)$ separation of central quantiles for the proper-clause model (doi:10.1002/rsa.10050).
• 2005. Boucheron, Bousquet, Lugosi and Massart give moment inequalities for functions of independent variables (doi:10.1214/009117904000000856).
• 2022. Ding, Sly and Sun prove the satisfiability conjecture for large $k$ (doi:10.4007/annals.2022.196.1.1).
• 2026. Carenini proves an $O_{k,\eta}(n/\log n)$ window (ECCC TR26-145, arXiv:2609.26222) and then a polynomial window $O_{k,\eta}(n^{1/2+1/k})$ with variance $O_k(n^{1+2/k})$, resolving the satisfiability conjecture for every fixed $k\ge3$ (ECCC TR26-229, made public October 5, 2026); priority for that resolution belongs to Carenini. A companion OpenAI preprint gives an alternative proof of the limiting threshold.

The source of this mission is an OpenAI preprint dated September 27, 2026.

Setting

Fix $k\ge3$ and $n\ge k$. A proper $k$-clause is an OR of literals on $k$ distinct variables; let $C_1,C_2,\dots$ be independent uniform choices among the $2^k\binom nk$ signed proper clauses (signs fair, whole clauses may repeat). Put

$$F_m=C_1\wedge\dots\wedge C_m,\qquad F_0=\text{true},\qquad H_n=\min\{m\ge1:\ F_m\ \text{unsatisfiable}\},$$

and, for fixed $B>0$, the capped hitting time $T_{n,B}=\min\{H_n,\lfloor Bn\rfloor\}$. Since each assignment survives a clause with probability $1-2^{-k}$, $H_n$ is a.s. finite with all moments. Write

$$\ell_k(n)=\begin{cases}\log(en),&k=3,\\1,&k\ge4,\end{cases}\qquad U_k=\frac{\log2}{-\log(1-2^{-k})}.$$

Formalization targets

Goal: Theorem 1.1

There are constants $C_k,c_k>0$ with

$$\operatorname{Var}(H_n)\le C_k\,n\,\ell_k(n)\quad(n\ge k),\qquad \operatorname{Var}(H_n)\ge c_kn\quad(n\ \text{large}),$$

and for every fixed $B>0$ a constant $C_{k,B}$ with $\operatorname{Var}(T_{n,B})\le C_{k,B}\,n\,\ell_k(n)$; if $B>U_k$ then also $\operatorname{Var}(T_{n,B})\ge c_kn$ for large $n$. Hence $\operatorname{Var}(H_n)=\Theta_k(n)$ for $k\ge4$. Lean: OAI.RandomKSAT.variance_main, open on the platform.

Milestone: Propositions A.1–A.2 (optimality of exponents)

The killing-probability exponent $\beta=k/(k-1)$ in the lifetime bound $\tau_k(S)q_d(S)^\beta\le C_kd^\beta$ (Proposition 2.3) cannot be decreased, and the block-error term $g^{-(k-1)}$ in the replacement lemma cannot be improved to $o(g^{-(k-1)})$ uniformly. Lean: OAI.RandomKSAT.sharpness.

Significance

For $k\ge4$ the theorem determines the variance of the hitting time up to constants, so the transition window has width $\Theta_k(\sqrt n)$ in the variance sense, matching Wilson's lower bound and improving Carenini's $O_k(n^{1+2/k})$ variance bound. For $k=3$ it leaves only a logarithmic gap, closed in a companion OpenAI preprint. Chebyshev's inequality then gives concentration of $H_n$ about $\mathbb EH_n$ at scale $\sqrt{n\ell_k(n)}$.

The results are proved in an OpenAI preprint; they have not been peer reviewed, and no machine-checked proof exists.

Difficulty

The Efron–Stein inequality reduces the upper bound to the expected squared delay caused by deleting one clause, which counts pairs of prefixes at which that clause is pivotal. Controlling this occupation time requires a uniform estimate relating how quickly a set of assignments is killed by shorter $(k-1)$-clauses to its lifetime under $k$-clauses, valid for every assignment set with no lower cutoff. Earlier arguments truncate the number of clauses incident to the deleted clause's variables at a logarithmic level, which costs a logarithm; keeping that number as a random parameter without destroying independence is the main obstacle. Appendix A shows the relevant exponents are sharp.

Formalization scope

• Clause n k is a dependent pair of a $k$-element Finset (Fin n) and a sign vector on it; clauseLaw is uniform; streamLaw is the infinite product (Measure.infinitePi).
• firstFailure ω is the least $m$ with an unsatisfiable prefix, valued in ℕ∞; H = (firstFailure ω).toNat; T B ω = (min (firstFailure ω) ⌊Bn⌋).toNat. The infinite case has probability zero.
• variance is ProbabilityTheory.variance under streamLaw n k; ell, U are as displayed.
• In the milestone, blockKill u s S g is the probability that $g$ independent proper $s$-clauses kill $S$, and lifetime u k S $=\sum_m\mathbb P(S\text{ survives }m\text{ clauses})$ is $\tau_k(S)$.

Infrastructure: product measures on clause streams, Efron–Stein, conditioning on incidence patterns. Formalizations of Proposition 2.3 (lifetime from shorter-clause killing), Proposition 4.3 (conditional squared delay), Corollary 5.2 and Proposition 6.2 (linear variance lower bound) are welcome.

Selected references

• OpenAI, Variance of the Random k-SAT Hitting Time, preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Variance-of-the-Random-k-SAT-Hitting-Time-September-27-2026/article.pdf
• OpenAI, A Limiting Satisfiability Threshold for Every Fixed Clause Size, preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Limiting-Satisfiability-Threshold-for-Every-Fixed-Clause-Size-September-25-2026/article.pdf
• G. Carenini, A polynomial scaling window for random k-SAT and a proof of the satisfiability conjecture, ECCC TR26-229, 2026. https://eccc.weizmann.ac.il/report/2026/229/
• G. Carenini, The scaling window of random k-SAT, ECCC TR26-145, 2026. https://arxiv.org/abs/2609.26222
• E. Friedgut (appendix by J. Bourgain), Sharp thresholds of graph properties, and the k-SAT problem, J. Amer. Math. Soc., 1999. https://doi.org/10.1090/S0894-0347-99-00305-7
• D. B. Wilson, On the critical exponents of random k-SAT, Random Structures Algorithms, 2002. https://doi.org/10.1002/rsa.10050
• J. Ding, A. Sly, N. Sun, Proof of the satisfiability conjecture for large k, Ann. of Math., 2022. https://doi.org/10.4007/annals.2022.196.1.1
• B. Efron, C. Stein, The jackknife estimate of variance, Ann. Statist., 1981. https://doi.org/10.1214/aos/1176345462
• S. Boucheron, O. Bousquet, G. Lugosi, P. Massart, Moment inequalities for functions of independent random variables, Ann. Probab., 2005. https://doi.org/10.1214/009117904000000856

Motivation

A random $k$-SAT formula on $n$ Boolean variables is a conjunction of $m$ independent random clauses, each an OR of $k$ literals on distinct variables. As the clause density $m/n$ grows, the formula changes from almost surely satisfiable to almost surely unsatisfiable. Random $k$-SAT is a central model in probabilistic combinatorics, the theory of algorithms and statistical physics: its threshold is where hard instances are expected to concentrate, and it is a proving ground for methods from spin-glass theory. The satisfiability conjecture, formulated explicitly by Chvátal and Reed, asserts that for each fixed $k$ the transition happens at a limiting density $\alpha_k$ that does not drift with $n$.

Timeline

• 1992. Chvátal and Reed settle $k=2$ and formulate the conjecture for every fixed clause size (doi:10.1109/SFCS.1992.267789); Goerdt gives an independent proof for $k=2$ (doi:10.1006/jcss.1996.0081).
• 1999. Friedgut, with an appendix by Bourgain, proves a sharp transition around a sequence of densities, leaving open whether the sequence converges (doi:10.1090/S0894-0347-99-00305-7).
• 2002, 2006. Mézard, Parisi and Zecchina, and Mertens, Mézard and Zecchina, predict threshold values via the cavity method (doi:10.1126/science.1073287, doi:10.1002/rsa.20090).
• 2004. Achlioptas and Peres prove bounds $2^k\log2-O(k)$ (doi:10.1090/S0894-0347-04-00464-3).
• 2013, 2014. Bayati, Gamarnik and Tetali develop combinatorial interpolation for sparse random structures (doi:10.1214/12-AOP816); Abbe and Montanari study concentration of solution counts (doi:10.1002/rsa.20501).
• 2016. Coja-Oghlan and Panagiotou locate the threshold sequence within $o_k(1)$ of $2^k\log2-(1+\log2)/2$ (doi:10.1016/j.aim.2015.11.007).
• 2022. Ding, Sly and Sun prove the conjecture for all sufficiently large $k$, with the 1RSB value (doi:10.4007/annals.2022.196.1.1).
• 2026. Carenini proves a polynomial scaling window and resolves the conjecture for every fixed $k\ge3$ (ECCC TR26-229, made public October 5, 2026; https://eccc.weizmann.ac.il/report/2026/229/). Priority for the resolution belongs to Carenini.

The source of this mission is an OpenAI preprint dated September 25, 2026, which gives an alternative proof of the existence of the limiting threshold.

Setting

Fix $k\ge3$. For $n\ge k$, a proper $k$-clause chooses $k$ distinct variables among $x_1,\dots,x_n$ uniformly and gives each an independent fair sign, so each of the $2^k\binom nk$ clauses is equally likely. Let $C_1,C_2,\dots$ be independent such clauses (sampled with replacement: two positions may hold the same clause) and

$$F_{n,m}=\bigwedge_{i=1}^mC_i,\qquad P_n(m)=\mathbb P(F_{n,m}\ \text{is satisfiable}),\qquad P_n(0)=1 .$$

The ratio $c=m/n$ is the clause density.

Formalization targets

Goal: Theorem 1.1

For every fixed integer $k\ge3$ there is $\alpha_k\in(0,\infty)$ such that

$$\lim_{n\to\infty}P_n(\lfloor cn\rfloor)=\begin{cases}1,&0\le c<\alpha_k,\\ 0,&c>\alpha_k.\end{cases}$$

No assertion is made at $c=\alpha_k$, and the value of $\alpha_k$ is not identified. Lean: OAI.FixedClauseThreshold.main, open on the platform.

Significance

The theorem settles, for every fixed $k\ge3$, the existence half of the threshold question: Friedgut's sharp transition happens at a location that converges. Previously this was known only for large $k$ (Ding–Sly–Sun) and for $k=2$. Existence is a prerequisite for questions about the value of $\alpha_k$, its computability, and the fluctuations of the satisfiability hitting time, which companion OpenAI preprints address. The proof here proceeds through concentration of a capped last satisfiable index and a comparison between system sizes; it does not rely on Carenini's window.

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists.

Difficulty

A sharp-threshold theorem gives a narrow window at each $n$ but no control of how the window's center moves with $n$. Convergence needs a comparison between different system sizes, and interpolation methods from spin-glass theory deliver free-energy bounds, not hard satisfiability statements, and often only for even arity. The center must also be shown to concentrate polynomially, which requires bounding how many variables are forced along the clause process.

Formalization scope

• ProperClause n k is a function Fin n → Option Bool with exactly $k$ defined entries; some b at $i$ is the literal satisfied when $\sigma_i=b$.
• Formula n k m := Fin m → ProperClause n k (ordered, with replacement); properSATProbability n k m is the exact ratio of satisfiable formulas to all formulas, which equals $P_n(m)$ under the uniform product law.
• Degenerate sizes: $m=0$ gives probability $1$; for $n<k$ and $m>0$ the ensemble is empty and the ratio is $0$ by convention, affecting only finitely many $n$.
• HasLimitingThreshold k asserts $\exists\,\alpha>0$ with limits $1$ for $0\le c<\alpha$ and $0$ for $c>\alpha$ at $m=\lfloor cn\rfloor$.

Infrastructure: finite counting of formulas, Efron–Stein-type variance bounds, a deterministic concentration-to-convergence lemma (Theorem 5.1), and the Poisson/interpolation comparison with the transfer back to proper clauses. Formalizations of Proposition 2.2 (integrated forcing), Proposition 3.3 (polynomial concentration) and Theorem 5.1 are welcome.

Selected references

• OpenAI, A Limiting Satisfiability Threshold for Every Fixed Clause Size, preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Limiting-Satisfiability-Threshold-for-Every-Fixed-Clause-Size-September-25-2026/article.pdf
• G. Carenini, A polynomial scaling window for random k-SAT and a proof of the satisfiability conjecture, ECCC TR26-229, 2026. https://eccc.weizmann.ac.il/report/2026/229/
• V. Chvátal, B. Reed, Mick gets some (the odds are on his side), FOCS 1992. https://doi.org/10.1109/SFCS.1992.267789
• E. Friedgut (appendix by J. Bourgain), Sharp thresholds of graph properties, and the k-SAT problem, J. Amer. Math. Soc., 1999. https://doi.org/10.1090/S0894-0347-99-00305-7
• D. Achlioptas, Y. Peres, The threshold for random k-SAT is $2^k\log2-O(k)$, J. Amer. Math. Soc., 2004. https://doi.org/10.1090/S0894-0347-04-00464-3
• A. Coja-Oghlan, K. Panagiotou, The asymptotic k-SAT threshold, Adv. Math., 2016. https://doi.org/10.1016/j.aim.2015.11.007
• J. Ding, A. Sly, N. Sun, Proof of the satisfiability conjecture for large k, Ann. of Math., 2022. https://doi.org/10.4007/annals.2022.196.1.1
• M. Bayati, D. Gamarnik, P. Tetali, Combinatorial approach to the interpolation method and scaling limits in sparse random graphs, Ann. Probab., 2013. https://doi.org/10.1214/12-AOP816
• E. Abbe, A. Montanari, On the concentration of the number of solutions of random satisfiability formulas, Random Structures Algorithms, 2014. https://doi.org/10.1002/rsa.20501

Motivation

A uniform spanning tree of a finite connected graph is a spanning tree chosen uniformly at random. On an infinite graph one takes limits along finite pieces: the free uniform spanning forest (FUSF) is the weak limit of uniform spanning trees of an increasing sequence of finite connected subgraphs, with no boundary identification. Uniform spanning forests connect random walks, electrical networks, determinantal processes and $\ell^2$-Betti numbers of groups.

A random object on a graph is a factor of IID if it can be produced by one measurable rule from independent uniform labels on the vertices, in a way that commutes with all graph symmetries. Such representations are the measure-theoretic analogue of local algorithms, and they are central in ergodic theory of group actions. Whether the FUSF is a factor of IID was raised by Lyons at Oberwolfach in 2013, and Timár's 2025 paper describes the unrestricted question as open.

Timeline

• 1991. Pemantle constructs infinite-volume uniform spanning trees on $\mathbb Z^d$ (Ann. Probab., 1991; arXiv:math/0404043).
• 2001. Benjamini, Lyons, Peres and Schramm develop the general theory of free and wired uniform spanning forests; on transient graphs the wired forest is a factor of IID via Wilson's algorithm rooted at infinity (doi:10.1214/aop/1008956321).
• 2003. Lyons develops determinantal probability measures on countable sets (doi:10.1007/s10240-003-0016-0).
• 2009. Borcea, Brändén and Liggett introduce strongly Rayleigh measures and their negative-dependence theory (doi:10.1090/S0894-0347-08-00618-8).
• 2013. Lyons discusses the FUSF factor question for Cayley graphs (doi:10.4171/OWR/2013/42).
• 2016. Lyons and Thom prove Bernoulli isomorphism for equivariant determinantal measures on amenable Cayley graphs and ask a broader determinantal factor question (doi:10.1017/etds.2014.70).
• 2022. Nam, Sly and Zhang give FIID codings of free Ising measures on regular trees through Brownian-driven systems (doi:10.1007/s00220-021-04260-2).
• 2025. Timár proves FIID representability of the free forest on recurrent and invariantly amenable unimodular random graphs (doi:10.1007/s11856-025-2884-1).

The source of this mission, an OpenAI preprint dated September 25, 2026, proves the unrestricted statement with one rule for all graphs.

Setting

Let $G$ be an infinite, connected, locally finite, simple, undirected graph. For a finite connected subgraph $H$, let $\mathrm{UST}_H$ be the uniform law on spanning trees of $H$. For finite connected subgraphs $H_1\subseteq H_2\subseteq\cdots$ whose edges exhaust $E(G)$, the laws $\mathrm{UST}_{H_n}$ (edges outside $H_n$ absent) converge weakly; the limit $\mathrm{FUSF}_G$ on $\{0,1\}^{E(G)}$ does not depend on the exhaustion (Proposition 2.2).

A rule $\Phi(G,U,e)\in\{0,1\}$ takes a graph, real vertex labels $U=(U_v)$ and an edge. It is equivariant if $\Phi(\sigma G,\sigma U,\sigma e)=\Phi(G,U,e)$ for every isomorphism $\sigma$, and root independent if it uses no distinguished vertex.

A law $\mu$ on $\{0,1\}^F$, $F$ finite, is strongly Rayleigh if $\sum_x\mu(x)\prod_iz_i^{x_i}\ne0$ whenever all $\operatorname{Im}z_i>0$; on a countable set, every finite marginal must be strongly Rayleigh.

Formalization targets

Milestones (strongly Rayleigh processes, Section 6)

• Lemma 6.1: for strongly Rayleigh $\mu$ and tilts $\mu_h$, $\partial p_i/\partial h_j=\operatorname{Cov}_{\mu_h}(X_i,X_j)$ and $\sum_j|\partial p_i/\partial h_j|\le2p_i(1-p_i)\le\tfrac12$.
• Theorem 1.3: an invariant strongly Rayleigh law on $\{0,1\}^\Gamma$, $\Gamma$ a countable group, is an equivariant factor of IID.
• Inputs to Corollary 1.4: finite determinantal laws with $0\le K\le I$ exist and are strongly Rayleigh; on a countable set the determinantal law of a positive contraction exists and is unique.
• Corollary 1.4: invariant determinantal laws on countable groups are factors of IID, in particular when $K_{gh,gk}=K_{h,k}$.

Goal: Theorem 1.1

$$\exists\ \Phi\ \text{Borel, equivariant, root independent}:\quad \forall G,\quad \{e:\Phi(G,U,e)=1\}\sim\mathrm{FUSF}_G\quad\text{for IID Uniform}[0,1]\ U.$$

The Lean statement OAI.Problem336.fusf_is_factor_iid is open on the platform.

Significance

Theorem 1.1 answers the FUSF factor question without amenability, transience, unimodularity, degree bounds or moment assumptions, and with a single rule for all graphs; Corollary 1.2 gives the factor statement under every unimodular random graph law. Theorem 1.3 and Corollary 1.4 extend the method to all invariant strongly Rayleigh and determinantal processes on countable groups, addressing the regular-action case of the Lyons–Thom question. The paper asserts an ordinary Borel factor, not a finitary one.

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. Formalization would also provide uniform spanning trees, the free forest limit, strongly Rayleigh measures and determinantal laws as reusable Lean objects.

Difficulty

Previous constructions use structure that is absent in general: Wilson's algorithm works for the wired forest on transient graphs, and Timár's construction needs monotone limits along a hyperfinite exhaustion. A factor must produce one exact sample of the infinite-volume law while controlling all edges jointly, and equivariance forbids any choice of root or ordering. The paper's route observes the forest through independent Brownian noises and must show that the posterior drift has a uniformly Lipschitz response to the observations even when the fields are unbounded over the graph.

Formalization scope

• Graphs are coded on vertex set $\mathbb N$ by symmetric irreflexive ℕ → ℕ → Bool; edges are pairs $u<v$; a connected graph on $\mathbb N$ is automatically infinite. Equivariance is invariance under every permutation of $\mathbb N$ applied to graph, labels and edge.
• RuleBorel is joint measurability of $\Phi$ in the product σ-algebras.
• IsVertexIID requires the label coordinates to have independent Uniform$[0,1]$ finite-dimensional laws (with $s=\varnothing$ this forces a probability measure).
• HasFUSFLaw asks that every cylinder probability (edges in $A$ present, edges in $B$ absent) be the limit of the corresponding uniform-spanning-tree ratio along every exhaustion by finite connected subgraphs covering all edges.
• The strongly Rayleigh and determinantal milestones use ProbabilityMeasure (Γ → Bool), left translation $(\tau_ga)_h=a_{g^{-1}h}$, i.i.d. labels in Set.Icc 0 1 via Measure.infinitePi, and Hermitian kernels with $0\le\langle c,Kc\rangle\le\|c\|^2$ on finitely supported vectors.

A complete development needs the matrix-tree theorem and Kirchhoff formulas, weak limits on $\{0,1\}^{E}$, Brownian motion and a Borel Picard iteration for the decoder, and the Borcea–Brändén–Liggett theory. Contributions formalizing Proposition 2.2 (free exhaustion limit), Lemma 2.3 (finite-field forest response) and Proposition 4.2 (sampling from independent Brownian paths) are welcome.

Selected references

• OpenAI, The free uniform spanning forest is a factor of IID, preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-free-uniform-spanning-forest-is-a-factor-of-IID-September-25-2026/The-free-uniform-spanning-forest-is-a-factor-of-IID-September-25-2026.pdf
• I. Benjamini, R. Lyons, Y. Peres, O. Schramm, Uniform spanning forests, Ann. Probab., 2001. https://doi.org/10.1214/aop/1008956321
• R. Lyons, ℓ²-Betti numbers, cost, and the free uniform spanning forest, Oberwolfach Reports, 2013. https://doi.org/10.4171/OWR/2013/42
• Á. Timár, Factor of iid's through stochastic domination, Israel J. Math., 2025. https://doi.org/10.1007/s11856-025-2884-1
• R. Lyons, A. Thom, Invariant coupling of determinantal measures on sofic groups, Ergodic Theory Dynam. Systems, 2016. https://doi.org/10.1017/etds.2014.70
• R. Lyons, Determinantal probability measures, Publ. Math. IHÉS, 2003. https://doi.org/10.1007/s10240-003-0016-0
• J. Borcea, P. Brändén, T. M. Liggett, Negative dependence and the geometry of polynomials, J. Amer. Math. Soc., 2009. https://doi.org/10.1090/S0894-0347-08-00618-8
• D. Nam, A. Sly, L. Zhang, Ising model on trees and factors of IID, Comm. Math. Phys., 2022. https://doi.org/10.1007/s00220-021-04260-2
• R. Pemantle, Choosing a spanning tree for the integer lattice uniformly, Ann. Probab., 1991. https://arxiv.org/abs/math/0404043

Motivation: continuum phase transitions with a power-law tail

Whether identical classical particles in $\mathbb R^3$, interacting only through a stable radial pair potential, can undergo a phase transition is a classical existence problem of rigorous statistical mechanics, highlighted in Simon's list of problems in mathematical physics (Simon 1984). A transition shows up as a singularity of the thermodynamic free energy. Earlier rigorous continuum transitions rely on extra structure — two species, many-body terms, hard cores, or interactions defined through a fixed partition into boxes — or on a mean-field limit in which the potential itself changes. A natural requirement for a satisfactory answer is a single fixed pair potential with a bounded core and an explicit integrable power-law tail.

Timeline

• 1965 — Motzkin and Straus's weighted-graph maximization, later used for occupation bounds (Motzkin–Straus 1965).
• 1966 — Lebowitz and Penrose: rigorous van der Waals–Maxwell theory in the Kac limit (Lebowitz–Penrose 1966).
• 1970 — Ruelle's superstability framework (Ruelle 1970).
• 1971 — Ruelle: transition for a symmetric two-species continuum system (Ruelle 1971).
• 1973 — Gerardi, Marchioro, Olivieri and Presutti extend the Lebowitz–Penrose limit to superstable references (GMOP 1973).
• 1984 — Simon lists the problem among fifteen problems in mathematical physics.
• 1998–1999 — Lebowitz, Mazel and Presutti: liquid–vapor transition with attractive pair and repulsive four-body interactions (PRL 1998, J. Stat. Phys. 1999).
• 2026 — He, Jauslin, Lebowitz and Peled: transition for a finite-range box-modified Kac pair interaction (CMP 2026); Dereudre and Renaud-Chan: density coexistence for saturated many-body interactions (arXiv:2602.11078).
• 2026 — Two OpenAI preprints (OpenAI Math Release, September 24, 2026): a radial potential with divergent core and $o(r^{-3})$ tail with a temperature singularity, and the present A radial continuum phase transition with algebraic decay, which claims a bounded continuous potential with $|\phi(r)|\le Cr^{-3-1/32}$. Neither is peer reviewed, and the theorem is not formally verified.

Setting

Particles live in $\mathbb R^3$; a radial pair potential is a function $\phi:[0,\infty)\to\mathbb R$ (in Lean, ℝ≥0 → ℝ) applied to pair distances. For the cube $\Lambda_L=[0,L]^3$ and $N\ge0$,

$$U^\phi(x_1,\dots,x_N)=\sum_{i<j}\phi(|x_i-x_j|),\qquad Z_{L,N}(\beta)=\frac1{N!}\int_{\Lambda_L^N}e^{-\beta U^\phi}\,dx,\qquad Z_{L,0}=1 .$$

The potential is stable if $U^\phi\ge -BN$ for all configurations. The canonical free energy at density $\rho$ is

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

The packing constant is $p=\lim_{L\to\infty}M_L/L^3$, where $M_L$ is the largest number of points in $[0,L]^3$ at mutual distance $\ge1$; in Lean IsPackingDensity p asserts this limit. StrictTemperatureCorner f βc asserts finite left and right derivatives at $\beta_c$ with the right one strictly smaller, and non-differentiability.

Formalization targets

Milestone: the corner at the central density

At the single density $\rho=5p/3$: there are a bounded continuous stable $\phi$ with $|\phi(r)|\le Cr^{-3-1/32}$ for $r\ge1$ and $\beta_c\in[7/8,9/8]$ such that $f(\cdot,5p/3)$ exists for all $\beta>0$ and

$$f'_-(\beta_c,5p/3)>f'_+(\beta_c,5p/3).$$

Goal: a common corner on a density interval

There are a bounded continuous $\phi$, constants $B,C>0$ with

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

an open interval $I=(5p/3-\eta,\,5p/3+\eta)\subset(0,\infty)$ and one $\beta_c\in[7/8,9/8]$ such that for every $\rho\in I$ the free energy $f(\beta,\rho)$ exists and is finite for every $\beta>0$, and

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

This is Theorem 1.1 of the source. Both statements are published on the platform with status Open.

Significance

The result itself. The theorem gives a single-species, bounded, continuous radial pair potential with an explicit integrable power-law tail whose canonical free energy has a strict temperature corner at one critical inverse temperature for a whole interval of densities. The interaction is a genuine radial function of separations with all long-range terms kept; boxes appear only in the estimates. It does not treat Lennard–Jones-type potentials and does not identify the phases as conventional fluids. The companion preprint has a divergent core but only an $o(r^{-3})$ tail; the fixed power margin $1/32$ here needs a quantitative range estimate not present there.

Formalizing it. The statement fixes the model completely (free boundary conditions on $[0,L]^3$, Lebesgue measure without temperature normalization, $1/N!$, $\lfloor\rho L^3\rfloor$ particles), so a formal proof would settle exactly which version of the problem is solved. The infrastructure (thermodynamic limits, convex duality for pressures, Kac comparisons) is reusable for the companion mission.

Difficulty

The Lebowitz–Penrose theory produces non-convex mean-field free energies only in the limit where the attraction range tends to infinity, and that limiting object is not the free energy of any fixed potential. A single potential must therefore contain infinitely many attractions at growing ranges, and the required singularity must survive all of them. Density coexistence at fixed temperature does not by itself give a temperature corner at a fixed density: two supporting slopes with equal density coordinate and different energy coordinates are needed. A pointwise power bound constrains how strong the successive attractions may be relative to their ranges, which is why a quantitative comparison with an explicit error is required.

Formalization scope

• Positions are EuclideanSpace ℝ (Fin 3); distances enter through nndist, so the potential is a function on ℝ≥0. Boundedness, continuity, stability with $B>0$, and decay with $C>0$ are separate conjuncts.
• $p$ is existentially quantified but pinned by IsPackingDensity p (a limit), and $p>0$ is required; packingNumber is a sSup over a bounded set of naturals.
• IsCanonicalFreeEnergy φ ρ f asserts $-\log Z/(\beta L^3)\to f(\beta)$ for every $\beta>0$, so $f$ is determined on $(0,\infty)$; one-sided derivatives use HasDerivWithinAt on Iic βc and Ici βc.
• The goal requires the interval to lie in $(0,\infty)$ and $\beta_c$ to be independent of $\rho$.
• Needed infrastructure: superstability and occupation moments, existence of thermodynamic limits and their convex duality, a Motzkin–Straus bound, quantitative Kac comparison, and subdifferential persistence arguments.

Selected references

• B. Simon, Fifteen problems in mathematical physics, in Perspectives in Mathematics, Birkhäuser, 1984, 423–454. https://math.caltech.edu/SimonPapers/R27.pdf
• T. S. Motzkin and E. G. Straus, Maxima for graphs and a new proof of a theorem of Turán, Canad. J. Math. 17 (1965), 533–540. https://doi.org/10.4153/CJM-1965-053-6
• J. L. Lebowitz and O. Penrose, Rigorous treatment of the van der Waals–Maxwell theory of the liquid-vapor transition, J. Math. Phys. 7 (1966), 98–113. https://doi.org/10.1063/1.1704821
• D. Ruelle, Superstable interactions in classical statistical mechanics, Comm. Math. Phys. 18 (1970), 127–159. https://doi.org/10.1007/BF01646091
• D. Ruelle, Existence of a phase transition in a continuous classical system, Phys. Rev. Lett. 27 (1971), 1040–1041. https://doi.org/10.1103/PhysRevLett.27.1040
• A. Gerardi, C. Marchioro, E. Olivieri and E. Presutti, Van der Waals–Maxwell theory, Lebowitz–Penrose limit and superstable interactions, Comm. Math. Phys. 29 (1973), 219–231. https://doi.org/10.1007/BF01645248
• J. L. Lebowitz, A. E. Mazel and E. Presutti, Liquid–vapor phase transitions for systems with finite-range interactions, J. Stat. Phys. 94 (1999), 955–1025. https://doi.org/10.1023/A:1004591218510
• Q. He, I. Jauslin, J. Lebowitz and R. Peled, Liquid-vapor transition in a model of a continuum particle system with finite-range modified Kac pair potential, Comm. Math. Phys. 407 (2026), 240. https://doi.org/10.1007/s00220-026-05735-w
• D. Dereudre and C. Renaud-Chan, First-order phase transition for Gibbs point processes with saturated interactions, arXiv:2602.11078 (2026). https://arxiv.org/abs/2602.11078v1
• R. T. Rockafellar and R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3
• OpenAI, A continuum temperature singularity for a radial pair potential, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-continuum-temperature-singularity-for-a-radial-pair-potential-September-24-2026/paper.pdf
• OpenAI, A radial continuum phase transition with algebraic decay, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-radial-continuum-phase-transition-with-algebraic-decay-September-24-2026/paper.pdf

Motivation: phase transitions for continuum particles

Whether a single species of classical particles in $\mathbb R^3$, interacting only through a stable radial pair potential, can undergo a phase transition is one of the long-standing existence questions of rigorous statistical mechanics; it appears in Simon's list of problems in mathematical physics (Simon 1984). A phase transition is detected as a loss of regularity of the thermodynamic free energy. Lattice models and continuum models with extra structure (several species, many-body terms, hard cores, box-restricted interactions) were handled long ago; ordinary pair potentials finite at every positive separation remained the difficult case.

Timeline

• 1966 — Lebowitz and Penrose give the rigorous van der Waals–Maxwell theory in the Kac (long-range) limit (Lebowitz–Penrose 1966).
• 1970 — Ruelle's superstability framework for classical continuum systems (Ruelle 1970).
• 1971 — Ruelle proves a transition for the two-species Widom–Rowlinson model (Ruelle 1971).
• 1975 — Israel's convex construction gives coexistence for hard-core continuum particles with a spherically symmetric pair perturbation (Israel 1975).
• 1984 — Simon lists the continuum phase-transition problem among fifteen problems in mathematical physics.
• 1998–1999 — Lebowitz, Mazel and Presutti prove a liquid–vapor transition for attractive pair plus repulsive four-body interactions (PRL 1998, J. Stat. Phys. 1999).
• 2025–2026 — He, Jauslin, Lebowitz and Peled: coexistence for a box-modified Kac pair interaction (CMP 2026); Dereudre and Renaud-Chan: low-temperature coexistence for saturated (many-body) interactions (arXiv:2602.11078).
• 2026 — An OpenAI preprint, A continuum temperature singularity for a radial pair potential (OpenAI Math Release, September 24, 2026), claims an admissible radial pair potential in $\mathbb R^3$ whose canonical free energy has a temperature corner at one critical inverse temperature for every density in an open interval. It has not been peer reviewed and the theorem is not formally verified.

Setting

A radial pair potential is $\Phi(x)=\phi(|x|)$ on $\mathbb R^3$ with $\Phi(0)=+\infty$. It is admissible if $\Phi$ is Borel measurable, $\phi$ is finite and locally bounded on $(0,\infty)$, and

1. $\phi(r)\to+\infty$ as $r\downarrow0$;
2. $\phi\le-a<0$ on some interval $[r_1,r_2]$ with $0<r_1<r_2$;
3. $\int_R^\infty r^2|\phi(r)|\,dr<\infty$ for some $R$;
4. (stability) $U_N(x_1,\dots,x_N)=\sum_{i<j}\Phi(x_i-x_j)\ge -BN$ for all $N$ and all configurations.

With $\Lambda_L=[-L/2,L/2]^3$ and free boundary conditions, the canonical partition function is

$$Z_{\Lambda_L,N}(\beta)=\frac1{N!}\int_{\Lambda_L^N}e^{-\beta U_N}\,dx,\qquad Z_{\Lambda_L,0}=1,\quad e^{-\beta\cdot\infty}=0,$$

and the canonical free-energy density at density $\rho>0$ is

$$f(\beta,\rho)=-\frac1\beta\lim_{L\to\infty}L^{-3}\log Z_{\Lambda_L,\lfloor\rho L^3\rfloor}(\beta).$$

In Lean, radialPotential φ takes values in EReal (value ⊤ at the origin), energy is the pair sum, partition φ β L N is the integral above, and HasCanonicalFreeEnergy φ f says $L^{-3}\log Z\to-\beta f(\beta,\rho)$ for all $\beta,\rho>0$.

Formalization targets

Goal: a strict temperature corner throughout a density interval

There exist an admissible $\phi$ with $\phi(r)=o(r^{-3})$ as $r\to\infty$, a free-energy function $f$ realizing the canonical limit for every $\beta>0,\rho>0$, a nonempty open interval $I\subset(0,\infty)$ and one $\beta_c\in(1/2,3/2)$ such that for every $\rho\in I$ the one-sided $\beta$-derivatives exist and

$$D^-_\beta f(\beta_c,\rho)\;>\;D^+_\beta f(\beta_c,\rho).$$

This is Theorem 1.1 of the source (MainStatement). The goal is published on the platform with status Open.

Significance

The result itself. The theorem exhibits a genuine one-species pair potential, finite at every positive separation and with all cross-cube interactions retained, whose canonical free energy is not $C^1$ in temperature at a fixed density, with one critical temperature for an entire interval of densities. It does not concern the Lennard–Jones potential, does not identify the coexisting states as liquid/vapor/solid, and does not give a power-law tail $|\phi(r)|\le Cr^{-3-\varepsilon}$; formulations of the historical problem that require such a margin are not resolved by it. A companion preprint (A radial continuum phase transition with algebraic decay) gives a bounded potential with tail $r^{-3-1/32}$.

Formalizing it. The statement is fully explicit about the model, normalization, and boundary conditions, so a formal proof would remove any ambiguity about which version of the problem is solved. It requires thermodynamic limits for superstable continuum systems, convex-analytic facts about pressures, and a Kac/Lebowitz–Penrose comparison with uniform estimates, none of which is currently in Mathlib.

Difficulty

Density coexistence for a grand-canonical system does not by itself produce a temperature corner at a fixed density; one needs two supporting slopes of the pressure with the same density coordinate and different energy coordinates. Classical tools for transitions (Peierls arguments, reflection positivity, Kac limits) either need lattice structure, many-body terms, or a limit in which the potential itself changes. Here a single fixed potential must be built through infinitely many attractions at growing ranges, and the convex supporting-slope information must survive every approximation step while preserving stability and integrable tails.

Formalization scope

• Space is EuclideanSpace ℝ (Fin 3); the potential is EReal-valued with ⊤ at the origin, and the Boltzmann weight is $0$ when the energy is ⊤. Stability is stated in EReal, which also rules out ⊥.
• Free boundary conditions on the closed cube $[-L/2,L/2]^3$, Lebesgue measure without temperature normalization, $1/N!$, and $N=\lfloor\rho L^3\rfloor$ via Nat.floor; the limit is over real $L\to\infty$.
• One-sided derivatives are HasDerivWithinAt on Iic βc and Ici βc, so both are finite real numbers; $f$ is pinned by HasCanonicalFreeEnergy for every $\beta>0,\rho>0$, so it cannot be chosen freely near $\beta_c$.
• $I$ is open, order-connected, nonempty and contained in $(0,\infty)$; $\beta_c$ is independent of $\rho$.
• Needed infrastructure: superstability estimates, existence of canonical and grand-canonical thermodynamic limits, Legendre duality for pressures, the Lebowitz–Penrose limit. These are reusable for the companion mission.

Selected references

• B. Simon, Fifteen problems in mathematical physics, in Perspectives in Mathematics, Birkhäuser, 1984, 423–454. https://math.caltech.edu/SimonPapers/R27.pdf
• J. L. Lebowitz and O. Penrose, Rigorous treatment of the van der Waals–Maxwell theory of the liquid-vapor transition, J. Math. Phys. 7 (1966), 98–113. https://doi.org/10.1063/1.1704821
• D. Ruelle, Superstable interactions in classical statistical mechanics, Comm. Math. Phys. 18 (1970), 127–159. https://doi.org/10.1007/BF01646091
• D. Ruelle, Existence of a phase transition in a continuous classical system, Phys. Rev. Lett. 27 (1971), 1040–1041. https://doi.org/10.1103/PhysRevLett.27.1040
• R. B. Israel, Existence of phase transitions for long-range interactions, Comm. Math. Phys. 43 (1975), 59–68. https://doi.org/10.1007/BF01609141
• J. L. Lebowitz, A. E. Mazel and E. Presutti, Liquid–vapor phase transitions for systems with finite-range interactions, J. Stat. Phys. 94 (1999), 955–1025. https://doi.org/10.1023/A:1004591218510
• Q. He, I. Jauslin, J. Lebowitz and R. Peled, Liquid–vapor transition in a model of a continuum particle system with finite-range modified Kac pair potential, Comm. Math. Phys. 407 (2026), 240. https://doi.org/10.1007/s00220-026-05735-w
• D. Dereudre and C. Renaud-Chan, First-order phase transition for Gibbs point processes with saturated interactions, arXiv:2602.11078 (2026). https://arxiv.org/abs/2602.11078v1
• OpenAI, A radial continuum phase transition with algebraic decay, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-radial-continuum-phase-transition-with-algebraic-decay-September-24-2026/paper.pdf
• OpenAI, A continuum temperature singularity for a radial pair potential, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-continuum-temperature-singularity-for-a-radial-pair-potential-September-24-2026/paper.pdf

Motivation

In the low-temperature phase $\beta>1$ of the Sherrington–Kirkpatrick (SK) spin glass, the Gibbs measure is believed to split into many nearly separated pieces, and local dynamics such as heat-bath (Glauber) updates should take a very long time to move between them. Worst-case slow mixing (some bad starting state) is a weak statement: it says nothing about what happens when the chain is started from a typical equilibrium sample, which is how such chains are used in practice. This mission asks for a much stronger obstruction: for most equilibrium configurations held fixed as starting points, the dynamics is still far from equilibrium after a stretched-exponential time.

Timeline

• 1975. Sherrington and Kirkpatrick introduce the model (doi:10.1103/PhysRevLett.35.1792).
• 1980. Parisi proposes his variational description of the free energy (doi:10.1088/0305-4470/13/4/009).
• 2003, 2006. Guerra's interpolation bound and Talagrand's matching lower bound establish the Parisi formula (doi:10.1007/s00220-002-0773-5, doi:10.4007/annals.2006.163.221).
• 2009–2010. Monthus–Garel and Billoire report numerical evidence for an $n^{1/3}$ scale of logarithmic relaxation times (doi:10.1088/1742-5468/2009/12/P12017, doi:10.1088/1742-5468/2010/11/P11034).
• 2018. Ben Arous and Jagannath turn overlap free-energy barriers into exponentially small spectral gaps for mean-field spin glasses under landscape hypotheses that exclude pure SK (doi:10.1007/s00220-018-3152-6).
• 2022. El Alaoui, Montanari and Sellke prove an obstruction to stable sampling algorithms at $\beta>1$ (arXiv:2203.05093).
• 2025. Sellke proves exponentially slow worst-case Glauber mixing for SK at sufficiently large $\beta$ (arXiv:2511.22621).
• 2026. Bandeira, El Alaoui and Rödder prove polynomial mixing at every $\beta$ under a large uniform external field (arXiv:2607.06813).

The source of this mission is an OpenAI preprint dated September 24, 2026. It covers the entire range $\beta>1$, at zero field, for typical rather than worst-case starts.

Setting

For $n\ge2$ and independent standard Gaussians $(J_{ij})_{i<j}$, put

$$H^J(x)=\frac1{\sqrt n}\sum_{i<j}J_{ij}x_ix_j,\qquad \pi^J(x)=\frac{e^{\beta H^J(x)}}{Z^J},\qquad x\in\{-1,1\}^n .$$

In continuous-time heat-bath dynamics each site has a rate-one clock; when site $i$ rings, its spin becomes $s\in\{\pm1\}$ with probability $e^{\beta sh_i}/(2\cosh\beta h_i)$, where $h_i=n^{-1/2}\sum_{j\ne i}J_{ij}x_j$. Let $P^J_t$ be its kernel and $K^J$ the discrete kernel that resamples one uniformly chosen site. For a fixed start $x$,

$$d^J(x,t)=\|P^J_t(x,\cdot)-\pi^J\|_{\rm TV},\qquad d^J_{\rm disc}(x,k)=\|(K^J)^k(x,\cdot)-\pi^J\|_{\rm TV}.$$

Formalization targets

Goal: Theorem 1.1

Let $\kappa=1/10000$. For every fixed $\beta>1$,

$$\mathbb P_{J,\ x_0\sim\pi^J}\Bigl\{d^J\bigl(x_0,e^{n^\kappa}\bigr)>\tfrac14\Bigr\}\to1,\qquad \mathbb P_{J,\ x_0\sim\pi^J}\Bigl\{d^J_{\rm disc}\bigl(x_0,\lfloor e^{n^\kappa}\rfloor\bigr)>\tfrac14\Bigr\}\to1 .$$

The order matters: $x_0$ is drawn from $\pi^J$ and then held fixed as the starting state. Lean: OAI.SK.main, open on the platform; it writes the joint probability as the disorder average of the Gibbs mass of slow starts.

Significance

The theorem shows that throughout the low-temperature phase, a Gibbs-sampled start carries information that local updates cannot erase in time $e^{n^{1/10000}}$; in particular (Corollary 1.2) every polynomial time scale is too short from a typical start. This separates the zero-field low-temperature SK model from the high-temperature and large-field regimes, where polynomial mixing holds. The exponent $1/10000$ is not claimed to be optimal; numerical studies suggest $n^{1/3}$.

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists.

Difficulty

Integrating the transition kernel over the starting state recovers $\pi^J$ at every time, so averaging arguments are useless; the obstruction must be established start by start, for a set of starts of Gibbs mass tending to one. Free-energy barrier criteria in the style of Ben Arous–Jagannath do not apply to the pure quadratic SK covariance. The proof needs quantitative Parisi-type comparisons for constrained replica overlaps, and a mechanism ("locking") that forces small overlaps with a third replica to stay put when two replicas overlap substantially.

Formalization scope

• hamiltonian J x = (∑_{i<j} J_{ij} x_i x_j)/√n; disorderLaw n is the product of standard Gaussians over pairs $i<j$.
• heatBath β J x y is the one-step kernel: average over sites $i$ of the conditional resampling probability, nonzero only when $y$ agrees with $x$ off $i$ (so holding is included).
• discreteKernel iterates it; continuousKernel β J t = ∑_k e^{-nt}(nt)^k/k! · K^k, the uniformized rate-$n$ chain, equivalent to rate-one clocks per site.
• continuousBadMass β n and discreteBadMass β n are $\mathbb E_J$ of the Gibbs mass of starts with distance $>1/4$ at time timeScale n = exp(n^κ) (resp. its floor).
• The goal asserts both bad masses tend to $1$ for each fixed $\beta>1$.

Infrastructure: finite Markov chains, Gaussian interpolation (Guerra–Talagrand bounds for constrained overlaps), Parisi functional regularity, and Gaussian concentration. The paper's Theorem 2.4 (quantitative free-energy comparison), Proposition 4.4 (absolute-overlap locking) and Proposition 6.1 (stretched-exponential coverage) are natural intermediate targets.

Selected references

• OpenAI, Stretched-exponential barriers for typical SK initial states, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Stretched-exponential-barriers-for-typical-SK-initial-states-September-24-2026/paper.pdf
• D. Sherrington, S. Kirkpatrick, Solvable model of a spin-glass, Phys. Rev. Lett., 1975. https://doi.org/10.1103/PhysRevLett.35.1792
• G. Parisi, A sequence of approximated solutions to the S-K model for spin glasses, J. Phys. A, 1980. https://doi.org/10.1088/0305-4470/13/4/009
• F. Guerra, Broken replica symmetry bounds in the mean field spin glass model, Comm. Math. Phys., 2003. https://doi.org/10.1007/s00220-002-0773-5
• M. Talagrand, The Parisi formula, Ann. of Math., 2006. https://doi.org/10.4007/annals.2006.163.221
• G. Ben Arous, A. Jagannath, Spectral gap estimates in mean field spin glasses, Comm. Math. Phys., 2018. https://doi.org/10.1007/s00220-018-3152-6
• M. Sellke, Exponentially slow mixing of the low temperature SK model, preprint, 2025. https://arxiv.org/abs/2511.22621
• A. S. Bandeira, A. El Alaoui, A. Rödder, Mixing of Glauber dynamics on high overlap Gibbs measures, preprint, 2026. https://arxiv.org/abs/2607.06813
• A. El Alaoui, A. Montanari, M. Sellke, Sampling from the Sherrington–Kirkpatrick Gibbs measure via algorithmic stochastic localization, FOCS 2022. https://arxiv.org/abs/2203.05093
• D. Panchenko, Free energy in the mixed p-spin models with vector spins, Ann. Probab., 2018. https://doi.org/10.1214/17-AOP1194

Motivation

The Sherrington–Kirkpatrick (SK) model is the mean-field spin glass, and $\beta=1$ is its equilibrium critical point. Physicists expect critical slowing down: at a phase transition, local dynamics needs time growing polynomially in the system size to relax. For the SK model this was studied through linearized mean-field theory, dynamical equations for correlation and response, and simulations of equilibrium autocorrelations on an $n^{2/3}$ time scale. Rigorous results on Glauber dynamics had concentrated on high temperature, where mixing is fast. This mission asks for a rigorous total-variation obstruction at $\beta=1$: most equilibrium configurations, used as starting states, are still far from equilibrium after $o(n^{2/3})$ time.

Timeline

• 1975, 1978. Sherrington and Kirkpatrick introduce the model and study Glauber autocorrelations above the critical temperature (doi:10.1103/PhysRevLett.35.1792, doi:10.1103/PhysRevB.17.4384).
• 1976. Kosterlitz, Thouless and Jones analyze the spherical spin glass, with its transition at the spectral edge (doi:10.1103/PhysRevLett.36.1217).
• 1981–1982. Sompolinsky and Zippelius develop dynamical equations for correlation and response (doi:10.1103/PhysRevLett.47.359, doi:10.1103/PhysRevB.25.6860).
• 1996. Comets relates the Ising and spherical partition functions via a Haar-averaging identity (doi:10.24033/ast.331).
• 2011. Billoire and Campbell numerically examine critical autocorrelations on the $n^{2/3}$ scale (doi:10.1103/PhysRevB.84.054442).
• 2016, 2022. Baik and Lee, and Landon, prove free-energy fluctuation limits for the spherical model, including criticality (doi:10.1007/s10955-016-1610-0, doi:10.1063/5.0054298).
• 2019, 2022. Bauerschmidt–Bodineau and Eldan–Koehler–Zeitouni prove functional inequalities at high temperature (doi:10.1016/j.jfa.2019.01.007, doi:10.1007/s00440-021-01085-x).
• 2026. Du and Huang prove critical free-energy and overlap results (arXiv:2607.02172, arXiv:2608.08752); Wang and Boban–Li–Oveis Gharan prove fast mixing for $\beta<1/2$ and $\beta<1/2+\varepsilon_0$ (arXiv:2608.22159, arXiv:2609.13138).

The source of this mission is an OpenAI preprint dated September 24, 2026.

Setting

At $\beta=1$ and zero field, let $W_{ij}\sim N(0,1/n)$ be independent for $i<j$ and

$$\mu_W(x)\propto\exp\Bigl(\sum_{i<j}W_{ij}x_ix_j\Bigr),\qquad x\in\{-1,1\}^n .$$

A heat-bath update at site $i$ resamples $x_i$ from its conditional law given the other spins. In continuous time every site has an independent rate-one clock (generator $\sum_i(K_i-I)$); in discrete time each step updates a uniformly chosen site (kernel $n^{-1}\sum_iK_i$). For a fixed start $x$, $d^{\rm ct}_t(W,x)$ and $d^{\rm dt}_k(W,x)$ are the total-variation distances to $\mu_W$.

Formalization targets

Goal: Theorem 1.1 (realized equilibrium initial states)

For every deterministic $t_n\ge0$ with $t_n=o(n^{2/3})$ and every deterministic integer $k_n=o(n^{5/3})$,

$$\mu_W\{x:\ d^{\rm ct}_{t_n}(W,x)>1/4\}\ \xrightarrow{\ \mathbb P\ }\ 1,\qquad \mu_W\{x:\ d^{\rm dt}_{k_n}(W,x)>1/4\}\ \xrightarrow{\ \mathbb P\ }\ 1 .$$

Lean: OAI.CriticalSK.realized_equilibrium_initial_states, open on the platform.

Milestone: Theorem 1.2 (covariance and linear tests)

With $\Sigma=\operatorname{Cov}_{\mu_W}(x)$, $\mathcal D(f)=\sum_i\mu_W[\operatorname{Var}(f\mid x_{-i})]$ and $R_{\rm lin}=\sup_{a\ne0}\operatorname{Var}(a^{\mathsf T}x)/\mathcal D(a^{\mathsf T}x)$: for every $M_n\to\infty$, with probability tending to one,

$$\|\Sigma\|,\ R_{\rm lin}\ \in\ \bigl[n^{2/3}/M_n,\ M_nn^{2/3}\bigr].$$

Milestones: Theorem 1.3 (critical mixing bounds)

For every fixed $\epsilon>0$,

$$\mathbb P\{n^{2/3-\epsilon}\le t_{\rm mix}\le e^{\epsilon n}\}\to1,\qquad \mathbb P\{n^{5/3-\epsilon}\le k_{\rm mix}\le e^{\epsilon n}\}\to1,$$

with a separate Lean target for the lower bounds alone.

Significance

The theorem shows that at criticality the slow direction is visible from typical equilibrium starts, not only from adversarial ones, and pins the time scale $n^{2/3}$ to the spectral edge of the coupling matrix. Theorem 1.2 identifies the covariance scale $n^{2/3}$, contrasting with bounded covariance at every $\beta<1$. A companion OpenAI preprint uses Theorems 1.1 and 1.2 as inputs for matching upper bounds $n^{2/3+o(1)}$.

The results are proved in an OpenAI preprint; they have not been peer reviewed, and no machine-checked proof exists.

Difficulty

Averaging over the starting state gives back the stationary law, so the obstruction must be proved start by start. The slow observable is the projection $v^{\mathsf T}x$ on the top eigenvector of the coupling matrix; the difficulty is the static estimate that this projection is rarely small on the $n^{1/3}$ scale under the Ising Gibbs law. This requires edge-of-spectrum random matrix estimates, a precise comparison between the Ising law and a tilted spherical law, and control of the conditioning on the sphere.

Formalization scope

• hamiltonian W x = ∑_{i<j} W_{ij} x_i x_j; disorderLaw n is the product of gaussianReal 0 (1/n) over pairs $i<j$.
• siteKernel W i is the heat-bath kernel on configurations agreeing off $i$; discreteKernel = n^{-1}∑_i siteKernel; continuousKernel W t = exp(t ∑_i (siteKernel W i - 1)).
• continuousGoodMass/discreteGoodMass are the Gibbs masses of starts with distance $>1/4$; convergence in probability is written as $\mathbb P(|\text{mass}-1|\ge\delta)\to0$ for all $\delta>0$.
• covarianceNorm is the Euclidean operator norm; linearRayleigh is a real sSup over nonzero $a$ (the quotient is bounded and the set nonempty).
• Mixing times are sInf over times at which all starts are within $1/4$.

Infrastructure: finite continuous-time Markov chains (matrix exponentials), GOE edge estimates, tridiagonal models, spherical integrals. The intermediate results Proposition 3.1, Theorem 5.3 and Proposition 5.4 are natural further milestones.

Selected references

• OpenAI, Critical slowing down in the Sherrington–Kirkpatrick model, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Critical-slowing-down-in-the-Sherrington-Kirkpatrick-model-September-24-2026/paper.pdf
• D. Sherrington, S. Kirkpatrick, Solvable model of a spin-glass, Phys. Rev. Lett., 1975. https://doi.org/10.1103/PhysRevLett.35.1792
• H. Sompolinsky, A. Zippelius, Dynamic theory of the spin-glass phase, Phys. Rev. Lett., 1981. https://doi.org/10.1103/PhysRevLett.47.359
• F. Comets, A spherical bound for the Sherrington–Kirkpatrick model, Astérisque, 1996. https://doi.org/10.24033/ast.331
• H. Du, B. Huang, Fluctuations of the Sherrington–Kirkpatrick free energy at critical temperature, preprint, 2026. https://arxiv.org/abs/2607.02172
• H. Du, B. Huang, Overlap distribution of the critical Sherrington–Kirkpatrick model, preprint, 2026. https://arxiv.org/abs/2608.08752
• J. Baik, J. O. Lee, Fluctuations of the free energy of the spherical Sherrington–Kirkpatrick model, J. Stat. Phys., 2016. https://doi.org/10.1007/s10955-016-1610-0
• B. Landon, Free energy fluctuations of the two-spin spherical SK model at critical temperature, J. Math. Phys., 2022. https://doi.org/10.1063/5.0054298
• A. Billoire, I. A. Campbell, Dynamics in the Sherrington–Kirkpatrick Ising spin glass at and above $T_g$, Phys. Rev. B, 2011. https://doi.org/10.1103/PhysRevB.84.054442

Motivation

The Sherrington–Kirkpatrick (SK) model (1975) is the basic mean-field spin glass: $n$ Ising spins interact through independent Gaussian couplings of variance $\beta^2/n$, so each spin is weakly coupled to every other one with random signs. The model is the testing ground for questions about disordered systems, about sampling from Gibbs measures, and about the performance of Markov chain Monte Carlo. A central question is whether Glauber (heat-bath) dynamics, which resamples one spin at a time from its conditional law, relaxes at a rate independent of the system size. Equivalently: does the Gibbs measure satisfy a dimension-free Poincaré inequality with respect to the heat-bath Dirichlet form?

The equilibrium high-temperature phase is $\beta<1$, where the free energy equals its annealed value (Aizenman, Lebowitz and Ruelle 1987). Dynamical results had reached only part of this range.

Timeline

• 1963. Glauber introduces local stochastic spin dynamics (doi:10.1063/1.1703954).
• 1975. Sherrington and Kirkpatrick introduce the model (doi:10.1103/PhysRevLett.35.1792).
• 1987. Aizenman, Lebowitz and Ruelle prove the annealed free energy $\log2+\beta^2/4$ for all $\beta<1$ (doi:10.1007/BF01217677).
• 2006. Wu proves Poincaré inequalities under a Dobrushin-type condition (doi:10.1214/009117906000000368).
• 2019. Bauerschmidt and Bodineau prove a high-temperature log-Sobolev inequality for a different (full spin-flip) Dirichlet form (doi:10.1016/j.jfa.2019.01.007).
• 2022. Eldan, Koehler and Zeitouni give a spectral condition yielding a heat-bath gap for $\beta<1/4$ (doi:10.1007/s00440-021-01085-x); Anari, Jain, Koehler, Pham and Vuong prove $O(n\log n)$ mixing in the same range (arXiv:2106.04105).
• 2024. Anari, Koehler and Vuong extend this to $\beta\approx0.295$ (doi:10.1145/3618260.3649622); Adhikari, Brennecke, Xu and Yau obtain gaps for mixed $p$-spin models under a small-coefficient condition (doi:10.1007/s00440-024-01261-9); El Alaoui and Gaitonde, and Brennecke, Schertzer, Xu and Yau, control the spin covariance for all $\beta<1$ (arXiv:2212.02445, doi:10.2140/pmp.2024.5.131).
• 2026. Wang proves optimal mixing for $\beta<1/2$ (arXiv:2608.22159); Boban, Li and Oveis Gharan reach $\beta<1/2+\varepsilon_0$ (arXiv:2609.13138).

The source of this mission is an OpenAI preprint dated September 24, 2026, which treats every fixed $\beta<1$.

Setting

Fix $0<\beta<1$. Let $J$ be a symmetric $n\times n$ matrix with zero diagonal and independent entries $J_{ik}\sim N(0,\beta^2/n)$ for $i<k$. The zero-field Gibbs law on $\{-1,1\}^n$ is

$$\mu_0(x)=\frac1{Z}\exp\Bigl\{\tfrac12x^{\mathsf T}Jx\Bigr\}.$$

Let $P_i$ be the conditional expectation under $\mu_0$ given all spins except $x_i$; it averages $f$ over $x$ and its $i$-th flip with Gibbs weights. The unscaled Dirichlet form is

$$\mathcal D(f)=\sum_{i=1}^n\mathbb E_{\mu_0}\bigl(f-P_if\bigr)^2 .$$

The discrete heat-bath chain picks a uniform site and resamples it, with transition operator $n^{-1}\sum_iP_i$; its spectral gap is $\inf_f \mathcal D(f)/(n\operatorname{Var}_{\mu_0}f)$ over nonconstant $f$.

Formalization targets

Goal: Theorem 1.1

There is a finite constant $C_\beta$ such that

$$\mathbb P_J\Bigl\{\operatorname{Var}_{\mu_0}(f)\le C_\beta\,\mathcal D(f)\ \text{for every }f:\{-1,1\}^n\to\mathbb R\Bigr\}\ \longrightarrow\ 1,$$

and consequently the discrete heat-bath chain has spectral gap at least $1/(C_\beta n)$ with probability tending to one. Lean: OAI.SKGap.sk_main, open on the platform.

Significance

The theorem gives a size-independent relaxation time for continuous-time heat-bath dynamics (rate-one clocks) throughout the high-temperature phase, for every observable simultaneously on one disorder event. It extends the dynamical picture from $\beta<1/2+\varepsilon_0$ to the full equilibrium range $\beta<1$, where only linear-observable (covariance) control was previously known. A Poincaré inequality is the input for $L^2$ mixing bounds and for companion results on cutoff and critical slowing down.

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists.

Difficulty

Dobrushin-type influence bounds fail because the sum of absolute couplings at a site grows like $\sqrt n$; any argument must exploit cancellations from the random signs. Covariance bounds control only linear observables, while the Poincaré inequality must hold for all $2^{2^n}$-dimensional families of test functions at once. The natural route through stochastic localization runs into rare observation events: an event of exponentially small probability can still carry most of the variance of a particular test function, and invertibility of the field equation must hold at every sufficiently accurate solution along the observation path.

Formalization scope

• Spins are Fin n → Bool, with spinValue mapping to $\pm1$; couplings are indexed by pairs $i<k$ (Edge n) and symmetrized with zero diagonal by coupling.
• hamiltonian g 0 x = ½ ∑_{i,k} x_i J_{ik} x_k; mass, expectation, variance are exact finite sums over $\{-1,1\}^n$.
• conditionalExpectation g h i f x is the two-point Gibbs average over $x$ and its $i$-th flip; dirichlet is the unscaled form $\sum_i\mathbb E(f-P_if)^2$.
• disorderLaw β n = Measure.pi (fun _ => gaussianReal 0 (β^2/n)) over the edges (variance $\beta^2/n$).
• discreteGap g is the infimum of $\mathcal D(f)/(n\operatorname{Var}f)$ over $f$ with positive variance.
• MainStatement β asserts a single $C>0$ for which both the Poincaré event and the gap event have probability tending to $1$.

Formalization needs Gaussian product measures, finite Gibbs measures and heat-bath operators, and the analysis behind the proof: matrix concentration, TAP/AMP-type field recursions and stochastic localization. Formal versions of the paper's intermediate results (for example Proposition 8.3, the terminal observation gap) are welcome.

Selected references

• OpenAI, A spectral gap throughout the high-temperature Sherrington–Kirkpatrick phase, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-spectral-gap-throughout-the-high-temperature-Sherrington-Kirkpatrick-phase-September-24-2026/main.pdf
• D. Sherrington, S. Kirkpatrick, Solvable model of a spin-glass, Phys. Rev. Lett., 1975. https://doi.org/10.1103/PhysRevLett.35.1792
• M. Aizenman, J. L. Lebowitz, D. Ruelle, Some rigorous results on the Sherrington–Kirkpatrick spin glass model, Comm. Math. Phys., 1987. https://doi.org/10.1007/BF01217677
• R. Eldan, F. Koehler, O. Zeitouni, A spectral condition for spectral gap: fast mixing in high-temperature Ising models, Probab. Theory Related Fields, 2022. https://doi.org/10.1007/s00440-021-01085-x
• N. Anari, F. Koehler, T.-D. Vuong, Trickle-down in localization schemes and applications, STOC 2024. https://doi.org/10.1145/3618260.3649622
• S. Wang, Optimal mixing of Glauber dynamics for the Sherrington–Kirkpatrick model at $\beta<1/2$, preprint, 2026. https://arxiv.org/abs/2608.22159
• M. Boban, A. Li, S. Oveis Gharan, Rank-1-perturbed trickledown theorems, preprint, 2026. https://arxiv.org/abs/2609.13138
• C. Brennecke, A. Schertzer, C. Xu, H.-T. Yau, The two point function of the SK model without external field at high temperature, Probab. Math. Phys., 2024. https://doi.org/10.2140/pmp.2024.5.131
• Y. Chen, R. Eldan, Localization schemes: a framework for proving mixing bounds for Markov chains, Duke Math. J., 2025. https://doi.org/10.1215/00127094-2024-0063
• R. Eldan, Thin shell implies spectral gap up to polylog via a stochastic localization scheme, Geom. Funct. Anal., 2013. https://doi.org/10.1007/s00039-013-0214-y