Probability

Motivation

A diluted spin glass has finitely many interactions per spin on average. The source seeks the exact thermodynamic pressure using a hierarchy of random local-field laws. The source is OpenAI's September 2026 manuscript.

Setting

The pressure is the expected logarithm of the partition function divided by the number of Ising spins. A Poisson number of even-arity interactions and independent external fields define the model. The cavity functional uses nested probability laws and iterated logarithmic power means.

Formalization targets

$$\lim_{N\to\infty}F_N=\inf_{r\ge0}\ \inf_{\zeta,\ 0<m_1<\cdots<m_r<1} B_r(\zeta,m).$$

For every model of a diluted p-spin glass with Ising spins in {+1,-1} that satisfies the standing admissibility hypotheses, the free-energy density F_N converges, as N tends to infinity, to a variational value, so existence of the thermodynamic limit is part of the conclusion. A model consists of a density α ≥ 0, a probability law on interaction samples (θ, a, b, f), where θ is a real function on spin configurations in {±1}^p, a and b are reals and f assigns to each of the p slots a real function on spins, and a probability law for the external field on ℝ. Admissibility means: p is even and at least 2; α > 0; ‖θ‖ = max_s |θ(s)| and |h| are integrable under the disorder and field laws; almost surely a > 0 and, for every configuration s, exp θ(s) = a(1 + b ∏_l f_l(s_l)) with |b ∏_l f_l(s_l)| < 1; the functions f_1,…,f_p are independent and identically distributed, b is independent of the vector f, every power (−b)^n with n ≥ 1 is integrable, and E[(−b)^n] ≥ 0. No boundedness of interactions, fields or messages is added. F_N is (1/N) times the expectation of log Σ_σ exp(−H), where the number k of interactions is Poisson with mean αN, the k interactions are independent disorder samples, the N fields are independent field samples, and each interaction is placed on p index choices in {1,…,N} (repetitions allowed) averaged uniformly over all choices; here the log-weight of σ is Σ_j θ_j(σ at the chosen indices) + Σ_i h_i σ_i. The limit is the infimum over depths r ≥ 0 of φ_r, itself the infimum, over a nested law ζ in the r-fold hierarchy of probability measures (each level with the weak topology and its Borel σ-field) and exponents 0 < m_1 < … < m_r < 1, of the cavity functional B_r. B_r equals log 2 plus the Poisson(αp)-averaged expectation of the site term, a logarithm of an average over spin ε of exp(hε + Σ_j message_j(ε)), minus α(p−1) times the expectation of the log of the edge weight, with both terms evaluated through iterated log power-means in the exponents m_i.

The goal is OAI.DilutedSpinGlass.mezard_parisi.

Significance

The equality identifies the limit with the infimum over all finite hierarchy depths. Existence of the thermodynamic limit is part of the conclusion, not an assumption. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Upper bounds at each hierarchy depth do not yield equality with the infinite-size model. Unbounded disorder requires retaining integrability hypotheses through nested expectations.

Formalization scope

The admissibility predicate requires positive density, even arity at least two, first moments, the specified interaction factorization, and positivity and integrability of the relevant powers. The statement adds no boundedness restriction on interactions, fields, or trial messages.

The shared definitions are supplied by DilutedSpin. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, The Mézard–Parisi formula for diluted spin glasses, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

On an expanding infinite graph, the appearance of an infinite open cluster and the appearance of a unique one can occur at different densities. The source seeks a nonempty interval where infinitely many infinite clusters coexist. The source is OpenAI's September 2026 manuscript.

Setting

In bond percolation, edges are independently retained with probability $p$. The critical threshold $p_c$ records appearance of infinite clusters; $p_u$ records uniqueness. The intermediate operator threshold records boundedness on $\ell^2$ of the two-point connection kernel.

Formalization targets

$$p_c<p_{2\to2}\le p_u,\qquad\|T_{p_c}\|<\infty,$$

For a bond graph G, given by a map from an edge type E to unordered pairs of vertices in an infinite vertex type V, that is connected, locally finite (each vertex lies in finitely many edges) and quasi-transitive (finitely many vertex representatives such that every vertex is the image of one under an automorphism of G acting on vertices and edges), and whose vertex isoperimetric constant hV(G), the infimum over nonempty finite vertex sets A of |outer vertex boundary of A|/|A|, is strictly positive, the MainConclusion holds for Bernoulli bond percolation on G. Writing pc for the infimum of parameters p at which an infinite cluster occurs with positive probability, pu for the infimum of p at which there is almost surely exactly one infinite cluster, ptwo for the supremum of p at which the two-point function τ_p(x,y)=P_p(x connected to y) is the matrix kernel of a bounded operator on ℓ²(V), and operatorNorm(p) for the infimum of operator norms of such operators, valued in [0,∞], the conclusion has four parts. First, the supremum of operatorNorm(p) over p<pc equals operatorNorm(pc). Second, operatorNorm(pc) is finite. Third, pc<ptwo≤pu. Fourth, there exist p₁<p₂<1 with pc<p₁ such that, for almost every i.i.d. uniform [0,1] edge labelling, for every p in [p₁,p₂] the configuration of edges with label at most p has infinitely many infinite clusters. The proof is omitted (sorry) in the source.

The goal is OAI.Percolation.BenjaminiSchramm.full_main. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.

• cayley main.
• critical laws.
• arbitrary cayley.

Significance

The full goal also identifies the critical norm as the supremum from below and supplies simultaneous nonuniqueness over a fixed interval under the uniform-label coupling. Supporting statements cover critical laws and Cayley graphs. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

A separate almost-sure statement at each parameter does not establish one event valid for every parameter in an interval. Critical operator control must also survive the passage to the threshold itself.

Formalization scope

The graph has infinitely many vertices, is connected and locally finite, has finitely many vertex orbits, and has positive vertex isoperimetric constant. Thresholds lie in the unit interval; operator norms may take extended nonnegative values. The independent Cayley definition group is retained separately.

The shared definitions are supplied by BenjaminiSchramm, CayleyPercolation. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, Nonuniqueness of percolation on nonamenable quasi-transitive graphs, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

Random edge travel times produce a deterministic large-scale shape. The source studies two distinct regularity questions: corners and flat boundary segments. The available exponential target addresses differentiability and the structure of supporting lines. The source is OpenAI's September 2026 manuscript.

Setting

In first-passage percolation, travel time is the infimum of path costs on the nearest-neighbor square lattice. A time-constant norm gives the asymptotic travel time in each direction. Its unit ball is the limit shape.

Formalization targets

$$\frac{T(0,\lfloor tv\rfloor)}t\longrightarrow\mu(v)\quad\text{almost surely},\qquad \mu\text{ differentiable on }\mathbb R^2\setminus\{0\},\qquad\partial\{\mu\le1\}\text{ has regular }C^1\text{ charts}.$$

For any probability space (Ω, P) carrying an edge-weight family τ indexed by the edges of the nearest-neighbour lattice ℤ², where each vertex p has an east edge (p,false) and a north edge (p,true), such that the τ(e) are measurable, mutually independent, and each has the exponential distribution with rate 1 (the ExponentialEnvironment hypothesis), there exists a function μ on the plane ℝ² with the following properties. First, μ is a norm: nonnegative, zero only at the origin, subadditive, and satisfying μ(av)=|a|μ(v) for all real a. Second, μ is the time constant: for every v in ℝ², almost surely the first-passage time from (0,0) to the lattice point (⌊tv₀⌋,⌊tv₁⌋), defined as the infimum of path costs over nearest-neighbour step sequences (east, west, north, south) that sum the edge weights along the path, divided by t, converges to μ(v) as t→∞. Third, μ is Fréchet differentiable at every nonzero point. Fourth, at every point v with μ(v)=1 there is exactly one linear functional ℓ with ℓ(v)=1 and ℓ(w)≤μ(w) for all w. Fifth, the unit sphere of μ is a C¹ curve in the sense that near each point v with μ(v)=1 there is an open neighbourhood U and a C¹ function g on U whose zero set in U is exactly the set where μ=1, with g having a nonzero Fréchet derivative at each of those zeros. Sixth, for each boundary point v of the unit ball {μ≤1}, there is a unique line L that is the level set {z : g(z)=g(v)} of some nonzero continuous linear functional g that attains its maximum over the unit ball at v, so each boundary point has a unique supporting line. Seventh, every boundary point v of the unit ball has a C¹ curve chart: an open neighbourhood U of v and a C¹ map γ:ℝ→ℝ² with nowhere vanishing derivative, together with a function θ continuous on U, such that γ takes values in the boundary within U, θ(γ(t))=t for all t, and γ(θ(z))=z for each boundary point z in U.

The goal is OAI.PlanarFPP.manuscriptMain. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.

• gamma differentiability.

Significance

The chosen target supplies the norm and its limiting interpretation, unique normalized supporting functionals, unique supporting lines, and boundary charts. The Gamma-law differentiability statement is retained as a separate supporting target. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Pointwise convergence to a norm does not imply differentiability of that norm. Excluding corners requires additional information about nearby directions, and the chart conclusion requires regularity beyond mere continuity.

Formalization scope

The main target uses independent rate-one exponential weights. It does not assert strict convexity, despite the broader manuscript title; strict convexity is not added implicitly. The Gamma target has arbitrary positive shape and rate. Each original definition group remains independent.

The shared definitions are supplied by GammaPassage, PlanarFirstPassage. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, Strict convexity and differentiability of the planar exponential first-passage limit shape, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

Random triangle deletion constructs a partial triangle packing. Its terminal uncovered edges measure how efficiently this process covers pairs, and the source seeks the leading constant rather than only the growth exponent. The source is OpenAI's September 2026 manuscript.

Setting

Start from the complete graph on $n$ vertices. At each step choose a remaining triangle uniformly and remove its three edges. A triangle-free state stays fixed. The terminal leave $F_n$ is the edge count at the end.

Formalization targets

$$\mathbb E\left[\left(\frac{F_n}{n^{3/2}}-\frac1{2\sqrt2}\right)^2\right]\to0,\qquad \frac{F_n}{n^{3/2}}\xrightarrow{\mathbb P}\frac1{2\sqrt2},\qquad \frac{\mathbb E F_n}{n^{3/2}}\to\frac1{2\sqrt2}.$$

For the random triangle-removal process, three limits hold as n tends to infinity. The process starts from the complete graph on n vertices, with graphs represented as sets of 2-element subsets of Fin n. At each step, if the current graph G contains triangles (3-subsets all of whose pairs are edges of G), one triangle is chosen uniformly at random and its three edges are deleted; if there is no triangle, the graph stays unchanged. Running this for C(n,2) steps gives the terminal law on graphs, and expectation and probability are taken with respect to it. Writing normalizedLeave(G) = |E(G)| / n^(3/2) and sharpConstant c = 1/(2√2), the theorem asserts: first, the expected value of (normalizedLeave(G) − c)² tends to 0; second, for every ε > 0, the probability that |normalizedLeave(G) − c| > ε tends to 0; and third, the expected number of edges of the terminal graph divided by n^(3/2) tends to c.

The goal is OAI.SharpTerminalLeave.sharp_terminal_leave.

Significance

The three conclusions record mean-square concentration, concentration in probability, and the limiting normalized expectation. The exact leading constant is part of the target. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Early evolution estimates need to remain informative near termination, where triangles become scarce. A high-probability estimate alone need not control the second moment required here.

Formalization scope

Graphs are finite sets of pairs from Fin n, with transitions given by probability mass functions. Running for the initial edge count guarantees that the absorbing terminal law is reached. Expectations are finite sums and all limits are along natural $n$ tending to infinity.

The shared definitions are supplied by TriangleRemoval. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, The sharp terminal leave in random triangle removal, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

High probability under independent coordinate sampling need not give a family any closure under unions. Discrete convexity asks whether a bounded number of its members nevertheless cover most sets in the stronger sense of inexpensive containment certificates. The source is OpenAI's September 2026 manuscript.

Setting

On Bernoulli product space $2^{[N]}$, each coordinate is present independently with probability $p$. For a family $D$, the exceptional family $E_k(D)$ consists of sets contained in no union of $k$ members of $D$. A family is $p$-small when it has containment generators with total cost at most $1/2$.

Formalization targets

$$\mu_p(D)\ge1-2^{-75}\quad\Longrightarrow\quad E_{2^{75}}(D)\text{ is }p\text{-small}.$$

For every positive integer N, every density p with 0<p<1, and every family D of subsets of the ground set {0,...,N-1} (an arbitrary family, with no monotonicity assumption), if the product measure of D under independent Bernoulli(p) coordinates, namely the sum over s in D of p^|s|(1-p)^(N-|s|), is at least 1 - 1/2^75, then the family of exceptional sets is small. Here the exceptional family for k=2^75 consists of all subsets S of the ground set that are contained in no union of k members of D, where the k members are given as an arbitrary tuple of exactly k entries of D, repeats allowed and with no disjointness required. A family A is small at density p if there is a family G of generator sets that covers A, meaning every member of A contains some member of G, and whose cost, the sum over I in G of p^|I|, is at most 1/2.

The goal is OAI.TalagrandDiscreteConvexity.talagrand_discrete_convexity.

Significance

The conclusion supplies explicit containment witnesses at the original density. A small probability for the exceptional event alone would not provide such a cover. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

The family is arbitrary, so monotonicity cannot be used as an extra hypothesis. The same universal number of unions must work for all dimensions and all densities strictly between zero and one.

Formalization scope

Lean uses finite families of finite subsets of Fin N, with $N\ge1$ and $0<p<1$. A tuple has exactly $2^{75}$ entries; repetitions and overlaps are allowed. The cover cost counts each generator once. The separate two-union density-loss corollary is outside this goal.

The shared definitions are supplied by TalagrandDiscreteConvexity. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, Talagrand’s discrete-convexity conjecture, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

An increasing property of a random set can be certified by small subsets. Fractional certificates allow weight to be spread across many subsets, so comparing them with ordinary certificates measures the cost of removing this relaxation. The source is OpenAI's September 2026 manuscript.

Setting

A cover is a family of generators such that every member of the increasing family contains a generator. A generator of size $s$ costs $p^s$. An ordinary cover and a fractional cover both have budget $1/2$; a fractional cover assigns weights in $[0,1]$ and supplies total weight at least one inside each member. The expectation thresholds $q$ and $q_f$ are suprema of feasible parameters in $[0,1]$.

Formalization targets

$$q_f(\mathcal F)\le 25\cdot512^4\,q(\mathcal F).$$

For a finite nonempty ground type α and a family F of subsets of α that is nonempty, is not the entire power set, and is increasing (any superset of a member of F is again in F), the fractional threshold qf(F) is at most 25·512⁴ times the integral threshold q(F). Here q(F) is the supremum of those p in [0,1] for which F is small: some family G of sets covers F, meaning every H in F contains a member of G, with total cost Σ_{S∈G} p^{|S|} at most 1/2. The fractional threshold qf(F) is the analogous supremum of p in [0,1] for which there is a weight function g from subsets of α to [0,1] such that every H in F has Σ_{S⊆H} g(S) ≥ 1 and the fractional cost Σ_S g(S)·p^{|S|} is at most 1/2.

The goal is OAI.TalagrandThreshold.talagrand_expectation_threshold_equivalence.

Significance

The comparison gives a dimension-independent bound with the same budget on both sides. It isolates certificate rounding from the separate question of locating the random-set threshold. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Replacing fractional weights independently can lose control of covering every member simultaneously. The constant must be independent of both ground-set size and the sizes of weighted sets.

Formalization scope

The ground type is finite and nonempty, and the family is nonempty, proper, and increasing. Costs are finite real sums and thresholds are real suprema. The exact constant in the published goal is retained; the objective is this inequality, not an unspecified equivalent comparison.

The shared definitions are supplied by TalagrandExpectationThreshold. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, Integral and fractional expectation thresholds are equivalent, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

Sampling costs can be measured by potential and gradient queries independently of the computation between them. This model isolates the information needed for a well-conditioned log-concave distribution. The source manuscript presents the surrounding research claim.

Setting

The admissible potentials V on ℝᵈ are C², satisfy V(0)=0 and ∇V(0)=0, and have Hessian between I and 2I. Their Gibbs law has density proportional to exp(−V). A measurable adaptive algorithm receives exact (V(x),∇V(x)) replies.

Formalization target

For the least query budget q(d) achieving total-variation error at most 1/10, prove

$$\forall\varepsilon>0\;\exists C,\quad q(d)\le Cd^\varepsilon\quad(d\ge2),$$

plus q(d)≥c log d eventually for some c>0, and optimal dimension exponent γ*=0.

The selected formal target is OAI.LogConcaveSampling.exact_source_main.

Significance and status

The target gives both a subpolynomial upper bound and a logarithmic lower bound. It leaves computation between queries unrestricted. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

The sampler must work uniformly across every admissible potential and use a deterministic query budget on every execution. A dimension-dependent condition number or merely expected budget would change the problem.

Formalization scope

Algorithms have measurable query/output maps driven by private randomness and finite transcripts. Query complexity lies in ℕ∞, retaining infeasibility as infinity. Total variation is the specified supremum-style bound on measurable sets, and the upper/lower comparisons use ENNReal.

Selected references

• OpenAI, Subpolynomial query complexity for well-conditioned log-concave sampling, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

Free probability treats bounded self-adjoint operators $X_1,\dots,X_n$ in a tracial von Neumann algebra as noncommuting random variables, and the free analogue of independence is freeness. Voiculescu introduced two candidate analogues of Shannon entropy for such tuples. The microstates free entropy $\chi(X)$ measures how large the set of matrix tuples imitating the joint moments of $X$ is (Voiculescu 1994). The nonmicrostates free entropy $\chi^*(X)$ is built instead from free Fisher information, by integrating along the addition of free semicircular noise (Voiculescu 1998). The two agree for a single variable, and whether they agree in general is part of Voiculescu's unification problem (Voiculescu 2002, Sections 3.5 and 3.8). Guionnet stated the finite-entropy formulation explicitly: does $\chi(X)>-\infty$ imply $\chi(X)=\chi^*(X)$? (Guionnet 2004, Conjecture 7.1).

The question matters because $\chi$ carries the strongest structural consequences for von Neumann algebras (it is the tool behind results such as Ge's theorem that free group factors are prime, Ge 1996), while $\chi^*$ is far more computable. Equality would let analytic computations of $\chi^*$ transfer to $\chi$.

This mission asks for a machine-checked proof of Theorem 1.1 of an OpenAI preprint dated September 25, 2026 (source), which claims a tuple with $-\infty<\chi(X)\le\chi^*(X)-\tfrac12<\infty$. The preprint has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal is open.

Timeline

• 1991 — Voiculescu proves asymptotic freeness of independent GUE matrices (Invent. Math. 1991), the random-matrix input behind microstates.
• 1994 — Voiculescu defines the microstates free entropy $\chi$ (Invent. Math. 1994); Speicher develops the noncrossing cumulant calculus (Math. Ann. 1994).
• 1996 — Ge uses microstates entropy to prove that $L(F_2)$ is prime (PNAS 1996).
• 1998 — Voiculescu defines free Fisher information via conjugate variables and the nonmicrostates entropy $\chi^*$ (Invent. Math. 1998).
• 2002–2004 — Voiculescu's survey lists the unification problem (Bull. LMS 2002); Guionnet states the finite-entropy equality conjecture (Probab. Surv. 2004).
• 2003 — Biane, Capitaine and Guionnet prove $\chi\le\chi^*$ in general (Invent. Math. 2003).
• 2017–2020 — Equality is established for regular convex potentials by Dabrowski (arXiv:1604.06420) and Jekel (Anal. PDE 2020).
• 2024 — Jekel and Pi give an elementary proof of $\chi\le\chi^*$, including the conditional version (Doc. Math. 2024).
• 2026 — The OpenAI preprint claims a strict gap with both entropies finite (Theorem 1.1, p. 2).

Setting

Let $M$ be a von Neumann algebra with a faithful normal tracial state $\tau$, and $X=(X_1,\dots,X_n)$ a tuple of self-adjoint elements of $M$.

Microstates. For $R>0$, $m\in\mathbb N$, $\varepsilon>0$ and a matrix size $d$, let $\Gamma_R(X;m,d,\varepsilon)$ be the set of $n$-tuples of self-adjoint $d\times d$ complex matrices with operator norms at most $R$ whose normalized traces $d^{-1}\mathrm{Tr}$ of all words of length $\le m$ are within $\varepsilon$ of the corresponding $\tau$-moments of $X$. Volume is Lebesgue measure for the unnormalized Hilbert–Schmidt inner product. Then

$$\chi_R(X)=\inf_{m,\varepsilon}\ \limsup_{d\to\infty}\Bigl[d^{-2}\log\mathrm{Vol}\,\Gamma_R(X;m,d,\varepsilon)+\tfrac n2\log d\Bigr],\qquad \chi(X)=\sup_{R>0}\chi_R(X).$$

Free Fisher information. Vectors $\xi_1,\dots,\xi_n$ in the $L^2(\tau)$-closure of polynomials in $X$ are conjugate variables if $\tau(\xi_i P(X))=(\tau\otimes\tau)((\partial_iP)(X))$ for every noncommutative polynomial $P$, where $\partial_i$ is the free difference quotient. Then $\Phi^*(X)=\sum_i\|\xi_i\|_2^2$, or $+\infty$ if no conjugate variables exist.

Nonmicrostates entropy. With $S=(S_1,\dots,S_n)$ a standard free semicircular family free from $X$,

$$\chi^*(X)=\frac n2\log(2\pi e)+\frac12\int_0^\infty\Bigl(\frac n{1+s}-\Phi^*(X+\sqrt s\,S)\Bigr)\,ds .$$

Formalization targets

Goal: Theorem 1.1 (p. 2)

There exist $n\ge2$ and a bounded self-adjoint tuple $X$ in a von Neumann algebra with faithful normal tracial state such that

$$-\infty<\chi(X)\le\chi^*(X)-\tfrac12<\infty .$$

The Lean goal OAI.FiniteEntropySeparation.main asserts exactly this, with the semicircular family $S$ required to lie in the same algebra.

Significance

The result itself. The theorem answers the finite-entropy equality question negatively: finiteness of $\chi$ does not force $\chi=\chi^*$, so the matrix-approximation and Fisher-information definitions are genuinely different invariants even in the finite regime. Known equality results therefore cannot be extended by finiteness alone; any equality theorem must use structure such as convexity of a potential. The preprint notes that it does not settle the question for each fixed small number of variables.

Formalizing it. No formal definitions of free entropy, free Fisher information or free semicircular systems are known to exist in a proof assistant. A complete development would formalize both entropies, the comparison $\chi\le\chi^*$ in the form needed, Gaussian asymptotic freeness, cumulant calculus and matrix-volume estimates, all reusable across free probability.

Difficulty

Both entropies are hard to compute for any non-free tuple, and the gap must survive two limits that interact badly: the $\limsup$ over matrix size in $\chi$ and the integral over noise time in $\chi^*$. The preprint's tuple couples free semicirculars with a commuting discrete variable $Y$ that creates spectral blocks; after perturbing by small semicircular noise, $\chi$ is finite (Lemma 4.2, p. 9). The analytic side needs a Fisher-information bound in terms of higher cumulants (Proposition 3.2, p. 6), which makes $\chi^*$ nearly Gaussian at a suitable noise scale, while the matrix side must show that microstates, after GUE evolution, retain detectable block structure that independent GUE matrices of the same variances lack (Lemma 6.1, p. 12). Matching the two requires a finite-time entropy-production comparison along one fixed sequence of matrix laws (Lemma 5.1, p. 10); a naive application of $\chi\le\chi^*$ loses exactly the deficit being sought.

Formalization scope

• The algebra is a VonNeumannAlgebra H on a complex Hilbert space $H$; the trace is a vector state given by a unit vector that is tracial on $M$ and separating for $M$ (so the state is faithful and normal).
• $X$ and $S$ are Fin n-indexed self-adjoint elements of $M$. FreeStandardNoise requires each $S_i$ to have the semicircle moments (Catalan numbers) and the unital algebras generated by $X$ and by each $S_i$ to be free.
• Conjugate systems are vectors in the closed span of word vectors satisfying the derivative-moment identities; free Fisher information is an infimum in ℝ≥0∞, equal to $\infty$ when no conjugate system exists.
• $\chi^*$ is an EReal built from the positive and negative parts of the integrand as lower Lebesgue integrals over $(0,\infty)$.
• $\chi$ uses explicit real coordinates for Hermitian matrices that make the Euclidean volume equal to Hilbert–Schmidt volume, matrix sizes $d+1$ to avoid $d=0$, and EReal logarithms (volume zero gives $-\infty$).
• The finiteness conditions are part of the conclusion, so a degenerate witness with $\chi=-\infty$ or $\chi^*=\infty$ does not satisfy the goal.

Selected references

• OpenAI, A finite-entropy separation of microstates and nonmicrostates free entropy, OpenAI Math Release preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-finite-entropy-separation-of-microstates-and-nonmicrostates-free-entropy-September-25-2026/paper.pdf
• D. Voiculescu, The analogues of entropy and of Fisher's information measure in free probability theory. II, Invent. Math. 118 (1994), 411–440. https://doi.org/10.1007/BF01231539
• D. Voiculescu, The analogues of entropy and of Fisher's information measure in free probability theory. V, Invent. Math. 132 (1998), 189–227. https://doi.org/10.1007/s002220050222
• D. Voiculescu, Free entropy, Bull. London Math. Soc. 34 (2002), 257–278. https://doi.org/10.1112/S0024609301008992
• A. Guionnet, Large deviations and stochastic calculus for large random matrices, Probab. Surv. 1 (2004), 72–172. https://doi.org/10.1214/154957804100000033
• P. Biane, M. Capitaine, A. Guionnet, Large deviation bounds for matrix Brownian motion, Invent. Math. 152 (2003), 433–459. https://doi.org/10.1007/s00222-002-0281-4
• D. Jekel, J. Pi, An elementary proof of the inequality χ ≤ χ for conditional free entropy*, Doc. Math. 29 (2024), 1085–1124. https://doi.org/10.4171/DM/969
• D. Jekel, An elementary approach to free entropy theory for convex potentials, Anal. PDE 13 (2020), 2289–2374. https://doi.org/10.2140/apde.2020.13.2289
• D. Voiculescu, Limit laws for random matrices and free products, Invent. Math. 104 (1991), 201–220. https://doi.org/10.1007/BF01245072

Motivation

The quantum Heisenberg ferromagnet is the basic quantum model of a magnet: a quantum spin sits at each site of the lattice $\mathbb Z^d$ and neighbouring spins prefer to align. Its Hamiltonian is invariant under simultaneous rotation of all spins, so at zero external field no direction is preferred. Spontaneous magnetization asks whether an infinite-volume equilibrium state at positive temperature can nevertheless choose a direction, giving a nonzero expected spin at a single site. For classical spins and for quantum antiferromagnets this was settled decades ago; for the quantum ferromagnet in $d\ge3$ it has been a standard open problem of mathematical physics, recorded by Lieb in 1999 and again by Seiringer in 2025.

Timeline

• 1928–1930. Heisenberg proposes the exchange model of ferromagnetism (doi:10.1007/BF01328601); Bloch's spin-wave picture predicts the low-temperature reduction of magnetization (doi:10.1007/BF01339661).
• 1956. Dyson develops the theory of interacting spin waves and its thermodynamics (doi:10.1103/PhysRev.102.1217, doi:10.1103/PhysRev.102.1230).
• 1966. Mermin and Wagner exclude positive-temperature ferro- and antiferromagnetism for finite-range isotropic Heisenberg models in $d=1,2$ (doi:10.1103/PhysRevLett.17.1133).
• 1967. Haag, Hugenholtz and Winnink formulate equilibrium of infinite systems through the KMS condition (doi:10.1007/BF01646342).
• 1976. Fröhlich, Simon and Spencer prove low-temperature ordering for classical continuous-spin models in $d\ge3$ via infrared bounds (doi:10.1007/BF01608557); Powers relates the Heisenberg model to random walks on the permutation group (doi:10.1007/BF00398374).
• 1978. Dyson, Lieb and Simon prove ordering for quantum antiferromagnets (spin $\ge1$ in $d\ge3$, spin $\tfrac12$ in high dimension) and explain why reflection positivity gives no ferromagnetic infrared bound (doi:10.1007/BF01106729).
• 1988. Kennedy, Lieb and Shastry prove ground-state Néel order for the spin-$\tfrac12$ antiferromagnet on $\mathbb Z^3$ (doi:10.1007/BF01023854).
• 1991–1994. Conlon–Solovej random-walk representations and free-energy upper bound (doi:10.1007/BF01057876); Tóth's improved pressure bound (1993, doi:10.1007/BF00739568); Nachtergaele's general-spin stochastic-geometric representations (1994, doi:10.1007/978-94-015-8326-8_14).
• 1999. Lieb poses ferromagnetic long-range order as Problem A of the Mathematical Physics Open Problems list.
• 2015. Correggi, Giuliani and Seiringer prove the spin-wave free-energy asymptotics in $d=3$ (arXiv:1312.7873).
• 2020. Björnberg, Fröhlich and Ueltschi analyse the loop representation on the complete graph (arXiv:1811.12834).
• 2025–2026. Seiringer records the ordering problem in an Oberwolfach report; Klippel proves the free-energy asymptotics in $d=2$ (arXiv:2608.25506).

The source of this mission is an OpenAI preprint dated September 24, 2026, which claims a proof of spontaneous magnetization for every spin and every $d\ge3$.

Setting

Fix $d\ge3$ and a spin $S\in\{\tfrac12,1,\tfrac32,\dots\}$; write $\ell=2S$. Each site carries $\mathbb C^{2S+1}$ with basis $(e_m)_{m=-S}^{S}$ and

$$S^ze_m=me_m,\qquad S^+e_m=\sqrt{S(S+1)-m(m+1)}\,e_{m+1},\qquad S^-=(S^+)^*,$$

$S^x=(S^++S^-)/2$, $S^y=(S^+-S^-)/(2i)$. For finite $\Lambda\subset\mathbb Z^d$ the free-boundary Hamiltonian is

$$H_\Lambda=-\sum_{\{x,y\}\subset\Lambda,\ |x-y|_1=1}\ \bigl(S^x_xS^x_y+S^y_xS^y_y+S^z_xS^z_y\bigr),$$

each unordered edge counted once. The quasi-local algebra $\mathcal A$ is the norm completion of the local matrix algebras $\bigotimes_{x\in F}M_{2S+1}(\mathbb C)$. The dynamics is $\tau_t(A)=\lim_n e^{itH_{\Lambda_n}}Ae^{-itH_{\Lambda_n}}$ along the boxes $\Lambda_n=[-n,n]^d$.

A state is a positive linear functional $\omega$ on $\mathcal A$ with $\omega(1)=1$. It is $\beta$-KMS if for all $A,B\in\mathcal A$ there is a bounded function $F$, continuous on $\{0\le\operatorname{Im}z\le\beta\}$ and analytic inside, with

$$F(t)=\omega(A\,\tau_t(B)),\qquad F(t+i\beta)=\omega(\tau_t(B)\,A)\qquad(t\in\mathbb R).$$

It is translation invariant if $\omega\circ T_x=\omega$ for all $x\in\mathbb Z^d$.

Formalization targets

Goal: Theorem 1.1

$$\exists\,\beta_0>0\ \ \forall\,\beta\ge\beta_0\ \ \exists\,\omega\ \text{translation invariant, }\beta\text{-KMS for }\tau,\quad \omega(S_0^z)\ \ge\ \frac S4.$$

The Lean statement OAI.Heisenberg.spontaneous_magnetization also asserts that the box limits defining $\tau_t(A)$ converge for every $t$ and $A$ (the standing fact the theorem relies on). The goal is open on the platform.

Significance

The theorem gives an equilibrium state of the zero-field model, at every sufficiently low positive temperature, that breaks the rotation symmetry: a translation-invariant KMS state with one-site magnetization at least $S/4$. It addresses the ordering problem in its spontaneous-magnetization formulation; the volume-averaged finite-volume two-point criterion in Seiringer's account is a different formulation that the paper does not use. For $S=\tfrac12$ the Matsubara–Matsuda correspondence turns the ordered state into a hard-core boson state with off-diagonal long-range order, a lattice analogue of Bose–Einstein condensation.

The result is stated in an OpenAI preprint; it has not been peer reviewed, and there is no machine-checked proof. A formal proof would certify a long argument (loop representation, stable-polynomial pin test, Markov-walk return estimates, flow constructions and the KMS limit) whose individual steps are each delicate.

Difficulty

The classical route to continuous-symmetry breaking, infrared bounds from reflection positivity, fails for the quantum ferromagnet: as Dyson, Lieb and Simon explained, it does not yield the needed Duhamel bound. Spin-wave free-energy asymptotics, now known in $d=2,3$, control correlations only on a temperature-dependent finite length scale, not at all scales at a fixed temperature. Loop representations give positive weights, but positivity alone does not imply ordering: one must show that an interior cycle rarely avoids pins placed on the boundary, uniformly in the volume. Finally, a KMS state must be produced for the zero-field dynamics itself, so the symmetry-breaking field used in finite volume has to be removed while both KMS boundary conditions survive.

Formalization scope

• Sites are Fin d → ℤ; a spin level is Fin (ℓ+1) with magnetic quantum number $k-\ell/2$. The Hilbert space is $\ell^2$ of finitely supported configurations Site d →₀ Fin (ℓ+1), and the quasi-local algebra is the norm closure of the star-algebra generated by single-site matrix units on it (a faithful copy of the abstract quasi-local algebra).
• hamiltonian d ℓ Λ sums over nearest-neighbour pairs ($\ell^1$ distance one) with one orientation per edge; box d n is $[-n,n]^d$; dynamics is the limUnder of the box dynamics, and DynamicsConverges asserts that these limits exist.
• State packages a continuous linear functional with $\omega(1)=1$ and $\omega(A^*A)\ge0$; IsKMS β ω requires $0<\beta$ and, for every $A,B$, a bounded $F$ continuous on the closed strip, complex-differentiable on the open strip, with the two boundary identities.
• The conclusion reads $\operatorname{Im}\omega(S^z_0)=0$ and $\operatorname{Re}\omega(S^z_0)\ge\ell/8$.

A complete development needs quantum spin systems on $\mathbb Z^d$, Lieb–Robinson-type existence of infinite-volume dynamics, KMS states, and the probabilistic loop machinery. The quantum-spin and KMS infrastructure is reusable for other lattice models (including the Bloch-law missions of this family). Contributions formalizing the existence of the dynamics, Proposition 2.2 (spin-to-loop representation), Proposition 3.1 (simultaneous pin test) and Proposition 8.2 (vanishing-field limit) are welcome.

Selected references

• OpenAI, Spontaneous magnetization in the quantum Heisenberg ferromagnet, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Spontaneous-magnetization-in-the-quantum-Heisenberg-ferromagnet-September-24-2026/paper.pdf
• E. H. Lieb, Long Range Order for the Quantum Heisenberg Model, Mathematical Physics Open Problems, Problem A, 1999. https://web.math.princeton.edu/~aizenman/OpenProblems_MathPhys/9901.HeisenbergFerr.html
• R. Seiringer, The Heisenberg Ferromagnet: A Dilute Bose Gas in Disguise, Oberwolfach Report 7/2025. https://doi.org/10.4171/OWR/2025/7
• N. D. Mermin, H. Wagner, Absence of Ferromagnetism or Antiferromagnetism in One- or Two-Dimensional Isotropic Heisenberg Models, Phys. Rev. Lett., 1966. https://doi.org/10.1103/PhysRevLett.17.1133
• J. Fröhlich, B. Simon, T. Spencer, Infrared Bounds, Phase Transitions and Continuous Symmetry Breaking, Comm. Math. Phys., 1976. https://doi.org/10.1007/BF01608557
• F. J. Dyson, E. H. Lieb, B. Simon, Phase Transitions in Quantum Spin Systems with Isotropic and Nonisotropic Interactions, J. Stat. Phys., 1978. https://doi.org/10.1007/BF01106729
• M. Correggi, A. Giuliani, R. Seiringer, Validity of the Spin-Wave Approximation for the Free Energy of the Heisenberg Ferromagnet, Comm. Math. Phys., 2015. https://arxiv.org/abs/1312.7873
• B. Nachtergaele, Y. Ogata, R. Sims, Propagation of Correlations in Quantum Lattice Systems, J. Stat. Phys., 2006. https://arxiv.org/abs/math-ph/0603064
• J. Borcea, P. Brändén, T. M. Liggett, Negative Dependence and the Geometry of Polynomials, J. Amer. Math. Soc., 2009. https://arxiv.org/abs/0707.2340
• R. Haag, N. M. Hugenholtz, M. Winnink, On the equilibrium states in quantum statistical mechanics, Comm. Math. Phys., 1967. https://doi.org/10.1007/BF01646342

Motivation

Bose–Einstein condensation (BEC) means that a single one-particle state carries a macroscopic fraction of a many-boson system. It was predicted for the ideal gas by Bose and Einstein (1924–1925) and is observed in dilute atomic gases, but for interacting particles in the thermodynamic limit there was no rigorous proof, even in the ground state. The Penrose–Onsager criterion (Phys. Rev. 1956) identifies condensation with a macroscopic eigenvalue of the one-particle density matrix. Energy asymptotics of the dilute gas are now known to second order, but they do not determine single-orbital occupation, since the one-particle spectral gap closes as the volume grows. Lieb and Yngvason explicitly separated the condensation question from their energy theorem, and Solovej's 2025 survey lists fixed-density ground-state condensation as a major problem in the field (C. R. Physique 2025, Section 5).

This mission asks for a formal proof of ground-state condensation for the dilute three-dimensional hard-sphere Bose gas, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

• 1924–1925 — Bose and Einstein predict condensation in the ideal Bose gas (Z. Phys. 1924).
• 1947 — Bogoliubov's theory assumes a macroscopically occupied zero mode.
• 1956 — Penrose and Onsager's density-matrix criterion for condensation.
• 1957 — Dyson's bounds on the hard-sphere ground-state energy (Phys. Rev. 1957); Lee, Huang and Yang predict depletion of order $\sqrt{\rho a^3}$ (Phys. Rev. 1957).
• 1998 — Lieb and Yngvason prove the leading dilute energy asymptotics $4\pi\rho a$ (PRL 1998).
• 2002 — Lieb and Seiringer prove BEC for trapped gases in the Gross–Pitaevskii limit (PRL 2002).
• 2020 — Deuchert and Seiringer: homogeneous Gross–Pitaevskii limit at positive temperature (ARMA 2020).
• 2021–2026 — Fournais's length scales for BEC (EMS 2021); Fournais–Solovej's Lee–Huang–Yang lower bound including hard cores (Invent. Math. 2023); Basti et al.'s matching upper bound for hard spheres (arXiv:2603.13084); results of Chong–Liang–Nam (JFA 2026) and Junge (arXiv:2603.20776) in joint dilute and large-volume limits.
• September 2026 — The OpenAI preprint claims condensation at fixed density and fixed exclusion distance (Theorem 1.1, p. 3).

Setting

Let $\Lambda_L=(\mathbb R/L\mathbb Z)^3$ be the flat torus with torus distance $d_L$. For $N$ particles and exclusion distance $a>0$, the allowed configurations are

$$\Omega_{N,L,a}=\{X\in\Lambda_L^N:\ d_L(x_i,x_j)>a\ \text{for } i<j\}.$$

The hard-sphere Hamiltonian is the operator of the Dirichlet form $q[f]=\sum_{i=1}^N\int|\nabla_if|^2$ on $H^1_0(\Omega_{N,L,a})$ restricted to symmetric (bosonic) functions; wave functions vanish on forbidden configurations, and $a$ is the scattering length. A ground vector is a normalized bosonic minimizer of $q$. For a normalized bosonic $\Psi$, the condensate fraction in the constant orbital $\varphi_0=L^{-3/2}$ is

$$B(\Psi)=\frac{\langle\varphi_0,\Gamma^{(1)}_\Psi\varphi_0\rangle}{N}=\frac1{L^3}\int_{\Lambda_L^{N-1}}\Bigl|\int_{\Lambda_L}\Psi(x,Y)\,dx\Bigr|^2dY\in[0,1],$$

and for a density operator it is defined by linearity. The gas parameter is $\rho a^3$ with $\rho$ the density.

Formalization targets

Goal: Theorem 1.1 and Corollary 1.2 (p. 3)

There are absolute constants $\varepsilon_0,c_0>0$ such that, for all $a,\rho>0$ with $\rho a^3<\varepsilon_0$ and every sequence $N_k\to\infty$, $L_k\to\infty$ with $N_k/L_k^3\to\rho$:

1. for every choice of (possibly complex) bosonic ground vectors $\Psi_k$, $\ \liminf_k B(\Psi_k)\ge c_0$;
2. for every sequence of density operators $T_k$ supported on the bosonic ground spaces, the same bound holds for the occupation of $T_k$ (in particular for the normalized ground-space projections).

The constant $c_0$ does not depend on the gas parameter in this range.

Significance

The result itself. It is a proof of macroscopic condensation in an interacting continuum Bose gas with fixed density and fixed hard core, in the thermodynamic limit, uniformly over all ground states including degenerate ground spaces. Previous rigorous results let the gas parameter tend to zero with the volume, or concerned traps, scaling limits, or positive-temperature settings with different potentials. The theorem gives a positive fraction only; it does not reach the Lee–Huang–Yang depletion law.

Formalizing it. The statement involves Sobolev spaces with Dirichlet conditions on a configuration space of the torus, bosonic symmetry, density operators, and partial traces, none of which are packaged in Mathlib; the Lean development builds them concretely. The proof uses killed Brownian motion, percolation-type path constructions, and second-moment arguments. No machine-checked statement of BEC for an interacting system is known.

Difficulty

Energy estimates alone cannot detect occupation of the constant orbital, because the cost of moving particles out of it is of order $L^{-2}$ per particle and vanishes in the limit. One must show directly that a typical ground state correlates distant parts of the box. The preprint compares a tagged particle's position in distant cells by moving trajectories along random lattice routes; multiplying local comparison costs along a route loses a factor at every step, so instead it averages over random routes and bounds the second moment of the averaged likelihood, where exact cancellation of normalizers leaves a cost depending only on mutual encounters of two routes (Introduction, pp. 4–5; Section 8). A separate phase argument passes from $|\Psi|$ to complex $\Psi$ (Lemma 2.3, p. 9).

Formalization scope

• Configurations are Fin N → Fin 3 → AddCircle L; the allowed set uses the Euclidean torus distance with strict inequality a < dist.
• The form domain dirichletDomain is the closure, in $L^2\times(L^2)^{3N}$, of jets of smooth compactly supported test functions with support in the allowed set; energy is the sum of squared $L^2$ norms of the partial derivatives. IsGroundVector means: in the domain, bosonic (a.e. permutation invariant), normalized, and of minimal energy among such vectors.
• occupation is exactly $B(\Psi)$; mixedOccupation T is the trace of $T$ compressed by the bounded map $\Psi\mapsto L^{-3/2}\int\Psi(x,\cdot)\,dx$. GroundSupported T says every unit vector in $(\ker T)^\perp$ is (the first component of) a ground vector.
• Density operators are positive bounded operators with trace one, computed in a fixed Hilbert basis.
• Hypotheses on the sequences are only those of the source; the ground-vector hypothesis is required for every index $k$, which loses nothing since $\liminf$ depends only on tails.

Selected references

• OpenAI, Ground-state condensation in the dilute hard-sphere gas, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Ground-state-condensation-in-the-dilute-hard-sphere-gas-September-24-2026/paper.pdf
• O. Penrose, L. Onsager, Bose–Einstein condensation and liquid helium, Phys. Rev. 104 (1956). https://doi.org/10.1103/PhysRev.104.576
• F. J. Dyson, Ground-state energy of a hard-sphere gas, Phys. Rev. 106 (1957). https://doi.org/10.1103/PhysRev.106.20
• T. D. Lee, K. Huang, C. N. Yang, Eigenvalues and eigenfunctions of a Bose system of hard spheres and its low-temperature properties, Phys. Rev. 106 (1957). https://doi.org/10.1103/PhysRev.106.1135
• E. H. Lieb, J. Yngvason, Ground state energy of the low density Bose gas, Phys. Rev. Lett. 80 (1998). https://doi.org/10.1103/PhysRevLett.80.2504
• E. H. Lieb, R. Seiringer, Proof of Bose–Einstein condensation for dilute trapped gases, Phys. Rev. Lett. 88 (2002). https://doi.org/10.1103/PhysRevLett.88.170409
• S. Fournais, J. P. Solovej, The energy of dilute Bose gases II: the general case, Invent. Math. (2023). https://doi.org/10.1007/s00222-022-01175-0
• A. Deuchert, R. Seiringer, Gross–Pitaevskii limit of a homogeneous Bose gas at positive temperature, Arch. Ration. Mech. Anal. (2020). https://doi.org/10.1007/s00205-020-01489-4
• J. P. Solovej, Mathematical physics of dilute Bose gases, C. R. Physique (2025). https://doi.org/10.5802/crphys.247
• G. Basti, M. Brooks, S. Cenatiempo, A. Olgiati, B. Schlein, The Lee–Huang–Yang energy for a dilute gas of hard spheres: an upper bound, arXiv:2603.13084 (2026). https://arxiv.org/abs/2603.13084v2

Motivation: a dimension saving for the binary coordinate sweep

The Thorp shuffle cuts a deck in half, pairs cards in corresponding positions, and lets an independent fair coin order each pair before the pairs are interleaved. On $N=2^d$ cards, removing the deterministic rotation of coordinates turns $d$ physical shuffles into one binary coordinate sweep: in each coordinate direction, in order, every pair of positions differing in that coordinate is independently swapped with probability $1/2$. After one sweep each card is uniform, but the joint permutation retains dependence because cards share switches.

By finite-group Fourier analysis (Diaconis–Shahshahani 1981), fast mixing of the whole deck follows from a power saving $\|K_\lambda\|_{\rm op}\le D_\lambda^{-g}$ for the sweep in every irreducible representation $\lambda$ of $S_N$. The source obtains this saving by first controlling a perturbed sweep, in which each line permutation is mostly uniform, conditionally on prescribed trajectories of some cards, and then transferring the estimate analytically to the binary sweep.

Timeline

• 1973 — Thorp introduces the shuffle in a study of nonrandom shuffling in Faro (Thorp, JASA 1973).
• 1981 — Diaconis and Shahshahani introduce the Fourier upper-bound method for random walks on $S_n$ (Z. Wahrsch. 1981).
• 2005/2008 — Morris proves $O(d^{44})$ physical shuffles for $N=2^d$ with a chameleon process that conditions on the trajectory of an occupied set (SIAM J. Comput. 2008); Montenegro and Tetali sharpen it to $O(d^{29})$ (2006).
• 2009 — Morris proves $O((\log N)^4)$ for every even $N$ (Ann. Probab. 2009); Morris, Rogaway and Stegers analyze selected-card Thorp marginals for small-domain encryption (CRYPTO 2009).
• 2012 — Hoang, Morris and Rogaway use a conditional squared-discrepancy calculation for the swap-or-not shuffle (CRYPTO 2012).
• 2013 — Morris proves $O(d^3)$ for $N=2^d$, exposing complete labeled trajectories successively (CPC 2013).
• 2014–2015 — Czumaj and Vöcking: nearly uniform joint positions of a $(1-\varepsilon)$ fraction of the cards after $O(d^2)$ shuffles (ICALP 2014); Czumaj, switching networks (STOC 2015).
• 2026 — The OpenAI preprint Conditional coordinate sweeps and analytic transfer (OpenAI Math Release, September 26, 2026) proves the binary sweep contraction below, giving $t_{\rm mix}(d)=\Theta(d)$ physical shuffles. The preprint has not been peer reviewed and its results are not formally verified.

Setting

Positions are binary strings $\{0,1\}^d$, $N=2^d$ (Lean: Slot d := Fin d → Bool). For a coordinate $j$, a layer flips bit $j$ of a position $x$ according to a fair coin attached to the edge $\{x,x+e_j\}$; the binary sweep applies the layers for $j=1,\dots,d$ in order, with all coins independent (Lean: binarySweep, binaryLaw d its law on $S_N$). For an irreducible unitary representation $\rho_\lambda$ of $S_N$ of dimension $D_\lambda$, the sweep operator is

$$K_\lambda=\mathbb E_{g\sim B_N}\rho_\lambda(g).$$

Write $B_N^{*w}$ for the law of $w$ independent sweeps and $\|\mu-\nu\|_{\rm TV}=\tfrac12\sum_g|\mu(g)-\nu(g)|$.

For the conditional estimate, an ordered product grid is $\Omega=\Omega_1\times\dots\times\Omega_b$ with each $|\Omega_j|=m_j$ a power of two in $[R,R^2]$; a sweep permutes the lines parallel to coordinate $1$, then coordinate $2$, and so on, each line independently with law $L_m(z)=(1-z)U_m+zB_m$. A family $\mathcal H$ of $h$ prescribed trajectories (disjoint at every layer) is conditioned on; the remaining random bijection of the $s-h$ free slots has average $K^{\mathcal H}_\lambda$ in each irreducible $\lambda\vdash s-h$, with line cost $C(\mathcal H)=\sum_{L}\log\bigl(|L|^{h_L}/(|L|)_{h_L}\bigr)$.

Formalization targets

Milestone: conditional sweep moment estimate (Theorem 3.1)

There are a power of two $R\ge2$, an integer $q\ge1$ and $z_*>0$ such that for every grid, every feasible family $\mathcal H$, every $z\in[0,z_*]$ and every irreducible $\lambda\vdash s-h$,

$$\log\|K^{\mathcal H}_\lambda\|_{2q}^{2q}\le -c(s)\log D_\lambda+e(s)\,h\log s-C(\mathcal H),$$

with $c(s)=c_0+1/\sqrt{\log s}$, $e(s)=e_0-1/\sqrt{\log s}$, $c_0=e_0=10^{-4}$, and $\log 0=-\infty$.

Goal: binary sweep contraction (Theorem 1.1)

There are absolute constants $g>0$ and $d_0$ such that for all $d\ge d_0$ and every irreducible unitary representation of $S_{2^d}$ of dimension $D$,

$$\|K_\lambda\|_{\rm op}\le D^{-g};$$

the sign representation is annihilated, $\sum_g B_N(g)\,\mathrm{sgn}(g)=0$; and there is an absolute integer $w$ such that

$$\sup_{\tau\in S_N}\bigl\|B_N^{*w}(\cdot\,\tau^{-1})-U_N\bigr\|_{\rm TV}\xrightarrow[d\to\infty]{}0 .$$

The goal is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. Since one binary sweep is exactly $d$ physical shuffles, the goal gives $O(d)$ physical shuffles for mixing from every starting deck, and the support obstruction (Proposition 1.2: $t$ shuffles reach at most $2^{tN/2}$ permutations) gives the matching lower bound $2d-O(1)$; thus $t_{\rm mix}(d)=\Theta(d)$, improving Morris 2013. The power saving in every irreducible representation is a stronger, reusable statement: it controls any number of further sweeps and any function of the permutation through Fourier analysis.

Formalizing it. The goal is stated for explicit finite objects (coins, sweeps, Fourier operators on $\mathbb C^D$), with existential constants only. A formal proof would certify optimal-order mixing for the Thorp sweep. The conditional estimate (Theorem 3.1) is formalized separately and is the natural intermediate milestone.

Difficulty

The obvious induction—split the coordinates and multiply child bounds—breaks because revealing card paths changes the conditional law of the line permutations, and the induction must be stable when more paths are revealed. The source handles this with the line cost $C(\mathcal H)$, which records the exact cost of prescribing positions without replacement. A second obstacle is that the conditional estimate is only available for mostly-uniform lines ($z$ small), while the Thorp sweep is the binary case $z=1$; for a fixed grid the sweep operator is a matrix polynomial in $z$ whose behavior at $z=1$ is not controlled by real-segment bounds alone. Representations of very small "level" (first appearing on few tracked cards) need a separate sparse estimate.

Formalization scope

• Goal (binary_sweep_contraction_and_mixing): three conjuncts. BinaryContractionTarget: $\exists g>0\ \exists d_0\ \forall d\ge d_0\ \forall D$ and every irreducible representation $\rho$ of Equiv.Perm (Slot d) on EuclideanSpace ℂ (Fin D) preserving norms, the operator norm of $\sum_g \mathrm{binaryLaw}(g)\rho(g)$ is at most $D^{-g}$ (real power). Sign: for every $d>0$, $\sum_g \mathrm{binaryLaw}(g)\,\mathrm{sgn}(g)=0$. UniformSweepMixingTarget: $\exists w\ \forall\varepsilon>0\ \exists d_0\ \forall d\ge d_0\ \forall\tau$, total variation of the $w$-fold convolution power translated by $\tau$ from uniform is at most $\varepsilon$. Physical shuffles are not modelled; the statement is about sweeps.
• Milestone (conditional_main): grids are Grid with $b\ge1$ coordinates of $r\le\text{bits}_j\le2r$ ($R=2^r$); trajectories are Holes with disjointness at every layer and coordinate-respecting steps; feasibility means some line choices realize them; the residual bijection is identified with the stabilizer of the input holes via a fixed reference completion; representations are UnitaryIrrep of that stabilizer; the Schatten moment is $\mathrm{Re}\operatorname{Tr}((K^*K)^q)$; $z_*\le1/2$.
• The mapped item all_grid_moment is a parameter-explicit form of the same induction under numerical largeness hypotheses and a small-perturbation hypothesis, kept as a plain item.
• Infrastructure: Specht-module dimension estimates, branching and Pieri rules, signed Schur–Weyl decompositions, Schatten norms, and the subharmonic maximum principle; the analytic-transfer step is reusable for other families of averaging operators polynomial in a parameter.

Selected references

• E. O. Thorp, Nonrandom shuffling with applications to the game of Faro, J. Amer. Statist. Assoc. 68 (1973), 842–847. https://doi.org/10.1080/01621459.1973.10481434
• P. Diaconis and M. Shahshahani, Generating a random permutation with random transpositions, Z. Wahrsch. Verw. Gebiete 57 (1981), 159–179. https://doi.org/10.1007/BF00535487
• B. Morris, The mixing time of the Thorp shuffle, SIAM J. Comput. 38 (2008), 484–504. https://doi.org/10.1137/050636231
• R. Montenegro and P. Tetali, Mathematical aspects of mixing times in Markov chains, Found. Trends Theor. Comput. Sci. 1 (2006), 237–354. https://doi.org/10.1561/0400000003
• B. Morris, Improved mixing time bounds for the Thorp shuffle and L-reversal chain, Ann. Probab. 37 (2009), 453–477. https://doi.org/10.1214/08-AOP409
• B. Morris, Improved mixing time bounds for the Thorp shuffle, Combin. Probab. Comput. 22 (2013), 118–132. https://doi.org/10.1017/S0963548312000478
• B. Morris, P. Rogaway and T. Stegers, How to encipher messages on a small domain, CRYPTO 2009, LNCS 5677, 286–302. https://doi.org/10.1007/978-3-642-03356-8_17
• V. T. Hoang, B. Morris and P. Rogaway, An enciphering scheme based on a card shuffle, CRYPTO 2012, LNCS 7417, 1–13. https://doi.org/10.1007/978-3-642-32009-5_1
• A. Czumaj and B. Vöcking, Thorp shuffling, butterflies, and non-Markovian couplings, ICALP 2014, LNCS 8572, 344–355. https://doi.org/10.1007/978-3-662-43948-7_29
• A. Czumaj, Random permutations using switching networks, STOC 2015, 703–712. https://doi.org/10.1145/2746539.2746629
• A. Berele and A. Regev, Hook Young diagrams, combinatorics and representations of Lie superalgebras, Bull. Amer. Math. Soc. (N.S.) 8 (1983), 337–339. https://doi.org/10.1090/S0273-0979-1983-15110-8
• OpenAI, Conditional coordinate sweeps and analytic transfer, OpenAI Math Release preprint, September 26, 2026 (source; Theorem 1.1, p. 2; Theorem 3.1, p. 7). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Conditional-coordinate-sweeps-and-analytic-transfer-September-26-2026/main.pdf

Motivation: optimal-order mixing for the Thorp shuffle

The Thorp shuffle is a simple card-shuffling rule: cut a deck of $n$ cards into two equal halves, pair cards in corresponding positions, and let an independent fair coin decide the order within each pair when the pairs are interleaved. It is a standard test case for mixing-time methods and a building block in small-domain enciphering schemes. For $n=2^d$ every individual card is uniform after $d$ shuffles, but the joint order of all $n$ cards is much harder to control. Determining whether $O(d)=O(\log n)$ shuffles suffice to make the full permutation close to uniform was a long-standing question.

Timeline

• 1973 — Thorp introduces the model in a study of nonrandom shuffling in Faro (Thorp, JASA 1973).
• 2005/2008 — Morris proves the first polynomial-in-$d$ bound, $O(d^{44})$ shuffles for $n=2^d$, using evolving sets and a chameleon process (Morris, SIAM J. Comput. 2008).
• 2006 — Montenegro and Tetali sharpen this to $O(d^{29})$ by spectral-profile and evolving-set estimates (Montenegro–Tetali 2006, §6.4).
• 2009 — Morris introduces an entropy method based on card interactions and obtains $O(\log^4 n)$ for every even deck size (Morris, Ann. Probab. 2009).
• 2013 — Morris obtains $O(d^3)$ for dyadic decks (Morris, CPC 2013).
• 2026 — The OpenAI preprint Random-subspace tests and trace smoothing for coordinate sweeps (OpenAI Math Release, September 26, 2026) claims a uniform bound on a fixed Schatten moment of one coordinate sweep in the full regular representation, which yields total-variation mixing after an absolute number of sweeps, i.e. $O(d)$ physical shuffles. The preprint has not been peer reviewed and its result is not formally verified.

Setting

Index the $n=2^d$ positions by binary strings $x\in\mathbb F_2^d$ (in Lean, Card d := Fin d → Bool). One physical shuffle sends

$$(x_1,x_2,\dots,x_d)\longmapsto(x_2,\dots,x_d,\;x_1+\xi_{x_2,\dots,x_d})$$

with independent fair bits $\xi$ (Lean: step d ξ = rotate * pairSwitch ξ). After $d$ physical shuffles the rotations cancel, and the result is a coordinate sweep: one random matching switch in each coordinate direction. Write $\mu_t$ for the law on $S_n$ of $t$ physical shuffles (Lean: law d t, the fraction of coin sequences producing a given permutation).

For a partition $\lambda\vdash n$ let $V_\lambda$ be the Specht module (the irreducible representation of $S_n$ indexed by $\lambda$), of dimension $D_\lambda$, and let $Q_n(\lambda)=\sum_g \mu_d(g)\,\lambda(g)$ be the average of the sweep in $V_\lambda$. For an operator $Y$, $|Y|=(Y^*Y)^{1/2}$ and traces are unnormalized. The regular trace of the $P$-th power is

$$\operatorname{Tr}_{\rm reg}|Q_n|^P=\sum_{\lambda\vdash n}D_\lambda\operatorname{Tr}_{V_\lambda}|Q_n(\lambda)|^P ,$$

in which the trivial representation contributes exactly $1$. Total variation is $\|\mu-\nu\|_{\rm TV}=\tfrac12\sum_g|\mu(g)-\nu(g)|$.

Formalization targets

Goal: regular-trace smoothing (Theorem 1.1)

There is an absolute real $P\ge2$ such that for every $d\ge1$ (so $n=2^d\ge2$)

$$\operatorname{Tr}_{\rm reg}|Q_n|^P\le 1+n^{-10},$$

and for every integer $v$ with $2v\ge P$ and every initial deck $\sigma$,

$$\tfrac12\sum_{g\in S_n}\Bigl|\mu_{vd}(g\sigma^{-1})-\tfrac1{n!}\Bigr|\le\tfrac12\,n^{-5}.$$

The constant $P$ is not specified; only its existence and uniformity in $d$ are asserted. The goal is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. Since one sweep is $d$ physical shuffles, the second clause shows that $O(d)=O(\log n)$ Thorp shuffles bring the full permutation within $\tfrac12 n^{-5}$ of uniform from every starting deck. A counting argument on coin strings (Proposition 5.1 of the source) shows that at least $2d-O(1)$ physical shuffles are needed, so this order is optimal, improving the $O(d^3)$ bound of Morris 2013. The regular-trace bound is stronger than an operator-norm bound for each irreducible: it controls all singular values with their multiplicities, which is what yields polynomially small total-variation distance.

Formalizing it. The statement is fully finite and explicit: an existential over one real constant followed by inequalities for each $d$. A formal proof would certify an optimal-order mixing bound for a widely studied shuffle. Specht modules, Schatten-type traces via continuous functional calculus, and the shuffle law are all defined in the mission's definition file and can be reused for related shuffling problems.

Difficulty

Single-card and few-card statistics mix after one sweep, but the full permutation involves all $\sim n\log n$ bits of information, and the coin choices of a sweep interact across coordinates. The natural route—bounding the operator norm of $Q_n(\lambda)$ separately in each irreducible representation—does not suffice, because the regular trace weights each representation by its dimension $D_\lambda$, and the number of partitions grows like $e^{c\sqrt n}$. A uniform power must work simultaneously for representations of tiny dimension (very long first row), intermediate dimension, and dimension close to $\sqrt{n!}$, and splitting the coordinates into row and column groups produces two symmetry decompositions that do not commute.

Formalization scope

• Positions are Fin d → Bool; permutations are Equiv.Perm (Card d); partitions of $2^d$ are Young diagrams of cardinality $2^d$ (Shapes (2^d)).
• The Specht module is built concretely as the span of the orbit of the standard polytabloid in the space of functions on tabloids, transported to a Euclidean (Hilbert) space; cards are relabelled to cells by a fixed bijection. Q d μ is the average over all coin sequences of length $d$ of the representation of run d d.
• absoluteTrace A P is the real part of the trace of CFC.rpow (CFC.sqrt (A⋆A)) P, i.e. $\operatorname{Tr}|A|^P$; regularTrace multiplies by finrank.
• sweepDistance d v σ is total variation of the law of $v\cdot d$ physical shuffles, right-translated by $\sigma$, from the uniform weight $1/(2^d)!$. The integer $v$ is converted with Int.toNat; since $P\ge2$ and $2v\ge P$, $v\ge1$ and no truncation occurs.
• The support lower bound (Proposition 5.1) is not part of the goal.
• Infrastructure needed: Specht-module dimensions and branching, Schatten-norm inequalities (Hölder, Araki–Lieb–Thirring), Schur–Weyl duality, and the partial-deck density bound from the companion preprint on routing densities. Contributions formalizing any of these pieces are welcome.

Selected references

• E. O. Thorp, Nonrandom shuffling with applications to the game of Faro, J. Amer. Statist. Assoc. 68 (1973), 842–847. https://doi.org/10.1080/01621459.1973.10481434
• B. Morris, The mixing time of the Thorp shuffle, SIAM J. Comput. 38 (2008), 484–504. https://doi.org/10.1137/050636231
• R. Montenegro and P. Tetali, Mathematical aspects of mixing times in Markov chains, Found. Trends Theor. Comput. Sci. 1 (2006), 237–354. https://doi.org/10.1561/0400000003
• B. Morris, Improved mixing time bounds for the Thorp shuffle and L-reversal chain, Ann. Probab. 37 (2009), 453–477. https://doi.org/10.1214/08-AOP409
• B. Morris, Improved mixing time bounds for the Thorp shuffle, Combin. Probab. Comput. 22 (2013), 118–132. https://doi.org/10.1017/S0963548312000478
• H. Araki, On an inequality of Lieb and Thirring, Lett. Math. Phys. 19 (1990), 167–170. https://doi.org/10.1007/BF01045887
• A. Berele and A. Regev, Hook Young diagrams with applications to combinatorics and to representations of Lie superalgebras, Adv. Math. 64 (1987), 118–175. https://doi.org/10.1016/0001-8708(87)90007-7
• B. E. Sagan, The Symmetric Group, 2nd ed., GTM 203, Springer, 2001. https://doi.org/10.1007/978-1-4757-6804-6
• OpenAI, Random-subspace tests and trace smoothing for coordinate sweeps, OpenAI Math Release preprint, September 26, 2026 (source of the goal; Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Random-subspace-tests-and-trace-smoothing-for-coordinate-sweeps-September-26-2026/paper.pdf

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

A random configuration on the vertices of a graph is a factor of IID if it can be produced by a measurable rule from independent uniform labels at the vertices, where the rule commutes with the graph's automorphisms. On trees this notion connects ergodic theory (which invariant processes are "Bernoulli-like"), local algorithms on sparse random graphs (factors of IID are limits of what local algorithms can produce), and statistical mechanics. The free Ising state on the $d$-regular tree is the basic test case. It is easy to sample from a chosen root by broadcasting spins outward, but a factor rule may not use a root. Lyons asked for which inverse temperatures it is a factor of IID (Lyons 2017), and Nam, Sly and Zhang conjectured the answer $\tanh\beta\le(d-1)^{-1/2}$ after proving it for large $d$ below a non-explicit constant (Nam–Sly–Zhang 2022).

This mission asks for a formal proof of the exact threshold, including equality, as stated in an OpenAI preprint dated September 26, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

• 1995–1996 — Bleher, Ruiz and Zagrebnov (J. Stat. Phys. 1995) and Ioffe (Lett. Math. Phys. 1996): the free state on the regular tree is extremal exactly when $(d-1)\tanh^2\beta\le1$.
• 2000 — Evans, Kenyon, Peres and Schulman relate broadcasting on trees to the Ising model (Ann. Appl. Probab. 2000).
• 2010 — Pemantle and Peres give a capacity criterion that also covers critical cases (Ann. Probab. 2010).
• 2015 — Backhausz, Szegedy and Virág's correlation bound for factors of IID (Random Struct. Alg. 2015), which rules out the free state beyond the threshold.
• 2017 — Lyons surveys factors of IID on trees, records Sly's obstruction above the reconstruction threshold, and the finite-cluster construction in the uniqueness range $\tanh\beta\le 1/(d-1)$ (CPC 2017).
• 2022 — Nam, Sly and Zhang construct the free state as a factor for $d\ge d_0$ and $\tanh\beta\le c/\sqrt{d-1}$, via posterior-drift stochastic differential equations, and conjecture the sharp threshold (CMP 2022).

Setting

Let $T_d$ be the infinite $d$-regular tree with vertex set $V$; concretely, $V$ is the set of finite words over $\{1,\dots,d\}$ with no two equal consecutive letters, and $w$ is adjacent to $wc$. Put $\theta=\tanh\beta$ for $\beta\ge0$. The free zero-field Ising law $\mu_{d,\beta}$ on $\{-1,+1\}^V$ is determined by its marginals on finite connected subtrees $D$:

$$\mu_{d,\beta}(\sigma|_D=\eta)=\frac12\prod_{\{u,v\}\in E(D)}\frac{1+\theta\,\eta_u\eta_v}{2}.$$

Equivalently, a fair spin at one vertex is broadcast along edges, each child agreeing with its parent with probability $(1+\theta)/2$. A spin law is a factor of IID if it is the law of $\Phi(U)$ for i.i.d. uniform labels $U=(U_v)_{v\in V}$ and a measurable $\Phi:[0,1]^V\to\{-1,1\}^V$ such that, for each fixed automorphism $g$, $\Phi(gU)=g\Phi(U)$ almost surely, where $(gx)_v=x_{g^{-1}v}$.

Formalization targets

Goal: Theorem 1.1 (p. 1)

For every integer $d\ge3$ and every $\beta\ge0$,

$$\mu_{d,\beta}\ \text{is a factor of IID}\iff \tanh\beta\le\frac1{\sqrt{d-1}}.$$

Significance

The result itself. It answers the ferromagnetic case of Lyons's question and proves the Nam–Sly–Zhang conjecture for every $d\ge3$. The threshold coincides with the reconstruction (extremality) threshold of the free state, and the result holds at equality, where non-reconstruction alone gives no factor rule (a weak limit of factors need not be a factor). The preprint also shows that, in this range, the factor can be chosen to commute with every automorphism on every input (Lemma 8.5, p. 46). The converse direction ($\tanh\beta>(d-1)^{-1/2}$ excludes a factor) is known from Sly's obstruction via the Backhausz–Szegedy–Virág bound and is reproved on p. 2.

Formalizing it. The preprint's construction uses Brownian observation processes, stochastic localization, innovation equations of nonlinear filtering, and conditional-copy coupling arguments. Mathlib has Brownian motion only in early form and no stochastic calculus for infinitely many coupled SDEs; a formal proof would build reusable stochastic-analysis infrastructure. The converse needs the BSV correlation bound for factors of IID. No machine-checked factor-of-IID result for a non-trivial Gibbs measure is known.

Difficulty

Rooted sampling is easy; the obstacle is to remove the root while keeping the output a measurable function of the labels. Finite-cluster constructions only work in the uniqueness range $\theta\le1/(d-1)$. The Nam–Sly–Zhang approach observes $X_v(t)=t\sigma_v+B_v(t)$ and expresses the posterior through innovations $W_v$, which are independent Brownian motions; but being Brownian does not make $X$ a function of $W$, and that is the central step (pp. 2–3). At criticality $\theta=(d-1)^{-1/2}$ the field-response sums in the innovation equation are only borderline integrable near time zero, so infinite sums must be justified with an exact covariance-energy identity rather than with a contraction estimate (Section 1.2, p. 3).

Formalization scope

• TreeVertex d is the set of words in Fin d with distinct consecutive letters, treeAdj appends or removes one letter, and TreeAut d is the group of adjacency-preserving bijections.
• Labels have law Measure.infinitePi of Lebesgue measure on $[0,1]$; spins take values in a two-element type with the discrete σ-algebra, and configurations carry the product σ-algebra.
• HasFreeIsingLaw θ μ prescribes $\mu$ on every cylinder over a finite connected Finset by the product formula above; these cylinders determine the law.
• IsFactorOfIID d θ asks for a measurable Phi with pushforward law HasFreeIsingLaw θ and, for each automorphism g, Phi (relabel g U) = relabel g (Phi U) for almost every U (null set may depend on g), matching (1.1).
• The goal uses θ = Real.tanh β with $\beta\ge0$ and $d\ge3$; at $\beta=0$ both sides hold trivially (i.i.d. spins), which is consistent with the source. The stronger everywhere-equivariant version is not part of the goal.

Selected references

• OpenAI, The sharp factor-of-IID threshold for the free Ising model on regular trees, OpenAI Math Release preprint, September 26, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-sharp-factor-of-IID-threshold-for-the-free-Ising-model-on-regular-trees-September-26-2026/article.pdf
• D. Nam, A. Sly, L. Zhang, Ising model on trees and factors of IID, Comm. Math. Phys. 389 (2022), 1009–1046. https://doi.org/10.1007/s00220-021-04260-2
• R. Lyons, Factors of IID on trees, Combin. Probab. Comput. 26 (2017), 285–300. https://doi.org/10.1017/S096354831600033X
• Á. Backhausz, B. Szegedy, B. Virág, Ramanujan graphings and correlation decay in local algorithms, Random Structures Algorithms 47 (2015). https://doi.org/10.1002/rsa.20562
• P. M. Bleher, J. Ruiz, V. A. Zagrebnov, On the purity of the limiting Gibbs state for the Ising model on the Bethe lattice, J. Stat. Phys. 79 (1995). https://doi.org/10.1007/BF02179399
• D. Ioffe, On the extremality of the disordered state for the Ising model on the Bethe lattice, Lett. Math. Phys. 37 (1996), 137–143. https://doi.org/10.1007/BF00416016
• W. Evans, C. Kenyon, Y. Peres, L. J. Schulman, Broadcasting on trees and the Ising model, Ann. Appl. Probab. 10 (2000). https://doi.org/10.1214/aoap/1019487349
• R. Pemantle, Y. Peres, The critical Ising model on trees, concave recursions and nonlinear capacity, Ann. Probab. 38 (2010). https://doi.org/10.1214/09-AOP482
• R. Eldan, Thin shell implies spectral gap up to polylog via a stochastic localization scheme, GAFA 23 (2013), 532–569. https://doi.org/10.1007/s00039-013-0214-y
• A. El Alaoui, A. Montanari, An information-theoretic view of stochastic localization, IEEE Trans. Inform. Theory 68 (2022). https://doi.org/10.1109/TIT.2022.3180298

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.