All missions

Motivation

Standard generator subsets define natural subgroups in an Artin group. The source asks whether arbitrary conjugates of these subgroups remain in the same class after intersection. The source is OpenAI's September 2026 manuscript.

Setting

A standard parabolic subgroup is generated by a subset of the standard generators. A parabolic subgroup is any conjugate of one. There is no requirement that its Coxeter subgroup be finite.

Formalization targets

$$gA_Xg^{-1}\cap hA_Yh^{-1}=kA_Zk^{-1}\quad\text{for some }Z\subseteq S,\ k\in A_M.$$

The theorem, which is admitted in the source with a placeholder proof, states the following for a Coxeter matrix M on a finite, linearly ordered index set S, with Artin(M) the Artin group presented on generators S by the braid relations: the word of alternating generators s,t,s,... of length M(s,t) equals the alternating word beginning with t, for each pair s,t. For any two subsets X and Y of S and any two elements g and h of Artin(M), there exist a subset Z of S and an element k of Artin(M) such that the intersection of the two conjugate subgroups g P_X g⁻¹ and h P_Y h⁻¹ equals k P_Z k⁻¹. Here P_T is the standard parabolic subgroup generated by the images of the generators in T, and conjugation by g is the subgroup whose members x satisfy g⁻¹xg in P. There is no spherical-type or other restriction on M, so the intersection of two conjugates of standard parabolic subgroups is itself a conjugate of a standard parabolic subgroup.

The goal is OAI.HarmonicArtin.ParabolicIntersections.unconditional_parabolic_intersections. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.

• unconditional arbitrary intersections.
• unconditional nonclique dynamics.
• unconditional parabolic closure.

Significance

The selected goal is closure under binary intersection. Attached results also give arbitrary intersections controlled by at most the rank many members, unique parabolic closure, and dynamics for irreducible non-clique groups. 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

Conjugation obscures the standard generating subsets, so intersecting $X$ and $Y$ alone does not describe the subgroup intersection. The target must produce both a new subset and a new conjugating element.

Formalization scope

The generating type is finite and linearly ordered. The Coxeter-matrix convention encodes an infinite label by zero. The dynamics milestone has additional irreducibility and non-clique assumptions; those are not imposed on the intersection theorem.

The shared definitions are supplied by ArtinParabolicIntersections. 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, Parabolic intersections in Artin groups, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

A classifying-space problem asks whether a natural complex captures a group without additional higher homotopy. The source addresses the finite-rank Artin problem through the lifted spherical-cell complex. The source is OpenAI's September 2026 manuscript.

Setting

An Artin group is presented by alternating braid relations from a Coxeter matrix. A subset of generators is spherical when its associated Coxeter parabolic subgroup is finite. Lifted cells pair a group element with such a subset, with incidence determined by reduced coset words.

Formalization targets

$$\operatorname{ContractibleSpace}(\operatorname{SalvettiCover}(M))\qquad\text{for every Coxeter matrix }M\text{ on finite }S.$$

For every Coxeter matrix M indexed by a finite type S of standard generators, the topological space SalvettiCover(M) is contractible. The Artin group Artin(M) is the free group on S modulo the braid relators, one for each ordered pair (s,t): the alternating word s t s t ... of length M(s,t) times the inverse of the alternating word t s t s ... of the same length. A subset T of S is spherical when the standard parabolic subgroup of the Coxeter group generated by the simple reflections in T is finite. A lifted cell is a pair (a,T) of an Artin group element and a spherical subset. One lifted cell (a,T) is a face of (b,U) when T is contained in U and there is a word w in letters of U that is reduced in the Coxeter group (its Coxeter length equals the word length), is of minimal length in its coset with respect to the parabolic subgroup generated by T, and satisfies a = b times the image of w in the Artin group. The preorder on lifted cells is the reflexive transitive closure of this face relation, and SalvettiCover(M) is the geometric realization, as a topological space, of the nerve of that preorder viewed as a category.

The goal is OAI.HarmonicArtin.salvetti_cover_contractible.

Significance

The goal makes the full topological realization contractible, rather than only asserting vanishing of a selected homotopy group. It supplies a precise target for the covering-space component of the source. 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

Local spherical pieces need not automatically fit into a globally contractible realization. The face relation and its transitive closure must retain the interaction between Artin words and Coxeter length.

Formalization scope

SalvettiCover is the geometric realization of the nerve of the lifted-cell preorder. The generator type is finite but need not be equipped with a chosen enumeration. The mission preserves this published model instead of substituting a different complex.

The shared definitions are supplied by HarmonicArtin. 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, Harmonic heights and the Artin K(pi,1) conjecture, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

An Ising spin system probes a quadratic form only on cube vertices. The source asks whether random orthogonal eigenvectors allow its pressure to be determined by the limiting eigenvalue distribution at every positive temperature. The source is OpenAI's September 2026 manuscript.

Setting

The pressure is the normalized logarithm of the average Boltzmann weight under the uniform spin prior. Eigenvectors are Haar orthogonal, and the deterministic empirical eigenvalue laws converge weakly to a compactly supported probability law. The variational formula uses an edge-extended spectral transform.

Formalization targets

$$\mathbb E P_N(\beta)\to\mathcal V_\beta,\qquad P_N(\beta)\to\mathcal V_\beta\ \text{almost surely}\qquad(\beta>0).$$

For a spin system on N Ising spins σ ∈ {−1,1}^N, the rotated pressure for eigenvalues λ₁,…,λ_N, an orthogonal rotation U and a field c is (1/N) times the log of the average over all 2^N spin configurations of exp(H(σ)), where H(σ) = (1/2)∑ᵢ λᵢ (Uσ)ᵢ² + ∑ᵢ cᵢσᵢ. The theorem states that, for any probability space (Ω,P), random N×N orthogonal matrices U_N that are measurable and whose laws are right-invariant under multiplication (Haar-type), and any deterministic eigenvalue arrays (eig_N,i), the following holds under these assumptions: ν is a probability measure on ℝ whose support lies in [a,b] and contains both a and b; for every ε>0, eventually in N all eigenvalues lie in [a−ε,b+ε]; the empirical spectral laws (1/N)∑ᵢ δ_{eig_N,i} converge weakly to ν; and the inverse temperature β is strictly positive. Then, with eigenvalues β·eig_N,i, rotation U_N(ω)⁻¹ and zero external field, the expected rotated pressure ∫ pressure dP converges as N → ∞, and the pressure itself converges for P-almost every ω, in both cases to the real part of the variational functional of the measureR transform of the β-rescaled law of ν, evaluated at the edge β·b.

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

• gaussianPattern ground limit unconditional.
• gaussianPattern norm limits unconditional.
• gaussianPattern pressure limit unconditional.
• ground state limit unconditional.
• limiting pressure of extreme limits unconditional.
• limiting wasserstein field pressure of extreme limits unconditional.
• random field pressure tendsto ae unconditional.
• random pressure limit unconditional.
• random pressure tendsto ae unconditional.
• random pressure tendsto in measure unconditional.

Significance

The selected goal is the all-positive-temperature zero-field pressure theorem. The attached results also cover field laws, random spectra, Gaussian-pattern pressure and ground energy, and related norm limits under their stated assumptions. 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

Weak spectral convergence does not control rare extreme eigenvalues. The explicit no-outlier condition is essential to the selected statement’s comparison with the limiting spectral functional.

Formalization scope

The spin prior is uniform probability, and temperature is implemented by multiplying eigenvalues by $\beta$. The no-outlier condition holds eventually within every enlargement of the limiting support interval. Almost-sure convergence and expectation convergence are both conclusions; other attached variants keep their own uniform-integrability and field hypotheses.

The shared definitions are supplied by InvariantIsing. 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, All-temperature pressure for orthogonally invariant Ising spin glasses, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

Rectangular matrix products arise when the two outer dimensions are much larger than the inner dimension. The dual exponent records the largest inner growth rate compatible with arithmetic exponent two. The source manuscript presents the surrounding research claim.

Setting

For k∈[0,1], ω_ℂ(1,k,1) is the infimum of exponents for multiplying an n×⌈nᵏ⌉ matrix by a ⌈nᵏ⌉×n matrix over ℂ. The dual exponent α is the supremum of k for which this infimum equals two.

Formalization target

Prove the strict bound

$$\alpha_{\mathbb C}>\frac{93}{200}=0.465.$$

The additional published rectangular endpoint asserts ω_ℂ(1,709/1000,1)<523/250=2.092.

The selected formal target is OAI.MatrixMultiplication.complex_alpha_gt_93_div_200.

Significance and status

Strictness is part of both statements. The supplied goal concerns the complex dual exponent; the manuscript title’s square bound and broader field claims are not attached formal targets. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

An algorithm for one size does not establish an asymptotic exponent. The definition quantifies over every positive slack and all positive sizes with one bound constant for each slack.

Formalization scope

Algorithms are division-free arithmetic programs with constants and input gates of cost zero and addition, subtraction and multiplication of cost one. Correctness is quantified over all input matrices. The dual exponent is a real supremum of exact exponent-two shapes, using the prescribed inner-dimension ceiling.

Selected references

• OpenAI, Complex Matrix Multiplication Below 2.258 and Rectangular Bounds, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

Singular integral estimates can detect geometric regularity in a measure whose support has no given parametrization. The mission turns a uniform Riesz-transform bound into uniform pieces of Lipschitz images. The source manuscript presents the surrounding research claim.

Setting

Let μ be a regular measure in ℝᵈ, with d≥4 and 2≤n≤d−2. Ahlfors–David regularity means that μ(B(x,r)) is comparable to rⁿ on its support at admissible radii. Hard-truncated Riesz transforms use the kernel (x−y)/|x−y|^(n+1), excluding distances at most ε.

Formalization target

With fixed dimension and bounds C_AD,C_R, prove that there exist θ>0 and M≥0 such that every eligible μ satisfies

$$\mu(B(x,r)\cap\operatorname{range}g)\ge\theta r^n$$

for some M-Lipschitz map g from the open n-dimensional radius-r ball, at every support point and admissible radius.

The selected formal target is OAI.RieszRectifiability.quantitative_higher_codimension_riesz_rectifiability.

Significance and status

The constants θ and M are uniform across the entire class of measures with the prescribed analytic bounds. This is the exact quantitative ball-image conclusion. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

Individual rectifiable pieces with constants depending on μ do not yield this quantifier order. The Riesz bound ranges over every positive hard truncation and every scalar L² input.

Formalization scope

Ambient space is EuclideanSpace ℝ (Fin d). Radii are positive and bounded by the extended support diameter. The hypothesis uses μ.Regular, nonnegative Riesz constants, MemLp and eLpNorm; the conclusion uses the actual measure of the intersection with a Lipschitz image. No endpoint codimensions are included.

Selected references

• OpenAI, Riesz transforms and uniform rectifiability in higher codimension, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

Closed diagonal orbits encode lattices in totally real number fields. Their distribution tests whether arithmetic families fill the space of unimodular lattices as their discriminants grow. The source manuscript presents the surrounding research claim.

Setting

For a fixed prime n=d+1 ≥ 5, Xₙ is the quotient of SLₙ(ℝ) by its integral lattice subgroup. A packet consists of normalized full lattices of one local homothety type, including the specified sign translates. Its measure averages orbital probabilities with orbit-volume weights.

Formalization target

For any sequence of totally real degree-n fields and full lattices whose multiplier discriminants tend to infinity, prove

$$\exists\nu,\quad\nu\text{ is Haar probability},\qquad\mu_i\Rightarrow\nu,$$

and tightness of the entire family {μᵢ}. Weak convergence uses every bounded continuous real test function and includes the probability normalization of every μᵢ.

The selected formal target is OAI.DukePrimeDegree.prime_degree_packet_measure_equidistribution_unconditional.

Significance and status

The conclusion addresses arbitrary local types and includes absence of escape of mass. The fixed-Haar formulation is also available as a supporting target. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

Convergence on compactly supported tests alone would not establish the requested probability convergence on a noncompact quotient. The packet normalization and tightness must be justified uniformly through the discriminant limit.

Formalization scope

The source definitions use completed lattices over ℤₚ, diagonal-flow period covolumes and volume-weighted sums over distinct orbits. The theorem fixes prime degree at least five and allows both fields and local types to vary. Both published formulations and their shared definitions are referenced.

Selected references

• OpenAI, Equidistribution of Prime-Degree Torus Packets with Arbitrary Local Type, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

Real zeros of Dirichlet L-functions close to one obstruct uniform estimates for primes in arithmetic progressions. A conductor-independent logarithmic gap is the precise quantitative issue addressed here. The source manuscript presents the surrounding research claim.

Setting

A Dirichlet character χ modulo an integer q is primitive, nonprincipal, and real-valued when its complex values have zero imaginary part. Its analytically continued L-function is denoted L(s,χ). The zero β is real and lies strictly between zero and one; log is the natural logarithm.

Formalization target

Prove that one positive real constant works for every allowed modulus, character and zero:

$$\exists c>0\;\forall q\ge3,\quad L(\beta,\chi)=0,\ 0<\beta<1\Longrightarrow c\le(1-\beta)\log q.$$

The constant must be independent of q and χ.

The selected formal target is OAI.SiegelZeros.WeightedTorusJets.exists_absolute_real_zero_gap.

Significance and status

This is the uniform zero-gap conclusion itself, not a statement for a bounded family of conductors. The source dated October 1, 2026 states this as its principal result. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

A bound whose constant varies with the character cannot establish this quantifier order. The arithmetic and analytic estimates must retain one positive constant across every conductor and every real primitive character.

Formalization scope

The goal uses Mathlib’s actual Dirichlet characters and L-functions over ℂ, with q : ℕ, a nonzero instance and q ≥ 3. Both available published formulations are referenced. The second formulation merely groups the zero hypotheses differently and is not presented as an independent milestone. The manuscript’s interpolation and determinant lemmas have no supplied published theorem IDs and are not attached as milestones.

Selected references

• OpenAI, Uniform exclusion of Landau–Siegel zeros, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation: when are optimal transport maps continuous?

Given two probability densities $\rho_0,\rho_1$ on a compact Riemannian manifold, optimal transport with the quadratic cost $c(x,y)=d(x,y)^2/2$ seeks the map $T$ pushing $\rho_0\,\mathrm{vol}$ to $\rho_1\,\mathrm{vol}$ at least total cost. McCann proved that such a map exists and is unique almost everywhere (McCann 2001). Whether it is continuous when the densities are merely bounded above and below depends on the geometry of the cost: the Ma–Trudinger–Wang (MTW) condition, a sign condition on a fourth derivative of $c$, is the decisive curvature hypothesis, and its weak form is known to be necessary. The question is whether weak MTW is also sufficient on every compact manifold, with estimates that do not degenerate as transport graphs approach conjugate points.

Background

• 1992 — Caffarelli's regularity theory for maps with convex potentials, based on sections and contact-volume comparison (Caffarelli 1992).
• 2001 — McCann's polar factorization on Riemannian manifolds (McCann 2001).
• 2005 — Ma, Trudinger and Wang introduce the curvature condition (MTW 2005).
• 2009 — Loeper links MTW to supporting cost functions and shows its necessity for continuity (Loeper 2009).
• 2010 — Loeper and Villani: uniform estimates under strict MTW and nonfocality (Loeper–Villani 2010).
• 2011 — Figalli, Rifford and Villani: transport continuity implies convex injectivity domains and weak MTW; on surfaces continuity is equivalent to their conjunction, and the equivalence with weak MTW alone is posed (FRV 2011).
• 2013 — Figalli, Kim and McCann: Hölder continuity and injectivity of optimal maps under weak MTW with cost-convexity hypotheses (FKM 2013), and products of round spheres (FKM 2013).
• 2015 — Figalli, Gallouët and Rifford: weak MTW implies convex injectivity domains on nonfocal manifolds (FGR 2015).
• 2019 — Lebedeva, Petrunin and Zolotov list the convexity and continuity questions (LPZ 2019, Questions 8.6–8.7).
• 2026 — Two OpenAI preprints (OpenAI Math Release, September 25, 2026): a companion proving that weak MTW forces convex injectivity domains and global support, and Uniform Bi-Hölder Transport from Weak MTW (this mission), claiming uniform bi-Hölder optimal maps for every density-bounded class. Neither is peer reviewed, and the theorem is not formally verified.

Setting

Let $(M,g)$ be a smooth, connected, compact Riemannian manifold without boundary, of dimension $n\ge2$, with distance $d$ and volume $\mathrm{vol}$. Put $c(x,y)=\tfrac12 d(x,y)^2$ and let

$$I(x)=\{p\in T_xM:\ d(x,\exp_x(ap))=a|p| \text{ for some } a>1\}$$

be the open injectivity domain. Weak MTW: for every $p\in I(x)$ and $\xi\perp\eta$ in $T_xM$,

$$-\frac32\,\frac{\partial^4}{\partial s^2\partial t^2}\,c\big(\exp_x(t\xi),\exp_x(p+s\eta)\big)\Big|_{s=t=0}\ \ge 0 .$$

For $0<\lambda\le\Lambda$, the density class consists of measurable $\rho$ with $\int\rho\,d\mathrm{vol}=1$ and $\lambda\le\rho\le\Lambda$ almost everywhere. An optimal map from $\rho_0$ to $\rho_1$ is a measurable $T$ with $T_\#(\rho_0\mathrm{vol})=\rho_1\mathrm{vol}$ minimizing $\int c(x,T(x))\rho_0(x)\,d\mathrm{vol}$ among such maps.

In Lean, metricVolume n is the $n$-dimensional Hausdorff measure normalized to agree with Lebesgue measure on $\mathbb R^n$ (which equals Riemannian volume), riemannianExp is defined from complete geodesics, and WeakMTW uses iteratedDeriv 2 twice.

Formalization targets

Goal: uniform bi-Hölder optimal maps

Fix $(M,g)$ satisfying weak MTW and $0<\lambda\le\Lambda$ with a nonempty density class. There are $\alpha\in(0,1]$ and $C<\infty$, depending only on $(M,g),\lambda,\Lambda$, such that for all densities $\rho_0,\rho_1$ in the class, the almost-everywhere unique optimal map has a homeomorphic representative $\widetilde T$ with

$$d(\widetilde T x,\widetilde T x')\le C\,d(x,x')^\alpha,\qquad d(\widetilde T^{-1}y,\widetilde T^{-1}y')\le C\,d(y,y')^\alpha .$$

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

Significance

The result itself. The constants are common to the whole density class; they do not depend on the densities or their derivatives, and the theorem allows conjugate cut points without nonfocality, strict MTW, or cut avoidance. Combined with the necessity result of Figalli–Rifford–Villani it gives the equivalence of weak MTW with transport continuity for bounded densities on compact manifolds, with uniform estimates in the forward direction. No explicit exponent is obtained (the positive exponent comes from a contradiction argument).

Formalizing it. The Lean statement packages existence, almost-everywhere uniqueness, homeomorphic regularity and uniform bi-Hölder bounds in one assertion over all density pairs, making precise what "class-uniform" means. A proof requires the companion geometric results (convex injectivity domains, global support), McCann's theorem, and Caffarelli-type section estimates on manifolds — none currently in Mathlib.

Difficulty

Hölder estimates obtained after localizing near a smooth part of the cost give a density-dependent exponent and localization scale; they do not give a common scale or constant for a family whose transport graphs approach conjugate pairs, where the cost stops being smooth. Weak MTW constrains the cost only where it is smooth and only for orthogonal directions. Earlier uniform results needed strict MTW and nonfocality, or special geometry (products of spheres).

Formalization scope

• Volume is the normalized Hausdorff measure euclideanVolumeFactor n • μH[n]; densities are AEMeasurable, integrable, of mass one, and between lam and cap almost everywhere; nonemptiness of the class is a hypothesis, as in the source.
• IsOptimalMap requires measurability, the pushforward identity for withDensity measures, and minimality among all measurable maps with that pushforward; uniqueness is almost everywhere for $\rho_0\,\mathrm{vol}$.
• The conclusion requires one $\alpha\in(0,1]$ and one $C\ge0$ before quantifying over densities, and a homeomorphism M ≃ₜ M with the same exponent and constant for $T$ and $T^{-1}$; a trivializing choice is excluded because $T$ must itself be optimal.
• Weak MTW is a hypothesis only at $p\in I(x)$ and orthogonal $\xi,\eta$.
• Needed infrastructure: Riemannian geodesics and cut locus, semiconvex potentials, Kantorovich duality and McCann's theorem, Hausdorff measure versus Riemannian volume, Caffarelli-type sections.

Selected references

• L. A. Caffarelli, The regularity of mappings with a convex potential, J. Amer. Math. Soc. 5 (1992), 99–104. https://doi.org/10.1090/S0894-0347-1992-1124980-8
• R. J. McCann, Polar factorization of maps on Riemannian manifolds, Geom. Funct. Anal. 11 (2001), 589–608. https://doi.org/10.1007/PL00001679
• X.-N. Ma, N. S. Trudinger and X.-J. Wang, Regularity of potential functions of the optimal transportation problem, Arch. Ration. Mech. Anal. 177 (2005), 151–183. https://doi.org/10.1007/s00205-005-0362-9
• G. Loeper, On the regularity of solutions of optimal transportation problems, Acta Math. 202 (2009), 241–283. https://doi.org/10.1007/s11511-009-0037-8
• G. Loeper and C. Villani, Regularity of optimal transport in curved geometry: the nonfocal case, Duke Math. J. 151 (2010), 431–485. https://doi.org/10.1215/00127094-2010-003
• A. Figalli, L. Rifford and C. Villani, Necessary and sufficient conditions for continuity of optimal transport maps on Riemannian manifolds, Tohoku Math. J. 63 (2011), 855–876. https://doi.org/10.2748/tmj/1325886291
• A. Figalli, Y.-H. Kim and R. J. McCann, Hölder continuity and injectivity of optimal maps, Arch. Ration. Mech. Anal. 209 (2013), 747–795. https://doi.org/10.1007/s00205-013-0629-5
• A. Figalli, Y.-H. Kim and R. J. McCann, Regularity of optimal transport maps on multiple products of spheres, J. Eur. Math. Soc. 15 (2013), 1131–1166. https://doi.org/10.4171/JEMS/388
• A. Figalli, T. O. Gallouët and L. Rifford, On the convexity of injectivity domains on nonfocal manifolds, SIAM J. Math. Anal. 47 (2015), 969–1000. https://doi.org/10.1137/140961821
• N. Lebedeva, A. Petrunin and V. Zolotov, Bipolar comparison, Geom. Funct. Anal. 29 (2019), 258–282. https://doi.org/10.1007/s00039-019-00481-9
• OpenAI, Global Support and Convex Injectivity Domains under Weak MTW, OpenAI Math Release preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Global-Support-and-Convex-Injectivity-Domains-under-Weak-MTW-September-25-2026/paper.pdf
• OpenAI, Uniform Bi-Hölder Transport from Weak MTW, OpenAI Math Release preprint, September 25, 2026 (Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Uniform-Bi-Holder-Transport-from-Weak-MTW-September-25-2026/paper.pdf

Motivation

A symplectic embedding preserves the standard symplectic form $\omega_0=\sum_j dx_j\wedge dy_j$ on $\mathbb C^n$, and in particular preserves volume. Gromov's nonsqueezing and two-ball theorems showed that symplectic embeddings obey constraints invisible to volume (Gromov 1985). The ball-packing problem asks exactly when finitely many balls can be embedded disjointly and symplectically into a given ball, and so measures how far symplectic rigidity goes beyond volume.

In real dimension four the answer involves infinitely many obstructions coming from pseudoholomorphic curves and algebraic geometry (McDuff–Polterovich 1994; Biran 1997). In higher dimensions Siegel and Yao conjectured that only two obstructions survive: volume and Gromov's two-ball obstruction (Conjecture A of Siegel–Yao 2025).

This mission asks for a machine-checked proof of Theorem 1.1 of an OpenAI preprint dated September 23, 2026 (source), which claims Conjecture A in every real dimension $2n\ge6$. The preprint has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal is open.

Background

• 1985 — Gromov introduces pseudoholomorphic curves and proves the two-ball obstruction $R_1+R_2\le R$ (Invent. Math. 1985).
• 1994 — McDuff and Polterovich connect packing to blowups and algebraic geometry (Invent. Math. 1994).
• 1995 — Traynor gives explicit packing constructions (J. Differential Geom. 1995).
• 1997–2001 — Biran proves packing stability in dimension four (GAFA 1997; GAFA 2001).
• 2005 — Schlenk's monograph develops folding and planar constructions (de Gruyter 2005).
• 2011–2016 — Buse and Hind extend equal-ball stability to higher dimensions (Geom. Topol. 2011; Compos. Math. 2013); Buse, Hind and Opshtein prove unequal-ball stability in dimension four for small capacities (Trans. AMS 2016).
• 2025 — Siegel and Yao formulate Conjecture A for higher-dimensional packings.
• 2026 — The OpenAI preprint claims Conjecture A for all $n\ge3$ (Theorem 1.1, p. 2).

Setting

For $R>0$ write

$$B^{2n}(R)=\Bigl\{z\in\mathbb C^n:\ \pi\sum_{j=1}^n|z_j|^2\le R\Bigr\},$$

so $R$ is the capacity, the Euclidean radius is $\sqrt{R/\pi}$, and $\mathrm{vol}\,B^{2n}(R)=R^n/n!$. An embedding of a closed ball into the open ball $\operatorname{int}B^{2n}(R)$ means a smooth map defined on an open neighbourhood of the closed ball, which is a topological embedding there, pulls $\omega_0$ back to $\omega_0$, and sends the closed ball into the open target. A packing of $B^{2n}(R_1),\dots,B^{2n}(R_k)$ is a family of such embeddings whose images of the closed balls are pairwise disjoint.

Formalization targets

Milestone: necessity in Theorem 1.1 (p. 4)

If $n\ge3$, $k\ge1$, $R,R_i>0$ and a packing exists, then

$$\sum_{i=1}^kR_i^n<R^n\qquad\text{and}\qquad R_i+R_j<R\ \ (i\ne j).$$

The images lie in some $\operatorname{int}B^{2n}(\sigma)$ with $\sigma<R$ by compactness, so the volume bound and Gromov's two-ball obstruction give the strict inequalities.

Goal: Theorem 1.1 (p. 2)

For integers $n\ge3$, $k\ge1$ and positive reals $R,R_1,\dots,R_k$, a symplectic embedding $\bigsqcup_iB^{2n}(R_i)\hookrightarrow\operatorname{int}B^{2n}(R)$ exists if and only if the two inequalities above hold.

Significance

The result itself. In every real dimension at least six, the volume and two-ball obstructions are the only obstructions to packing balls of arbitrary capacities into a ball. This contrasts with dimension four, where infinitely many further obstructions are essential, and it goes beyond packing-stability results, which concern many small balls. The theorem settles Siegel and Yao's Conjecture A.

Formalizing it. The necessity direction needs Gromov's two-ball theorem, which rests on pseudoholomorphic curve theory and has no formalization. The sufficiency direction uses Hamiltonian flows, Moser isotopies, toric domains, Kähler forms on projective degenerations and normal-cone transfer. A formal proof would require substantial new symplectic and algebro-geometric infrastructure, all of it reusable.

Difficulty

Sufficiency is the hard direction. The volume inequality is an integral condition, but a packing needs pointwise room; in the preprint's toric models over a surface with a handle, the unused-area profile $P$ has positive integral but need not be positive at every moment, and a Hamiltonian comparison theorem (Lemma 2.1, p. 5) is needed to rearrange it into disjoint ball layers (Lemma 3.3, p. 12). The models must then be transferred symplectically into the target ball using Kähler degenerations; three geometric cases arise (all capacities below $R/2$, Proposition 5.2, p. 25; one large capacity in dimension $\ge8$, Proposition 5.3, p. 26; one large capacity in dimension six, Proposition 6.7, p. 39). For necessity the obvious volume argument gives only non-strict inequalities; strictness comes from compactness of the images, and the pairwise bound is genuinely symplectic.

Formalization scope

• Phase space is Fin n → ℂ with capacity $\pi\sum_j|z_j|^2$ and $\omega_0(u,v)=\sum_j(\mathrm{Re}\,u_j\,\mathrm{Im}\,v_j-\mathrm{Im}\,u_j\,\mathrm{Re}\,v_j)$.
• SymplecticOn U f: $U$ open, $f$ is $C^\infty$ on $U$, $f|_U$ is a topological embedding, and fderiv preserves $\omega_0$ at every point of $U$.
• HasPacking n k R r: each closed ball $B^{2n}(r_i)$ lies in an open $U_i$ on which $f_i$ is symplectic, $f_i$ maps the closed ball into the open ball of capacity $R$, and images of distinct closed balls are disjoint.
• PackingInequalities uses strict inequalities and quantifies over ordered pairs $i\ne j$; the goal assumes $n\ge3$, $k\ge1$, $R>0$, $r_i>0$, matching the source exactly.
• Neither side is vacuous: for one ball the pairwise condition is empty and the statement reduces to $r_1<R$.

Selected references

• OpenAI, Symplectic Ball Packings in Higher Dimensions, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Symplectic-Ball-Packings-in-Higher-Dimensions-September-23-2026/paper.pdf
• K. Siegel, Y. Yao, On symplectic packing problems in higher dimensions, Math. Ann. 392 (2025), 5361–5392. https://doi.org/10.1007/s00208-025-03221-7
• M. Gromov, Pseudo holomorphic curves in symplectic manifolds, Invent. Math. 82 (1985), 307–347. https://doi.org/10.1007/BF01388806
• D. McDuff, L. Polterovich, Symplectic packings and algebraic geometry, Invent. Math. 115 (1994), 405–429. https://doi.org/10.1007/BF01231766
• P. Biran, Symplectic packing in dimension 4, Geom. Funct. Anal. 7 (1997), 420–437. https://doi.org/10.1007/s000390050014
• O. Buse, R. Hind, Ellipsoid embeddings and symplectic packing stability, Compos. Math. 149 (2013), 889–902. https://doi.org/10.1112/S0010437X12000826
• O. Buse, R. Hind, E. Opshtein, Packing stability for symplectic 4-manifolds, Trans. Amer. Math. Soc. 368 (2016), 8209–8222. https://doi.org/10.1090/tran/6802
• L. Traynor, Symplectic packing constructions, J. Differential Geom. 41 (1995), 735–751. https://doi.org/10.4310/jdg/1214456483
• F. Schlenk, Embedding Problems in Symplectic Geometry, de Gruyter (2005). https://doi.org/10.1515/9783110199697

Motivation: can every surface be realized locally in $\mathbb R^3$?

A Riemannian surface is abstract: it is given by a rule $g$ for measuring lengths and angles in local coordinates, not as a surface sitting in space. The local isometric realization problem asks whether every such surface can, near each point, be realized as an honest smooth surface in Euclidean three-space with the same lengths. The question goes back to the classical theory of surfaces. It is settled for real-analytic metrics and for smooth metrics with nonvanishing curvature, while the unrestricted smooth case is listed as open by Yau (Yau 2000, p. 236) and in Ghomi's problem survey (Ghomi 2019, §1.5, Problem 1.9).

Timeline

• 1926–1927 — Janet and Cartan: every real-analytic surface metric is locally realizable analytically in $\mathbb R^3$ (Janet 1926; Cartan 1927).
• 1954–1955 — Nash and Kuiper: $C^1$ isometric realizations exist with great flexibility (Nash 1954; Kuiper 1955). At $C^1$ regularity there is no curvature constraint.
• 1971 — Pogorelov constructs a $C^{2,1}$ metric with no local $C^2$ realization (Pogorelov 1971).
• 1985–1986 — C.-S. Lin: local realization for nonnegative curvature and for curvature changing sign cleanly, with finite differentiability (Lin 1985; Lin 1986).
• 1989 — Nakamura and Maeda: smooth local existence when the curvature changes sign cleanly (Trans. AMS 1989).
• 2002 — A Nadirashvili–Yuan preprint states a smooth counterexample with $K\le0$ (arXiv:math/0208127); their published 2008 paper instead proves a $C^{2,1}$ counterexample with $K\ge0$ and leaves the smooth question open (Calc. Var. PDE 2008).
• 2007–2009 — Khuri: counterexamples to local solvability for general Monge–Ampère equations (CPDE 2007), and work on Darboux's equation that leaves the needed curvature profile open (Khuri 2009).
• 2010–2016 — Positive results under finite-order conditions on the curvature zero set (Han–Khuri 2010; T.-Y. Lin 2016).
• 2026 — An OpenAI preprint, A Smooth Metric with No Local Isometric Immersion into Three-Space (OpenAI Math Release, September 24, 2026), claims a smooth metric on $(-1,1)^2$ that has no smooth isometric immersion on any neighborhood of the origin. It has not been peer reviewed, and the claim has not been formally verified.

Setting

Work in coordinates $p=(p_1,p_2)$ on the open square $Q=(-1,1)^2\subset\mathbb R^2$. A Riemannian metric on $Q$ is a map $p\mapsto g(p)$ to symmetric $2\times2$ real matrices that are positive definite; it is $C^\infty$ if every entry $g_{ij}$ is smooth. An isometric immersion of $(U,g)$, for an open set $U\subseteq Q$, is a map $F:U\to\mathbb R^3$ whose differential reproduces $g$:

$$\langle dF_p(v),\,dF_p(w)\rangle_{\mathbb R^3}=v^{\mathsf T} g(p)\,w\qquad(p\in U,\ v,w\in\mathbb R^2),$$

equivalently $\langle\partial_iF,\partial_jF\rangle=g_{ij}$. Positive definiteness forces $dF$ to have rank $2$. In Lean, Coord = Fin 2 → ℝ, Ambient = EuclideanSpace ℝ (Fin 3), square is $Q$, and LocalSmoothPositive packages smoothness of every entry and Matrix.PosDef at every point.

Formalization targets

Goal: a nonrealizable smooth metric (Theorem A)

$$\exists\, g\ \text{smooth, positive definite on } Q\ \text{ such that for every open } U\subseteq Q \text{ with } 0\in U,\ \text{there is no } C^\infty\ F:U\to\mathbb R^3 \text{ with } F^*\langle\cdot,\cdot\rangle=g .$$

This is Theorem A of the source (p. 1). Because a smooth isometric immersion restricts to an embedding near any point, it also rules out local smooth isometric embeddings. The stronger statement that $g$ can be chosen with the full Euclidean Taylor jet at the origin (Corollary 5.3) is not part of the goal. The goal is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. The theorem shows that smooth local isometric realization in $\mathbb R^3$ can fail, which answers negatively the unrestricted smooth problem recorded by Yau and Ghomi. It separates the smooth case from the analytic case (Janet–Cartan) and from finite regularity (Pogorelov, Nadirashvili–Yuan 2008). It also shows, by Corollary 5.3, that the infinite-order jet of the metric at a point does not decide realizability. It leaves open the same question under a sign condition $K\ge0$ or $K\le0$, since the construction uses both signs of curvature.

Formalizing it. The statement is short, but the claimed proof combines PDE estimates for Darboux's equation, hyperbolic propagation, a Baire-category argument and a boundary-saddle geometric step. The literature has disagreed about the status of the smooth question (NY2002 versus NY2008), so a machine-checked proof would remove the ambiguity. Mathlib has the manifold calculus needed to state the result (ContMDiff, mfderiv) but none of the PDE layer.

Difficulty

Where the Gaussian curvature $K$ is nonzero, the realization equations are elliptic or hyperbolic and can be solved locally, so any counterexample must exploit degeneracy where $K$ vanishes and changes type. Finite-regularity counterexamples (Pogorelov) do not carry over: existence at every finite order, on neighborhoods that shrink with the order, does not give one smooth map on a fixed neighborhood. Nonsolvable Monge–Ampère equations are also not enough by themselves, because the coefficients of the Darboux equation come from the same metric, so the obstruction has to be built into $g$ itself. Finally, the conclusion must hold for every neighborhood of the origin and every smooth immersion, with no a priori bounds on $F$.

Formalization scope

• The metric is a function on the subtype of the open set coordinateSquareOpen with values in Matrix (Fin 2) (Fin 2) ℝ. Each entry is ContMDiff … ∞ and each value is Matrix.PosDef, which includes symmetry (Hermitian over ℝ).
• The quantifier ranges over all U : Opens Coord with $U\subseteq Q$ and $0\in U$, and over all maps F : U → Ambient that are ContMDiff … ∞ on the open submanifold $U$. The isometry condition is stated with mfderiv and the Euclidean inner product: $\langle dF_p v, dF_p w\rangle = v\cdot(g(p)w)$.
• The conclusion is a negation of existence, so it is not trivialized by a junk value: $g$ must be genuinely smooth and positive definite, and an immersion on any neighborhood, however small, is excluded.
• Infrastructure needed: Gauss equation and second fundamental form in coordinates, Darboux's equation, energy and weighted elliptic estimates, hyperbolic propagation, and the Baire category theorem (available in Mathlib). The surface-theory layer is reusable for other isometric-embedding projects.

Selected references

• M. Janet, Sur la possibilité de plonger un espace riemannien donné dans un espace euclidien, Ann. Soc. Polon. Math. 5 (1926), 38–43. https://rcin.org.pl/dlibra/publication/31746/edition/15034
• É. Cartan, Sur la possibilité de plonger un espace riemannien donné dans un espace euclidien, Ann. Soc. Polon. Math. 6 (1927), 1–7. https://rcin.org.pl/dlibra/publication/32955/edition/18106
• J. Nash, $C^1$ isometric imbeddings, Ann. of Math. 60 (1954), 383–396. https://doi.org/10.2307/1969840
• N. H. Kuiper, On $C^1$-isometric imbeddings. I, Nederl. Akad. Wetensch. Proc. Ser. A 58 (1955), 545–556.
• A. V. Pogorelov, An example of a two-dimensional Riemannian metric admitting no local realization in $E^3$, Dokl. Akad. Nauk SSSR 198 (1971), 42–43. https://www.mathnet.ru/eng/dan36135
• C.-S. Lin, The local isometric embedding in $\mathbb R^3$ of 2-dimensional Riemannian manifolds with nonnegative curvature, J. Differential Geom. 21 (1985), 213–230. https://doi.org/10.4310/jdg/1214439563
• C.-S. Lin, The local isometric embedding in $\mathbb R^3$ of two-dimensional Riemannian manifolds with Gaussian curvature changing sign cleanly, Comm. Pure Appl. Math. 39 (1986), 867–887. https://doi.org/10.1002/cpa.3160390607
• G. Nakamura and Y. Maeda, Local smooth isometric embeddings of low-dimensional Riemannian manifolds into Euclidean spaces, Trans. Amer. Math. Soc. 313 (1989), 1–51. https://doi.org/10.1090/S0002-9947-1989-0992597-8
• N. Nadirashvili and Y. Yuan, Counterexamples for local isometric embedding, preprint (2002). https://arxiv.org/abs/math/0208127v1
• N. Nadirashvili and Y. Yuan, Improving Pogorelov's isometric embedding counterexample, Calc. Var. PDE 32 (2008), 319–323. https://doi.org/10.1007/s00526-007-0140-7
• M. A. Khuri, Counterexamples to the local solvability of Monge–Ampère equations in the plane, Comm. PDE 32 (2007), 665–674. https://doi.org/10.1080/03605300600635061
• M. A. Khuri, On the local solvability of Darboux's equation, Discrete Contin. Dyn. Syst. (2009, Supplement), 451–456. https://doi.org/10.3934/proc.2009.2009.451
• Q. Han and M. Khuri, Comm. Anal. Geom. 18 (2010), 649–704. https://doi.org/10.4310/CAG.2010.v18.n4.a2
• T.-Y. Lin, Comm. PDE 41 (2016), 1553–1592. https://doi.org/10.1080/03605302.2016.1227336
• S.-T. Yau, Review of geometry and analysis, Asian J. Math. 4 (2000), 235–278. https://doi.org/10.4310/AJM.2000.v4.n1.a16
• M. Ghomi, Open problems in geometry of curves and surfaces, survey (2019), §1.5. https://ghomi.math.gatech.edu/Papers/op.pdf
• OpenAI, A Smooth Metric with No Local Isometric Immersion into Three-Space, OpenAI Math Release preprint, September 24, 2026 (Theorem A, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Smooth-Metric-with-No-Local-Isometric-Immersion-into-Three-Space-September-24-2026/paper.pdf

Motivation

An isometric immersion realizes an abstract Riemannian manifold as a surface in Euclidean space whose induced lengths are exactly the prescribed ones. How many dimensions are needed is a classical question. Nash showed that every compact Riemannian $n$-manifold embeds smoothly and isometrically in some Euclidean space; for surfaces his bound is $\mathbb R^{17}$ (Nash 1956). Gromov lowered the immersion dimension for closed surfaces to $\mathbb R^5$ (Partial Differential Relations, 1986, §3.2.4). Three dimensions do not suffice even locally in the smooth category, and Gromov recorded the question whether every smooth Riemannian surface admits a smooth isometric immersion into $\mathbb R^4$ (Gromov 2000, §I, Remark (d)), later attributing it to Chern around 1950 (Gromov 2015, p. 4).

This mission asks for a machine-checked proof of Theorem 1.1 of an OpenAI preprint dated September 23, 2026 (source), which answers the compact, boundaryless form of that question: every closed smooth Riemannian surface admits a smooth isometric immersion into $\mathbb R^4$. The preprint has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal is open.

Background

• 1926–1927 — Janet and Cartan: analytic Riemannian surfaces embed locally isometrically in $\mathbb R^3$ (Janet 1926; Cartan 1927).
• 1954–1955 — Nash and Kuiper: strictly short immersions in positive codimension can be uniformly approximated by $C^1$ isometric immersions (Nash 1954; Kuiper 1955).
• 1956 — Nash's smooth embedding theorem, dimension $n(3n+11)/2$, i.e. $17$ for surfaces.
• 1973 — Poznyak: $C^{3,\alpha}$ metrics on compact parts of simply connected planar domains admit $C^{2,\alpha}$ isometric immersions into $\mathbb R^4$ (Russ. Math. Surveys 1973).
• 1986 — Gromov: smooth isometric immersions of closed surfaces into $\mathbb R^5$.
• 2026 — Lewicka proves $C^{1,\alpha}$ flexibility in $\mathbb R^4$ for low-regularity metrics on disk-type planar domains (arXiv:2511.16305); a companion OpenAI preprint gives a smooth metric on a square with no local smooth isometric immersion into $\mathbb R^3$; the present preprint claims the closed-surface case in $\mathbb R^4$ (Theorem 1.1, p. 2).

Setting

A closed surface $M$ is a compact smooth two-dimensional manifold without boundary; it need not be orientable or connected. A Riemannian metric $g$ assigns to each $p\in M$ a positive definite inner product $g_p$ on $T_pM$, depending smoothly on $p$. A smooth map $F:M\to\mathbb R^4$ is an isometric immersion if

$$\langle dF_p(v),dF_p(w)\rangle=g_p(v,w)\qquad(p\in M,\ v,w\in T_pM).$$

Positive definiteness of $g$ forces $dF_p$ to be injective, so $F$ is an immersion; self-intersections are allowed.

Formalization targets

Goal: Theorem 1.1 (p. 2)

For every closed smooth Riemannian surface $(M,g)$ there is a $C^\infty$ map $F:M\to\mathbb R^4$ with $F^*\delta_4=g$, where $\delta_4=\sum_{i=1}^4dx_i^2$. In Lean this is OAI.ClosedSurfaceR4.FiniteOrderSmoothing.smooth_isometric_immersion.

Significance

The result itself. The theorem lowers Gromov's immersion dimension for closed surfaces from five to four, with no restriction on curvature or topology, and settles the closed case of the question Gromov attributes to Chern. Dimension four is the first codimension in which the smooth problem can have a global answer for all surfaces, since smooth metrics with no local isometric immersion into $\mathbb R^3$ exist. The open (noncompact) case of the question is not addressed.

Formalizing it. Mathlib now has smooth manifolds, tangent bundles and smooth Riemannian metrics, so the statement is expressible without custom geometry. A complete proof would add Whitney's immersion theorem, Sard's theorem in equal dimensions, metric decompositions into rank-one terms, Nash–Moser-type smoothing estimates, and oscillatory correction schemes; none of these are formalized at this level, and all are reusable in geometric analysis.

Difficulty

The isometric immersion equation $dF^{\mathsf T}dF=g$ is a nonlinear system of three equations in four unknown functions, and its linearization loses derivatives, so a direct implicit function argument fails. Convex integration in the Nash–Kuiper style produces only $C^1$ solutions. Poznyak's smooth theory works on planar domains with boundary, but on a closed surface the successive local corrections must remain compatible globally. The preprint keeps a nondegenerate normal geometry (a nonzero vector-valued second fundamental form) through every step, adds the metric deficit one positive rank-one term $a^2dx^2$ at a time via a velocity loop in a plane normal to $F_y$ and $F_{yy}$ (Proposition 3.1, p. 8; Proposition 7.1, p. 25), and then corrects the approximate metric exactly by a smoothing scheme that solves the linearized equation only on oscillatory modes (Proposition 5.1, p. 15). Nonorientable surfaces are handled by starting from an immersion into a small round $3$-sphere, whose radial direction is a global normal (Lemma 9.1, p. 35).

Formalization scope

• $M$ is a type with ChartedSpace (EuclideanSpace ℝ (Fin 2)) M and IsManifold 𝓘(ℝ, ℝ²) ∞ M, assumed compact, Hausdorff and second countable. Being modeled on $\mathbb R^2$ (not a half-space) encodes "without boundary"; no orientability or connectedness is assumed.
• The metric is Mathlib's Bundle.ContMDiffRiemannianMetric of class $C^\infty$ on the tangent bundle.
• The conclusion asks for ContMDiff … ∞ F and equality of the Euclidean inner product of mfderiv images with g.inner p v w for all tangent vectors; immersivity follows and is not stated separately.
• The statement is not trivialized: the conclusion is an exact pointwise identity for a smooth map, and the hypotheses are satisfied by every closed surface with any metric.

Selected references

• OpenAI, Smooth isometric immersions of closed surfaces into Euclidean four-space, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Smooth-isometric-immersions-of-closed-surfaces-into-Euclidean-four-space-September-23-2026/paper.pdf
• J. Nash, The imbedding problem for Riemannian manifolds, Ann. of Math. 63 (1956). https://doi.org/10.2307/1969989
• J. Nash, C¹-isometric imbeddings, Ann. of Math. 60 (1954). https://doi.org/10.2307/1969840
• M. Gromov, Partial Differential Relations, Springer (1986). https://doi.org/10.1007/978-3-662-02267-2
• M. Gromov, Spaces and questions, Geom. Funct. Anal. (2000). https://www.ihes.fr/~gromov/wp-content/uploads/2018/08/SpacesandQuestions.pdf
• M. Gromov, Geometric, algebraic and analytic descendants of Nash isometric embedding theorems (2015). https://www.ihes.fr/~gromov/wp-content/uploads/2018/08/nash-copy-Oct9.pdf
• E. G. Poznyak, Isometric immersions of two-dimensional Riemannian metrics in Euclidean space, Russian Math. Surveys (1973). https://doi.org/10.1070/RM1973v028n04ABEH001591
• M. Lewicka, Full flexibility of isometric immersions of metrics with low Hölder regularity in Poznyak theorem's dimension, arXiv:2511.16305v3 (2026). https://arxiv.org/abs/2511.16305v3
• H. Whitney, The singularities of a smooth n-manifold in (2n−1)-space, Ann. of Math. 45 (1944). https://doi.org/10.2307/1969266
• R. S. Hamilton, The inverse function theorem of Nash and Moser, Bull. AMS 7 (1982). https://doi.org/10.1090/S0273-0979-1982-15004-2

Motivation

How rigid is a von Neumann algebra inside $B(H)$? If two algebras $M,N\subseteq B(H)$ have unit balls that are uniformly close, must they be the same algebra up to a small change of coordinates? Kadison and Kastler introduced the distance between the unit balls in 1972 (Amer. J. Math. 1972) and asked whether sufficiently close algebras are spatially isomorphic, implemented by a unitary close to the identity. The positive answer for a class of algebras is called (strong) Kadison–Kastler stability. The problem connects perturbation theory, Hochschild cohomology, and Kadison's similarity problem, and it was settled previously only for injective (amenable) algebras, type I algebras, and specific nonamenable examples.

This mission asks for a formal proof of the uniform strong Kadison–Kastler stability theorem stated in an OpenAI preprint dated September 23, 2026 (source): a single tolerance works for all von Neumann algebras on all Hilbert spaces. The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

• 1972 — Kadison and Kastler introduce the metric and prove stability results for type I algebras (Amer. J. Math. 1972).
• 1974–1975 — Phillips proves spatial isomorphism for close type I algebras (Pacific J. Math. 1974); Christensen obtains a conjugating unitary near the identity (J. LMS 1975).
• 1977 — Christensen (Invent. Math. 1977), Johnson (Proc. LMS 1977) and Raeburn–Taylor (JFA 1977) settle the injective case.
• 1980 — Christensen's theory of near inclusions (Acta Math. 1980).
• 1982 — Johnson's examples show that for C*-algebras the implementing unitary cannot always be chosen near the identity in a uniform way (Canad. Math. Bull. 1982).
• 1983 — Haagerup's cyclic similarity estimate (Ann. of Math. 1983).
• 2010–2012 — Christensen, Sinclair, Smith, White and Winter prove spatial isomorphism for close separable nuclear C*-algebras (PNAS 2010; Acta Math. 2012).
• 2012–2014 — Cameron, Christensen, Sinclair, Smith, White and Wiggins construct the first nonamenable Kadison–Kastler stable factors, $(L^\infty(X)\rtimes SL_n(\mathbb Z))\bar\otimes R$ for $n\ge3$ (PNAS 2012; Duke 2014).
• September 2026 — The OpenAI preprint claims uniform stability for all von Neumann algebras (Theorem 1.1, p. 2).

Setting

Let $H$ be a complex Hilbert space and $B(H)$ the bounded operators with the operator norm. A von Neumann algebra $M\subseteq B(H)$ is a unital $*$-subalgebra equal to its double commutant (in particular it contains the identity $I_H$). Write $M_1=\{x\in M:\|x\|\le1\}$ for its unit ball. The Kadison–Kastler distance is the Hausdorff distance of unit balls,

$$d(M,N)=\max\Bigl(\sup_{x\in M_1}\inf_{y\in N_1}\|x-y\|,\ \sup_{y\in N_1}\inf_{x\in M_1}\|x-y\|\Bigr).$$

A unitary $u\in B(H)$ conjugates $M$ to $N$ if $uMu^*=N$.

Formalization targets

Goal: Theorem 1.1 (p. 2)

For every $\varepsilon>0$ there is $\delta>0$ such that for every complex Hilbert space $H$ and all von Neumann algebras $M,N\subseteq B(H)$ with $d(M,N)<\delta$, there is a unitary $u\in B(H)$ with

$$uMu^*=N\qquad\text{and}\qquad\|u-I_H\|<\varepsilon .$$

The tolerance $\delta$ depends only on $\varepsilon$: not on the algebras, their type, their representations, or the size of $H$.

Significance

The result itself. It answers the Kadison–Kastler perturbation question in its strongest uniform form for von Neumann algebras, including all nonamenable and type III cases and non-separable Hilbert spaces. Consequences include that every algebraic or analytic invariant preserved by unitary conjugacy (type, factoriality, property $\Gamma$, Cartan subalgebras) is locally constant in the Kadison–Kastler metric. The analogous C*-algebra statement fails in its uniform-unitary form by Johnson's examples, so the theorem is specific to von Neumann algebras.

Formalizing it. The statement uses only Mathlib's VonNeumannAlgebra, unitary operators and Hausdorff distance, so it is fully expressible today. The proof, however, draws on free probability, tracial ultraproducts, Tomita–Takesaki theory, crossed products, Poisson boundaries and measurable cocycles, most of which are absent from Mathlib. Formalizing even the amenable (injective) case would be a substantial reusable contribution.

Difficulty

Closeness of unit balls supplies nearby elements but no linear or multiplicative correspondence between the algebras, and it gives no control at matrix levels, where perturbation arguments naturally live. For nonamenable algebras the classical route through vanishing Hochschild cohomology is unavailable. The preprint proceeds by cases. For finite factors it proves a uniform bound on all matrix amplifications of commutator maps (Theorem 3.1, p. 11) and corrects nearby unitaries to a measurable cocycle over an amenable boundary action (Section 4). Infinite factors require comparing modular groups through Tomita graphs (Proposition 6.5, p. 41) and aligning the modular action (Proposition 7.1, p. 45) before passing to crossed products (Theorem 8.4, p. 59). General algebras then require aligning centers and passing from separable to arbitrary Hilbert spaces (Section 9) without losing uniformity.

Formalization scope

• $H$ ranges over complex Hilbert spaces (NormedAddCommGroup, InnerProductSpace ℂ, CompleteSpace) in a fixed universe u; $\delta$ is chosen before $H$, so the uniformity over Hilbert spaces is part of the statement.
• VonNeumannAlgebra H is Mathlib's notion; these algebras contain the identity, so "unital with identity $I_H$" is built in.
• kkDistance M N is Metric.hausdorffDist of the closed unit balls. Both balls contain $0$ and are bounded, so the Hausdorff distance is finite and the definition is exactly (1.1).
• NearConjugacy M N ε asks for a unitary $v$ with $v\,M\,v^*=N$ as sets and $\|v-1\|<\varepsilon$.
• There is no trivializing reading: the hypotheses are satisfied by $M=N$, and the conclusion is nontrivial for $M\neq N$.

Selected references

• OpenAI, Universal strong Kadison–Kastler stability, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Universal-strong-Kadison-Kastler-stability-September-23-2026/paper.pdf
• R. V. Kadison, D. Kastler, Perturbations of von Neumann algebras. I. Stability of type, Amer. J. Math. 94 (1972). https://doi.org/10.2307/2373592
• E. Christensen, Perturbations of type I von Neumann algebras, J. London Math. Soc. (1975). https://doi.org/10.1112/jlms/s2-9.3.395
• E. Christensen, Perturbation of operator algebras, Invent. Math. 43 (1977). https://doi.org/10.1007/BF01390201
• B. E. Johnson, Perturbations of Banach algebras, Proc. London Math. Soc. (1977). https://doi.org/10.1112/plms/s3-34.3.439
• I. Raeburn, J. L. Taylor, Hochschild cohomology and perturbations of Banach algebras, J. Funct. Anal. (1977). https://doi.org/10.1016/0022-1236(77)90072-6
• E. Christensen, Near inclusions of C-algebras*, Acta Math. 144 (1980). https://doi.org/10.1007/BF02392125
• B. E. Johnson, A counterexample in the perturbation theory of C-algebras*, Canad. Math. Bull. 25 (1982). https://doi.org/10.4153/CMB-1982-043-4
• U. Haagerup, Solution of the similarity problem for cyclic representations of C-algebras*, Ann. of Math. 118 (1983). https://doi.org/10.2307/2007028
• E. Christensen, A. M. Sinclair, R. R. Smith, S. A. White, W. Winter, Perturbations of nuclear C-algebras*, Acta Math. 208 (2012). https://doi.org/10.1007/s11511-012-0075-5
• J. Cameron, E. Christensen, A. M. Sinclair, R. R. Smith, S. A. White, A. D. Wiggins, Kadison–Kastler stable factors, Duke Math. J. 163 (2014). https://doi.org/10.1215/00127094-2819736

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

In Bernoulli bond percolation on a graph $G=(V,E)$, each edge is kept (open) independently with probability $p$. As $p$ grows, an infinite connected component of open edges appears at the critical probability $p_c(G)$. The criticality problem asks whether an infinite cluster can already exist at $p_c$. A negative answer means the phase transition is continuous. Benjamini and Schramm (1996) conjectured that, on every graph with a large symmetry group and $p_c<1$, there is no infinite cluster at $p_c$. The question contains the famous open case of $\mathbb Z^3$ and connects percolation to geometric group theory, since Cayley graphs of finitely generated groups are the main examples.

Timeline

• 1957. Broadbent and Hammersley introduce percolation (doi:10.1017/S0305004100032680).
• 1960, 1980. Harris and Kesten settle nearest-neighbour bond percolation on $\mathbb Z^2$, including $\theta(p_c)=0$ (doi:10.1017/S0305004100034241, doi:10.1007/BF01197577).
• 1986–1987. Menshikov and Aizenman–Barsky prove sharpness of the subcritical phase; this does not settle behaviour at $p_c$ (doi:10.1007/BF01212322).
• 1990. Hara and Slade prove mean-field behaviour, including $\theta(p_c)=0$, for $\mathbb Z^d$ in sufficiently high dimension (doi:10.1007/BF02108785).
• 1996. Benjamini and Schramm formulate the conjecture for quasi-transitive graphs with $p_c<1$ (doi:10.1214/ECP.v1-978).
• 1999. Benjamini, Lyons, Peres and Schramm prove it for nonamenable graphs with a unimodular quasi-transitive action (doi:10.1214/aop/1022677450).
• 2006. Timár excludes infinitely many infinite critical clusters on nonunimodular transitive graphs (doi:10.1214/009117906000000494).
• 2016. Hutchcroft proves the conjecture for every quasi-transitive graph of exponential growth (arXiv:1605.05301). Duminil-Copin, Sidoravicius and Tassion treat slabs (doi:10.1002/cpa.21641).
• 2017. Fitzner and van der Hofstad reach nearest-neighbour $\mathbb Z^d$, $d\ge11$ (arXiv:1506.07977).
• 2021. Hermon and Hutchcroft cover certain groups of intermediate growth (arXiv:1809.11112).
• 2024. Kozma and Nitzan reduce the $\mathbb Z^d$ case to a conjectured gluing inequality (arXiv:2401.12397).
• 2026. Public, non-peer-reviewed announcements report AI-assisted proofs for $\mathbb Z^d$, including a reported Lean formalization of the lattice case (Leder, August 2026).

The source of this mission is an OpenAI preprint dated September 24, 2026, which treats the remaining subexponential-growth case for all quasi-transitive graphs.

Setting

A graph here has vertex set $V$ and a set $E$ of labelled bonds, each with a pair of endpoints; loops and parallel bonds are allowed. It is locally finite if each vertex lies in finitely many bonds, connected if any two vertices are joined by a path, and quasi-transitive if its automorphism group (bijections of vertices and of bonds respecting endpoints) has finitely many orbits on $V$. Examples include $\mathbb Z^d$ and every Cayley graph of a finitely generated group.

For $p\in[0,1]$, let $\mathbb P_p$ be the law of a random set $\omega\subseteq E$ containing each bond independently with probability $p$. The cluster $C_x(\omega)$ of $x$ is the set of vertices joined to $x$ by a finite path of bonds in $\omega$ (including $x$). Define

$$p_c(G)=\inf\{p\in[0,1]:\ \mathbb P_p(\exists x,\ |C_x|=\infty)>0\}.$$

Formalization targets

Goal: Theorem 1.1

For every infinite, connected, locally finite, quasi-transitive graph $G$,

$$p_c(G)<1\ \Longrightarrow\ \mathbb P_{p_c(G)}\bigl(\exists x\in V:\ |C_x|=\infty\bigr)=0.$$

The hypothesis $p_c<1$ is necessary, since at $p=1$ every infinite connected graph percolates. The Lean statement OAI.CriticalPercolation.BondGraph.no_percolation_at_criticality is open on the platform.

Significance

Theorem 1.1 resolves the Benjamini–Schramm criticality conjecture for Bernoulli bond percolation, and in particular gives $\theta(p_c)=0$ on $\mathbb Z^d$ for every $d\ge2$ (Corollary 10.1, p. 39), including the long-open case $d=3$. With Hutchcroft's exponential-growth theorem, the remaining work is the subexponential case, divided into superpolynomial growth and growth bounded by a polynomial along a sequence of scales. As a consequence the percolation probability is continuous at $p_c$ on every such graph.

The result is proved in an OpenAI preprint that has not been peer reviewed. No machine-checked proof of the general quasi-transitive statement exists; the reported Lean formalization concerns only nearest-neighbour $\mathbb Z^d$. A formal proof would also certify the structural input (Tessera–Tointon's finitary structure theorem) as used here.

Difficulty

The obvious strategy, renormalization from large finite boxes, needs a gluing inequality to connect independently found large clusters, and it needs coordinates: on a general quasi-transitive graph there is no lattice to place boxes in. Planar duality is unavailable, the lace expansion needs high dimension, and Hutchcroft's argument uses exponential growth essentially. In the superpolynomial case one must rule out two large distinct clusters adjacent across an edge; in the polynomial case one needs nilpotent-group coordinates (Gromov, Trofimov, Tessera–Tointon) and a two-direction corridor exploration in which conditional failure probabilities stay uniformly small. Neither uniqueness of the infinite cluster nor independence across coarse blocks can be assumed.

Formalization scope

• BondGraph V E stores ends : E → Sym2 V; loops and parallel bonds are allowed. LocallyFinite counts bonds at each vertex. Clusters use SimpleGraph.fromEdgeSet of the open bonds, so loops are discarded and parallel bonds collapse; reachability includes the zero-length path.
• Aut consists of a vertex bijection and a bond bijection that commute with ends; QuasiTransitive says some finite set of vertices meets every orbit.
• law p is ProbabilityTheory.setBernoulli Set.univ p on Set E: each bond retained independently with probability p : unitInterval.
• criticalProbability is sInf in unitInterval of $\{p:\mathbb P_p(\text{percolates})>0\}$; if the set were empty this would be $1$, which hpc excludes.
• percolates is the event that some cluster is infinite; the conclusion says it has measure $0$ at $p_c$.

A complete development needs Bernoulli product measures, Harris–FKG and conditional correlation inequalities, Hutchcroft's exponential-growth theorem, volume-growth theory of quasi-transitive graphs, and the Gromov–Trofimov–Tessera–Tointon structure theory. Each of these is reusable well beyond this mission. Contributions formalizing Proposition 3.1 (two-cluster bound), Theorem 6.1 (joint gluing), Theorem 7.1 (criticality with a nilpotent quotient action) or Proposition 9.3 (subcritical exploration), or the cited Theorem 2.2 (Hutchcroft), are welcome.

Selected references

• OpenAI, No percolation at criticality on quasi-transitive graphs, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/No-percolation-at-criticality-on-quasi-transitive-graphs-September-24-2026/paper.pdf
• I. Benjamini, O. Schramm, Percolation beyond $\mathbb Z^d$, many questions and a few answers, Electron. Commun. Probab., 1996. https://doi.org/10.1214/ECP.v1-978
• I. Benjamini, R. Lyons, Y. Peres, O. Schramm, Critical percolation on any nonamenable group has no infinite clusters, Ann. Probab., 1999. https://doi.org/10.1214/aop/1022677450
• T. Hutchcroft, Critical percolation on any quasi-transitive graph of exponential growth has no infinite clusters, C. R. Math., 2016. https://doi.org/10.1016/j.crma.2016.07.013
• J. Hermon, T. Hutchcroft, No percolation at criticality on certain groups of intermediate growth, IMRN, 2021. https://doi.org/10.1093/imrn/rnz265
• R. Tessera, M. C. H. Tointon, A finitary structure theorem for vertex-transitive graphs of polynomial growth, Combinatorica, 2021. https://doi.org/10.1007/s00493-020-4295-6
• G. Kozma, S. Nitzan, A reduction of the θ(p_c)=0 problem to a conjectured inequality, preprint, 2024. https://arxiv.org/abs/2401.12397
• T. Hara, G. Slade, Mean-field critical behaviour for percolation in high dimensions, Comm. Math. Phys., 1990. https://doi.org/10.1007/BF02108785
• H. Kesten, The critical probability of bond percolation on the square lattice equals 1/2, Comm. Math. Phys., 1980. https://doi.org/10.1007/BF01197577
• Á. Timár, Percolation on nonunimodular transitive graphs, Ann. Probab., 2006. https://doi.org/10.1214/009117906000000494

Motivation: tensor squares that contain everything

The irreducible complex representations of the symmetric group $S_n$ are indexed by partitions $\lambda\vdash n$ and written $S^\lambda$ (Specht modules). Decomposing a tensor product $S^\lambda\otimes S^\mu$ (with the diagonal action) into irreducibles is governed by the Kronecker coefficients

$$g(\lambda,\mu,\nu)=\dim\operatorname{Hom}_{S_n}\!\big(S^\nu,\,S^\lambda\otimes S^\mu\big),$$

which have no known positive combinatorial formula and are a central open topic in algebraic combinatorics and geometric complexity theory. A basic test of how far tensor products spread is the tensor square conjecture: in every degree (with a few exceptions) some single irreducible representation has a tensor square containing every irreducible representation.

Timeline

• 2012 — Saxl proposes (UCLA Combinatorics Seminar, 20 March 2012) that the staircase $\rho_m=(m,m-1,\dots,1)$ at triangular degree $n=m(m+1)/2$ has this property; recorded by Pak, Panova and Vallejo.
• 2013 — Heide, Saxl, Tiep and Zalesski conjecture an analogous covering property for alternating simple groups (HSTZ 2013, Rem. 1.3(3)).
• 2013/2016 — Pak, Panova and Vallejo state the tensor square conjecture for $n\ge3$, $n\ne4,9$, and the Saxl conjecture, and give a character-nonvanishing criterion (PPV 2016, Conj. 1.1–1.2, Lemma 1.3).
• 2015 — Ikenmeyer proves the staircase assertion for all $\nu$ comparable with the staircase in dominance order (Ikenmeyer 2015, Thm 2.1).
• 2017 — Luo and Sellke: staircase squares contain almost all partitions, and fourth powers cover everything in large degree (Luo–Sellke 2017).
• 2018 — Bessenrodt: all double-hook constituents (Bessenrodt 2018, Thm 4.10).
• 2021 — Li: the triple-hook case, and a conjectured family for nontriangular degrees (Li 2021).
• 2023 — Harman and Ryba: staircase tensor cubes contain everything (Harman–Ryba 2023, Thm 1.1).
• 2026 — An OpenAI preprint, Universal Tensor Squares for Symmetric Groups (OpenAI Math Release, September 24, 2026), claims the tensor square conjecture for every $n\notin\{2,4,9\}$, building on a companion preprint that proves Saxl's conjecture in a cyclic form. Neither preprint is peer reviewed and the main theorem is not formally verified; its proof uses exact computer calculations for degrees up to $64$.

Setting

For a Young diagram $\lambda$ with $n$ cells, fix a bijection $t$ between $\{0,\dots,n-1\}$ and the cells (a tableau). The Lean development realizes $S^\lambda$ inside the space of functions on words $\mathrm{Fin}\,n\to\mathrm{Fin}\,d$ ($d$ = number of rows), with $S_n$ acting by permuting letters: the polytabloid $e_t$ is the signed sum, over the column group of $t$, of the permuted indicator of the row word of $t$, and Specht t is the $\mathbb C$-span of the $S_n$-orbit of $e_t$. The Kronecker coefficient kronecker a b t is finrank of the space of $S_n$-intertwining maps from spechtRep t to the tensor product spechtRep a ⊗ spechtRep b. canonicalTableau λ is a fixed tableau of shape $\lambda$.

Formalization targets

Goal: a universal tensor square in every degree $n\notin\{2,4,9\}$

For every positive integer $n$ with $n\ne2,4,9$ there is a partition $\lambda\vdash n$ such that

$$g(\lambda,\lambda,\nu)>0\qquad\text{for every }\nu\vdash n ,$$

so the tensor square $S^\lambda\otimes S^\lambda$ contains every irreducible representation of $S_n$. The Lean statement asserts, for one Young diagram $\lambda$ with $n$ cells: positivity of kronecker for every target diagram $\nu$ with $n$ cells; irreducibility of spechtRep for $\lambda$; and that every finite-dimensional irreducible complex representation of $S_n$ admits an injective intertwining map into $S^\lambda\otimes S^\lambda$. This is Theorem 1.1 of the source together with its "thus" sentence. The goal is published on the platform with status Open.

Significance

The result itself. The theorem settles the tensor square conjecture of Pak, Panova and Vallejo, including all nontriangular degrees. Since the sign representation occurs, the chosen $\lambda$ must be self-conjugate. Via Letellier's results it also gives tensor squares of unipotent characters of $\mathrm{GL}_n(\mathbb F_q)$ that contain every unipotent character (Corollary 1.2 of the source). The companion cyclic Saxl theorem is used as input at staircase degrees.

Formalizing it. The proof combines representation-theoretic constructions with exact finite computations (Murnaghan–Nakayama recursion for all eligible $n\le64$, and capacity calculations), which the source certifies by included programs. A formal proof would replace these with checked computation and would require building Specht modules, Kronecker coefficients and branching rules in Lean, infrastructure Mathlib currently lacks.

Difficulty

Knowing that a smaller staircase square contains every constituent does not transfer to an enlarged diagram: constituents must survive a map from the actual enlarged tensor square, and the attached cells introduce alternating terms that can cancel. Almost-all or higher-power results (Luo–Sellke, Harman–Ryba) do not give a universal square. Small degrees cannot be handled by asymptotic estimates and require exact Kronecker computations, and $n=2,4,9$ are genuine exceptions.

Formalization scope

• Partitions are Mathlib YoungDiagrams with card = n; the representation space is (Fin n → Fin d) → ℂ, and Specht t is the cyclic span of one polytabloid. kronecker is Module.finrank ℂ of Representation.IntertwiningMap, so it is the genuine multiplicity of $S^\nu$ in the tensor square.
• The third conjunct quantifies over all finite-dimensional complex irreducible representations in a fixed universe; proving it requires that every irreducible of $S_n$ is isomorphic to some Specht module. The second conjunct (irreducibility of $S^\lambda$) is a standard fact the source uses implicitly.
• $n>0$ and $n\ne2,4,9$ match the source; $n=1$ is trivial.
• Needed infrastructure: Specht module theory (irreducibility, completeness), characters and Murnaghan–Nakayama, Littlewood–Richardson branching, verified computation for $n\le 64$. The Specht and Kronecker layer is shared with the companion Saxl mission.

Selected references

• I. Pak, G. Panova and E. Vallejo, Kronecker products, characters, partitions, and the tensor square conjectures, Adv. Math. 288 (2016), 702–731. https://doi.org/10.1016/j.aim.2015.11.002
• G. Heide, J. Saxl, P. H. Tiep and A. E. Zalesski, Conjugacy action, induced representations and the Steinberg square for simple groups of Lie type, Proc. London Math. Soc. 106 (2013), 908–930. https://doi.org/10.1112/plms/pds062
• C. Ikenmeyer, The Saxl conjecture and the dominance order, Discrete Math. 338 (2015), 1970–1975. https://doi.org/10.1016/j.disc.2015.04.027
• S. Luo and M. Sellke, The Saxl conjecture for fourth powers via the semigroup property, J. Algebraic Combin. 45 (2017), 33–80. https://arxiv.org/abs/1511.02387v2
• C. Bessenrodt, Critical classes, Kronecker products of spin characters, and the Saxl conjecture, Algebr. Comb. 1 (2018), 353–369. https://doi.org/10.5802/alco.18
• X. Li, Saxl Conjecture for triple hooks, Discrete Math. 344 (2021), 112340. https://doi.org/10.1016/j.disc.2021.112340
• N. Harman and C. Ryba, A tensor-cube version of the Saxl conjecture, Algebr. Comb. 6 (2023), 507–511. https://doi.org/10.5802/alco.267
• E. Letellier, Tensor products of unipotent characters of general linear groups over finite fields, Transform. Groups 18 (2013), 233–262. https://doi.org/10.1007/s00031-013-9211-3
• OpenAI, A Cyclic Polytabloid Proof of Saxl's Conjecture, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Cyclic-Polytabloid-Proof-of-Saxls-Conjecture-September-24-2026/paper.pdf
• OpenAI, Universal Tensor Squares for Symmetric Groups, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Universal-Tensor-Squares-for-Symmetric-Groups-September-24-2026/main.pdf

Motivation

A thin spanning tree of a graph is a spanning tree that uses only a small fraction of the edges of every cut. Thin trees were introduced for the asymmetric traveling salesman problem: Asadpour, Goemans, Mądry, Oveis Gharan and Saberi showed that a thin tree of low cost can be augmented into a cheap tour, giving an $O(\log n/\log\log n)$-approximation (doi:10.1287/opre.2017.1603). Goddyn conjectured that high edge connectivity forces thin trees; the strong thin tree conjecture asks for thinness $C/k$ in every $k$-edge-connected multigraph. For applications one wants not just existence but an efficient algorithm that finds such a tree, also when parallel-edge multiplicities are huge and written in binary.

Background. The maximum-entropy rounding of Asadpour et al. constructs $O(\log n/(k\log\log n))$-thin trees. Oveis Gharan and Saberi constructed $O(1/k)$-thin trees on planar and bounded-genus graphs (2011, doi:10.1137/1.9781611973082.75). Anari and Oveis Gharan proved existence of $\mathrm{poly}(\log\log n)/k$-thin trees in general (2015, arXiv:1411.4613), without a polynomial-time construction. Klein and Olver (2023, doi:10.1109/FOCS57990.2023.00011) and Klein, Olver and Yeoh (2026, doi:10.4230/LIPIcs.ICALP.2026.129) handled laminar families and near-minimum cuts. A companion OpenAI preprint claims the existence statement of the strong conjecture.

The source of this mission, an OpenAI preprint dated September 23, 2026, claims a deterministic polynomial-time construction.

Setting

Graphs are finite undirected loopless multigraphs; parallel copies count separately. For $\varnothing\ne S\subsetneq V(G)$, $\delta_G(S)$ is the multiset of edges with exactly one endpoint in $S$, and $G$ is $k$-edge-connected if $|\delta_G(S)|\ge k$ for every such $S$. A spanning tree $T$ is $\alpha$-thin if $|\delta_T(S)|\le\alpha|\delta_G(S)|$ for all such $S$. Two input formats are allowed: an explicit list of labelled edge copies, or a list of endpoint pairs with multiplicities written in binary (so the number of edges can be exponential in the input length). Running time is measured in the total binary input length.

Formalization targets

Goal: Theorem 1.1 (algorithmic strong thin trees)

There is an absolute constant $C$ and a deterministic algorithm that, given $k\ge1$ and a $k$-edge-connected multigraph $G$ on at least one vertex (in either format), returns in time polynomial in the input length a spanning tree $T$ with

$$|\delta_T(S)|\le\frac Ck\,|\delta_G(S)|\qquad(\varnothing\ne S\subsetneq V(G)),$$

returning the empty tree for a one-vertex graph. Lean: OAI.AlgorithmicThinTrees.algorithmic_strong_thin_trees, open on the platform.

Significance

The theorem would give an algorithmic resolution of the strong thin tree conjecture: not only do $C/k$-thin trees exist, they can be found deterministically in polynomial time, even for exponentially many parallel edges. It also yields simultaneous cost-and-cut rounding (Corollary 7.1): from a fractional point whose mass on every cut is at least one, a tree in its support with every cut load and total cost within constant factors, with no metric assumption on costs. The order $1/k$ is optimal. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists.

Difficulty

Existence proofs for thin trees go through the Marcus–Spielman–Srivastava interlacing-families theorem and a fixed-point argument, neither of which is constructive: they show that some choice works without locating it. The algorithm must replace these by explicit, rational, polynomially sized computations (checked signings, rational positive semidefinite decompositions, bounded denominators) and must work with binary multiplicities, where even listing the edges is exponential. Certifying thinness on all exponentially many cuts must also be done without enumerating them.

Formalization scope

• Graphs: StrongThinTree.MultiGraph n m (vertices Fin n, edges Fin m, loopless). Inputs are ExplicitInput or BinaryInput (ordered, distinct endpoint pairs with multiplicities); a binary input's edge copies are Σ i, Fin (multiplicity i).
• Valid x: $n\ge1$, $k\ge1$ and EdgeConnected k.
• The machine model is CurrentKS.Machine: a deterministic machine with finitely many binary stacks and a finite instruction table, run for a fuel bound. Inputs and outputs are self-delimiting binary encodings (CurrentKS.encodeNat).
• AlgorithmicStrongThinTrees: ∃ C > 0, ∃ M a degree, 0 < a ∧ ∀ x, Valid x → after a * (len + 1)^degree steps M has halted and its output stack encodes a duplicate-free edge list forming a ThinTree C k; for $n=1$ the output is empty.
• One machine and one polynomial serve all inputs in both formats.

Needed infrastructure: the existence theory of the companion mission, a model of deterministic computation with polynomial-time bounds, exact rational linear algebra, and constructive spectral sparsification. Contributions formalizing Proposition 2.5, Proposition 3.1, Lemma 6.1, Theorem A.1 (rational rank-one signing) or Corollary 7.1 are welcome.

Selected references

• OpenAI, A polynomial-time construction of strong thin trees, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-polynomial-time-construction-of-strong-thin-trees-September-23-2026/paper.pdf
• OpenAI, The strong thin tree conjecture, preprint, September 23, 2026.
• A. Asadpour, M. X. Goemans, A. Mądry, S. Oveis Gharan, A. Saberi, An O(log n/log log n)-approximation algorithm for the asymmetric traveling salesman problem, Oper. Res., 2017. https://doi.org/10.1287/opre.2017.1603
• N. Anari, S. Oveis Gharan, Effective-resistance-reducing flows, spectrally thin trees, and asymmetric TSP, FOCS, 2015. https://arxiv.org/abs/1411.4613
• S. Oveis Gharan, A. Saberi, The asymmetric traveling salesman problem on graphs with bounded genus, SODA, 2011. https://doi.org/10.1137/1.9781611973082.75
• N. Klein, N. Olver, Thin trees for laminar families, FOCS, 2023. https://doi.org/10.1109/FOCS57990.2023.00011
• N. Klein, N. Olver, Z. S. Yeoh, Thin trees for near minimum cuts, ICALP, 2026. https://doi.org/10.4230/LIPIcs.ICALP.2026.129
• O. Svensson, J. Tarnawski, L. A. Végh, A constant-factor approximation algorithm for the asymmetric traveling salesman problem, J. ACM, 2020. https://doi.org/10.1145/3424306

Motivation: the Shareshian–Wachs elementary-positivity conjecture

The chromatic symmetric function of a graph, introduced by Stanley, records all proper colorings of the graph with infinitely many colors as a symmetric function; it refines the chromatic polynomial. Whether it expands with nonnegative coefficients in the basis of elementary symmetric functions ("$e$-positivity") is a central question in algebraic combinatorics. The Stanley–Stembridge conjecture (1993) predicted $e$-positivity for incomparability graphs of $(3+1)$-free posets; it arose from positivity questions for immanants of Jacobi–Trudi matrices. Shareshian and Wachs introduced a $q$-graded refinement, the chromatic quasisymmetric function, which tracks ascents of colorings along edges, and conjectured that for natural unit interval graphs its elementary coefficients are polynomials in $q$ with nonnegative integer coefficients. The $q$-refinement is tied to geometry: it describes the graded representation of the symmetric group on the cohomology of regular semisimple Hessenberg varieties.

Timeline

• 1993 — Stanley and Stembridge formulate the $e$-positivity conjecture for $(3+1)$-free posets (J. Combin. Theory Ser. A 1993); Haiman's immanant results imply Schur positivity (JAMS 1993).
• 1995 — Stanley introduces the chromatic symmetric function (Adv. Math. 1995).
• 1996 — Gasharov gives a positive Schur expansion via poset tableaux (Discrete Math. 1996).
• 2012/2016 — Shareshian and Wachs introduce the chromatic quasisymmetric function, prove its symmetry and Schur positivity for natural unit interval graphs, and conjecture elementary positivity over $\mathbb N[q]$ and the Hessenberg connection (Configuration Spaces 2012; Adv. Math. 2016).
• 2013 — Guay-Paquet reduces the Stanley–Stembridge conjecture to unit interval orders (arXiv:1306.2400).
• 2015 — Athanasiadis gives a power-sum expansion (Electron. J. Combin. 2015).
• 2016–2018 — Brosnan–Chow (Adv. Math. 2018) and Guay-Paquet (arXiv:1601.05498) prove the Hessenberg representation identity.
• 2019–2023 — Positivity for substantial subfamilies: abelian Hessenberg varieties (Harada–Precup 2019), explicit expansions (Cho–Huh 2019), melting lollipops (Huh–Nam–Yoo 2020), abelian Dyck paths via $q$-rook theory (Colmenarejo–Morales–Panova 2023); the modular law of Abreu and Nigro (J. Combin. Theory Ser. A 2021).
• 2024–2025 — Hikita proves the Stanley–Stembridge conjecture ($q=1$) via a probabilistic formula (arXiv:2410.12758); his weights do not give coefficientwise positivity in $\mathbb N[q]$. Griffin, Mellit, Romero, Weigl and Wen give an independent proof (arXiv:2504.06936).
• 2026 — The OpenAI preprint Elementary positivity of chromatic quasisymmetric functions (OpenAI Math Release, September 24, 2026) claims elementary positivity over $\mathbb N[q]$ for all natural unit interval graphs, with an explicit permutation witness. It has not been peer reviewed and its theorem is not formally verified.

Setting

Let $h:[n]\to[n]$ be weakly increasing with $i\le h(i)$. The natural unit interval graph $G=G(h)$ has vertices $[n]=\{1,\dots,n\}$ and edges $\{i,j\}$ with $i<j\le h(i)$. A proper coloring $f:[n]\to\mathbb N_{>0}$ gives different colors to adjacent vertices, and $\operatorname{asc}_G(f)$ counts edges $\{a<b\}$ with $f(a)<f(b)$. The chromatic quasisymmetric function is

$$\chi_G(X;q)=\sum_{f\ \text{proper}} q^{\operatorname{asc}_G(f)}\prod_{a=1}^n x_{f(a)} .$$

For a partition $\lambda$, $e_\lambda=\prod_i e_{\lambda_i}$ with $e_k=\sum_{i_1<\dots<i_k}x_{i_1}\cdots x_{i_k}$. Let $D^0_G$ be the set of permutations $\sigma$ (as words $\sigma_1\cdots\sigma_n$) such that every adjacent descent $\sigma_i>\sigma_{i+1}$ is an edge, and $\operatorname{ginv}_G(\sigma)$ the number of inversions $i<j$, $\sigma_i>\sigma_j$, with $\{\sigma_i,\sigma_j\}$ an edge.

In Lean (namespace OAI.ElementaryPositivity), NaturalUnitIntervalGraph n stores a monotone extensive h : Fin n → Fin n; chromatic r is $\chi_G$ in $r$ variables as an MvPolynomial (Fin r) (Polynomial ℕ); Nondescent and graphInversions define $D^0_G$ and $\operatorname{ginv}_G$; a PermutationWitness is a map $\theta:D^0_G\to\{\lambda\vdash n\}$ together with the identity below in every number $r$ of variables, using Mathlib's MvPolynomial.esymmPart.

Formalization targets

Goal: elementary positivity with a permutation witness (Theorem 1.1)

For every $n$ and every natural unit interval graph $G$ on $[n]$ there is a map $\theta_G:D^0_G\to\{\lambda\vdash n\}$ with

$$\chi_G(X;q)=\sum_{\sigma\in D^0_G} q^{\operatorname{ginv}_G(\sigma)}\,e_{\theta_G(\sigma)}(X).$$

In particular every elementary coefficient of $\chi_G$ lies in $\mathbb N[q]$. The goal is published on the platform with status Open.

Significance

The result itself. The theorem resolves the elementary-positivity part of the Shareshian–Wachs conjecture, and at $q=1$, via Guay-Paquet's reduction, recovers the Stanley–Stembridge conjecture first proved by Hikita. It is stronger than positivity: it gives a combinatorial witness, assigning each permutation of $D^0_G$ an elementary partition while preserving its graph-inversion weight. Through the Brosnan–Chow/Guay-Paquet identity, it implies that each graded piece of the cohomology of a regular semisimple Hessenberg variety is a direct sum of Young permutation modules with multiplicities counted by the witness (Corollary 1.2). Elementary unimodality, the other part of the Shareshian–Wachs conjecture, is not addressed.

Formalizing it. The statement is a finite polynomial identity for each $n$, $G$ and $r$, fully expressible with Mathlib's multivariate polynomials and elementary symmetric polynomials. A machine-checked proof would certify a long bijective argument (walls, triangle moves, witness completion) with many case distinctions.

Difficulty

The coloring definition already has nonnegative coefficients in the monomial basis, but rewriting in the elementary basis involves subtraction, so positivity is not visible from the definition. Earlier positive formulas (Schur expansions, power-sum expansions, the acyclic-orientation formula) group partitions or work at $q=1$, and Hikita's probabilistic formula has rational $q$-weights that are only positive at real $q>0$, not coefficientwise. A proof over $\mathbb N[q]$ must produce, for each elementary partition and each power of $q$, a nonnegative integer count, uniformly over all graphs.

Formalization scope

• Graphs are encoded by h : Fin n → Fin n monotone with i ≤ h i (zero-indexed); edges are $i<j\le h(i)$ in either order.
• Colorings use $r$ colors Fin r and the identity is required for every $r\in\mathbb N$, which is equivalent to the identity of symmetric functions since both sides are homogeneous of degree $n$.
• Coefficients live in Polynomial ℕ, so nonnegativity in $\mathbb N[q]$ is built into the statement; the witness theta is an arbitrary function on the finite set $D^0_G$. The source's additional assertion that $\theta_G$ is produced by a deterministic terminating procedure is not encoded, but any such function on a finite set is computable by search, so nothing of mathematical substance is lost.
• Needed infrastructure: symmetric functions in finitely many variables, elementary basis manipulations, and bijections on ordered independent-set collections. These are reusable for other chromatic-function and LLT-positivity problems.

Selected references

• R. P. Stanley and J. R. Stembridge, On immanants of Jacobi–Trudi matrices and permutations with restricted position, J. Combin. Theory Ser. A 62 (1993). https://doi.org/10.1016/0097-3165(93)90048-D
• R. P. Stanley, A symmetric function generalization of the chromatic polynomial of a graph, Adv. Math. 111 (1995), 166–194. https://doi.org/10.1006/aima.1995.1020
• J. Shareshian and M. L. Wachs, Chromatic quasisymmetric functions, Adv. Math. 295 (2016). https://doi.org/10.1016/j.aim.2015.12.018
• M. Guay-Paquet, A modular law for the chromatic symmetric functions of (3+1)-free posets, arXiv:1306.2400 (2013). https://arxiv.org/abs/1306.2400v1
• P. Brosnan and T. Y. Chow, Unit interval orders and the dot action on the cohomology of regular semisimple Hessenberg varieties, Adv. Math. 329 (2018), 955–1001. https://doi.org/10.1016/j.aim.2018.02.020
• A. Abreu and A. Nigro, Chromatic symmetric functions from the modular law, J. Combin. Theory Ser. A 180 (2021). https://doi.org/10.1016/j.jcta.2021.105407
• T. Hikita, A proof of the Stanley–Stembridge conjecture, arXiv:2410.12758 (2024, revised 2025). https://arxiv.org/abs/2410.12758v2
• S. T. Griffin, A. Mellit, M. Romero, K. Weigl and J. J. Wen, On Macdonald expansions of q-chromatic symmetric functions and the Stanley–Stembridge conjecture, arXiv:2504.06936 (2025). https://arxiv.org/abs/2504.06936v1
• OpenAI, Elementary positivity of chromatic quasisymmetric functions, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 2; Corollary 1.2, p. 4). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Elementary-Positivity-of-Chromatic-Quasisymmetric-Functions-September-24-2026/paper.pdf