Prove2Me
← Collections

OAI Math

All of openAI's results.

https://github.com/openai/math

317 missions

Missions

121–140 of 317
Completed
AnalysisMathematical PhysicsProbability·Captain: wurtle

A continuum temperature singularity for a radial pair potentialResearch Paper

Motivation: phase transitions for continuum particles

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

Timeline

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

Setting

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

  1. ϕ(r)→+∞\phi(r)\to+\infty as r↓0r\downarrow0;
  2. ϕ≤−a<0\phi\le-a<0 on some interval [r1,r2][r_1,r_2] with 0<r1<r20<r_1<r_2;
  3. ∫R∞r2∣ϕ(r)∣ dr<∞\int_R^\infty r^2|\phi(r)|\,dr<\infty for some RR;
  4. (stability) UN(x1,…,xN)=∑i<jΦ(xi−xj)≥−BNU_N(x_1,\dots,x_N)=\sum_{i<j}\Phi(x_i-x_j)\ge -BN for all NN and all configurations.

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

ZΛL,N(β)=1N!∫ΛLNe−βUN dx,ZΛL,0=1,e−β⋅∞=0,Z_{\Lambda_L,N}(\beta)=\frac1{N!}\int_{\Lambda_L^N}e^{-\beta U_N}\,dx,\qquad Z_{\Lambda_L,0}=1,\quad e^{-\beta\cdot\infty}=0,

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

f(β,ρ)=−1βlim⁡L→∞L−3log⁡ZΛL,⌊ρL3⌋(β).f(\beta,\rho)=-\frac1\beta\lim_{L\to\infty}L^{-3}\log Z_{\Lambda_L,\lfloor\rho L^3\rfloor}(\beta).

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

Formalization targets

Goal: a strict temperature corner throughout a density interval

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

Dβ−f(βc,ρ)  >  Dβ+f(βc,ρ).D^-_\beta f(\beta_c,\rho)\;>\;D^+_\beta f(\beta_c,\rho).

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

5 thms2 active usersReviewed
Completed
AnalysisMathematical PhysicsProbability·Captain: wurtle

A radial continuum phase transition with algebraic decayResearch Paper

Motivation: continuum phase transitions with a power-law tail

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

Timeline

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

Setting

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

Uϕ(x1,…,xN)=∑i<jϕ(∣xi−xj∣),ZL,N(β)=1N!∫ΛLNe−βUϕ dx,ZL,0=1.U^\phi(x_1,\dots,x_N)=\sum_{i<j}\phi(|x_i-x_j|),\qquad Z_{L,N}(\beta)=\frac1{N!}\int_{\Lambda_L^N}e^{-\beta U^\phi}\,dx,\qquad Z_{L,0}=1 .

The potential is stable if Uϕ≥−BNU^\phi\ge -BN for all configurations. The canonical free energy at density ρ\rho is

f(β,ρ)=−lim⁡L→∞1βL3log⁡ZL,⌊ρL3⌋(β).f(\beta,\rho)=-\lim_{L\to\infty}\frac1{\beta L^3}\log Z_{L,\lfloor\rho L^3\rfloor}(\beta).

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

Formalization targets

Milestone: the corner at the central density

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

f−′(βc,5p/3)>f+′(βc,5p/3).f'_-(\beta_c,5p/3)>f'_+(\beta_c,5p/3).

Goal: a common corner on a density interval

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

∑i<jϕ(∣xi−xj∣)≥−BN,∣ϕ(r)∣≤C r−3−1/32 (r≥1),\sum_{i<j}\phi(|x_i-x_j|)\ge -BN,\qquad |\phi(r)|\le C\,r^{-3-1/32}\ (r\ge1),

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

f−′(βc,ρ)>f+′(βc,ρ).f'_-(\beta_c,\rho)>f'_+(\beta_c,\rho).

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

14 thms2 active usersReviewed
Dynamical SystemsGraph TheoryProbability·Captain: wurtle

The free uniform spanning forest is a factor of IIDResearch Paper

Motivation

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

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

Timeline

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

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

Setting

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

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

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

Formalization targets

Milestones (strongly Rayleigh processes, Section 6)

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

Goal: Theorem 1.1

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

9 thms2 active usersReviewed
Completed
CombinatoricsProbabilityTheoretical Computer Science·Captain: wurtle

A Limiting Satisfiability Threshold for Every Fixed Clause SizeResearch Paper

Motivation

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

Timeline

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

Setting

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

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

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

Formalization targets

Goal: Theorem 1.1

For every fixed integer k≥3k\ge3 there is αk∈(0,∞)\alpha_k\in(0,\infty) such that

lim⁡n→∞Pn(⌊cn⌋)={1,0≤c<αk,0,c>αk.\lim_{n\to\infty}P_n(\lfloor cn\rfloor)=\begin{cases}1,&0\le c<\alpha_k,\\ 0,&c>\alpha_k.\end{cases}

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

20 thms2 active usersReviewed
Completed
CombinatoricsProbabilityTheoretical Computer Science·Captain: wurtle

Variance of the Random k-SAT Hitting TimeResearch Paper

Motivation

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

Timeline

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

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

Setting

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

Fm=C1∧⋯∧Cm,F0=true,Hn=min⁡{m≥1: Fm unsatisfiable},F_m=C_1\wedge\dots\wedge C_m,\qquad F_0=\text{true},\qquad H_n=\min\{m\ge1:\ F_m\ \text{unsatisfiable}\},

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

ℓk(n)={log⁡(en),k=3,1,k≥4,Uk=log⁡2−log⁡(1−2−k).\ell_k(n)=\begin{cases}\log(en),&k=3,\\1,&k\ge4,\end{cases}\qquad U_k=\frac{\log2}{-\log(1-2^{-k})}.

Formalization targets

Goal: Theorem 1.1

There are constants Ck,ck>0C_k,c_k>0 with

Var⁡(Hn)≤Ck n ℓk(n)(n≥k),Var⁡(Hn)≥ckn(n large),\operatorname{Var}(H_n)\le C_k\,n\,\ell_k(n)\quad(n\ge k),\qquad \operatorname{Var}(H_n)\ge c_kn\quad(n\ \text{large}),

and for every fixed B>0B>0 a constant Ck,BC_{k,B} with Var⁡(Tn,B)≤Ck,B n ℓk(n)\operatorname{Var}(T_{n,B})\le C_{k,B}\,n\,\ell_k(n); if B>UkB>U_k then also Var⁡(Tn,B)≥ckn\operatorname{Var}(T_{n,B})\ge c_kn for large nn. Hence Var⁡(Hn)=Θk(n)\operatorname{Var}(H_n)=\Theta_k(n) for k≥4k\ge4. Lean: OAI.RandomKSAT.variance_main, open on the platform.

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

32 thms2 active usersReviewed
CombinatoricsMathematical LogicProbability·Captain: wurtle

Computing the Random 3-SAT ThresholdResearch Paper

Motivation

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

Timeline

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

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

Setting

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

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

A real α\alpha is computable if a single algorithm, on input rr, halts with a rational qrq_r satisfying ∣qr−α∣≤2−r|q_r-\alpha|\le2^{-r}.

Formalization targets

Goal: Theorem 1.1

There is α3∈(0,∞)\alpha_3\in(0,\infty) such that for every fixed real a≥0a\ge0

lim⁡n→∞p(n,⌊an⌋)={1,a<α3,0,a>α3,\lim_{n\to\infty}p(n,\lfloor an\rfloor)=\begin{cases}1,&a<\alpha_3,\\0,&a>\alpha_3,\end{cases}

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

2 thms1 active userReviewed
Dynamical SystemsMathematical PhysicsProbability·Captain: wurtle

The sharp factor-of-IID threshold for the free Ising model on regular treesResearch Paper

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 dd-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⁡β≤(d−1)−1/2\tanh\beta\le(d-1)^{-1/2} after proving it for large dd 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β≤1(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⁡β≤1/(d−1)\tanh\beta\le 1/(d-1) (CPC 2017).
  • 2022 — Nam, Sly and Zhang construct the free state as a factor for d≥d0d\ge d_0 and tanh⁡β≤c/d−1\tanh\beta\le c/\sqrt{d-1}, via posterior-drift stochastic differential equations, and conjecture the sharp threshold (CMP 2022).

Setting

Let TdT_d be the infinite dd-regular tree with vertex set VV; concretely, VV is the set of finite words over {1,…,d}\{1,\dots,d\} with no two equal consecutive letters, and ww is adjacent to wcwc. Put θ=tanh⁡β\theta=\tanh\beta for β≥0\beta\ge0. The free zero-field Ising law μd,β\mu_{d,\beta} on {−1,+1}V\{-1,+1\}^V is determined by its marginals on finite connected subtrees DD:

μd,β(σ∣D=η)=12∏{u,v}∈E(D)1+θ ηuηv2.\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+θ)/2(1+\theta)/2. A spin law is a factor of IID if it is the law of Φ(U)\Phi(U) for i.i.d. uniform labels U=(Uv)v∈VU=(U_v)_{v\in V} and a measurable Φ:[0,1]V→{−1,1}V\Phi:[0,1]^V\to\{-1,1\}^V such that, for each fixed automorphism gg, Φ(gU)=gΦ(U)\Phi(gU)=g\Phi(U) almost surely, where (gx)v=xg−1v(gx)_v=x_{g^{-1}v}.

Formalization targets

Goal: Theorem 1.1 (p. 1)

For every integer d≥3d\ge3 and every β≥0\beta\ge0,

μd,β is a factor of IID  ⟺  tanh⁡β≤1d−1.\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≥3d\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⁡β>(d−1)−1/2\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 θ≤1/(d−1)\theta\le1/(d-1). The Nam–Sly–Zhang approach observes Xv(t)=tσv+Bv(t)X_v(t)=t\sigma_v+B_v(t) and expresses the posterior through innovations WvW_v, which are independent Brownian motions; but being Brownian does not make XX a function of WW, and that is the central step (pp. 2–3). At criticality θ=(d−1)−1/2\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][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 β≥0\beta\ge0 and d≥3d\ge3; at β=0\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

2 thms1 active userReviewed
CombinatoricsMathematical PhysicsProbability·Captain: wurtle

Critical strip-crossing mass on the honeycomb latticeResearch Paper

Motivation

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

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

Background

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

Setting

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

KN(k)=∑arches to kρ∣γ∣,AN=∑k≠0KN(k),BN=∑bridgesρ∣γ∣,mN=∑k≥1k KN(k).K_N(k)=\sum_{\text{arches to }k}\rho^{|\gamma|},\quad A_N=\sum_{k\ne0}K_N(k),\quad B_N=\sum_{\text{bridges}}\rho^{|\gamma|},\quad m_N=\sum_{k\ge1}k\,K_N(k).

Write fN≍gNf_N\asymp g_N if ℓgN≤fN≤ugN\ell g_N\le f_N\le u g_N for all N≥1N\ge1 with fixed constants ℓ,u>0\ell,u>0.

Formalization targets

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

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

cAN+BN=1,mN+1−mN≍BN,mN≍N3/4,BN≍N−1/4,cA_N+B_N=1,\qquad m_{N+1}-m_N\asymp B_N,\qquad m_N\asymp N^{3/4},\qquad B_N\asymp N^{-1/4},

and BNB_N is nonincreasing in NN.

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

2 thms1 active userReviewed
Completed
Group TheoryProbabilityRepresentation Theory·Captain: wurtle

From partial permutation information to Fourier boundsResearch Paper

Motivation: when do partial observations of a permutation force full randomness?

Many random permutations are analysed through what they do to a few labels at a time: the joint positions of kk chosen cards in a shuffle, or the images of a list of inputs under a block cipher built from a shuffle. Such partial information does not by itself control the whole permutation. The uniform law on the alternating group already has uniform images on every set of at most n−2n-2 labels, yet it is at total-variation distance 1/21/2 from uniform on SnS_n. Converting partial-permutation estimates into full-permutation estimates therefore needs an additional argument, and this is the bottleneck in recent work on the Thorp shuffle, where fixed fractions of the deck were known to randomize quickly (Czumaj–Vöcking 2014; Czumaj 2015) long before the full deck was.

Timeline

  • 1954 — Frame, Robinson and Thrall prove the hook-length formula for the degrees of irreducible representations of SnS_n (Canad. J. Math. 1954).
  • 1981 — Diaconis and Shahshahani analyse random transpositions by Fourier analysis on SnS_n, establishing the upper-bound-lemma framework (Z. Wahrsch. 1981).
  • 2004 — Liebeck and Shalev show that the Witten zeta sums ∑λ⊢n(fλ)−u\sum_{\lambda\vdash n}(f^\lambda)^{-u} tend to 22 for every fixed u>0u>0 (J. Algebra 2004).
  • 2009, 2013 — Morris uses entropy and trajectory comparison to prove O((log⁡n)4)O((\log n)^4) and O((log⁡n)3)O((\log n)^3) mixing bounds for the Thorp shuffle (Ann. Probab. 2009; CPC 2013).
  • 2014–2015 — Czumaj and Vöcking show that a fixed fraction of the cards randomizes in O((log⁡n)2)O((\log n)^2) layers; Czumaj obtains full-permutation sampling by recursively applying partial randomizers on shrinking sets.
  • 2026 — The OpenAI preprint From partial permutation information to Fourier bounds (OpenAI Math Release, September 26, 2026) proves that coset caps for complementary blocks control every Fourier matrix (Theorem 1.1). It has not been peer reviewed.

Setting

Let XX be a finite set of nn labels and G=Sym(X)G=\mathrm{Sym}(X), acting as maps from initial labels to final positions. For M⊆XM\subseteq X, let HM≤GH_M\le G be the block subgroup of permutations that fix every label outside MM. Two permutations have the same images on X∖MX\setminus M exactly when they lie in the same left coset gHMgH_M, so a bound on the law of those images is a bound on coset masses.

For a nonnegative weight ff on GG and a unitary representation ρ\rho of GG on a finite-dimensional complex inner-product space VV, the Fourier transform is f^(ρ)=∑g∈Gf(g)ρ(g)\widehat f(\rho)=\sum_{g\in G}f(g)\rho(g), with D=dim⁡VD=\dim V. The Hilbert–Schmidt norm is unnormalized, ∥A∥HS2=tr⁡(A∗A)\|A\|_{\mathrm{HS}}^2=\operatorname{tr}(A^*A). For u>0u>0 the symmetric degree constant is

Cu=sup⁡m≥1 ∑λ⊢mDλ−u,C_u=\sup_{m\ge1}\ \sum_{\lambda\vdash m} D_\lambda^{-u},

where DλD_\lambda ranges over the degrees of the irreducible complex representations of SmS_m.

Formalization targets

Goal: complementary cosets control Fourier matrices (Theorem 1.1)

Partition XX into b≥1b\ge1 nonempty blocks M1,…,MbM_1,\dots,M_b and put Hi=HMiH_i=H_{M_i}. Let f≥0f\ge0 on GG have total mass at most one and satisfy

f(gHi)≤B[G:Hi](g∈G, 1≤i≤b).f(gH_i)\le \frac{B}{[G:H_i]}\qquad(g\in G,\ 1\le i\le b).

Then for every u>0u>0 and every irreducible unitary ρ\rho of degree DD,

∥f^(ρ)∥HS2≤b B Cu D−1+(u+2)/band∥f^(ρ)∥op2≤b B Cu D−1+(u+2)/b.\|\widehat f(\rho)\|_{\mathrm{HS}}^2\le b\,B\,C_u\,D^{-1+(u+2)/b} \qquad\text{and}\qquad \|\widehat f(\rho)\|_{\mathrm{op}}^2\le b\,B\,C_u\,D^{-1+(u+2)/b}.

No restriction is placed on the block sizes or on multiplicities in the restriction of ρ\rho to H1×⋯×HbH_1\times\dots\times H_b. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. Theorem 1.1 is a quantitative transfer principle: a single law whose complementary partial images are never much heavier than uniform has a power saving in every irreducible representation of SnS_n. With b=8b=8 and u=1u=1 it gives ∥f^(ρ)∥HS2≤8C1D−5/8\|\widehat f(\rho)\|_{\mathrm{HS}}^2\le 8C_1D^{-5/8}, which is enough for the principal application in the source (Corollary 3.6, p. 9): if the images of a uniformly chosen set of 7n/87n/8 labels are close to uniform in average total variation and the sign mean tends to zero, then the product of just two independent copies of the permutation converges to uniform. This is the step used by the companion Thorp-shuffle preprints to turn fixed-list estimates into full-deck mixing in O(log⁡n)O(\log n) shuffles. The statement concerns arbitrary laws on SnS_n and does not depend on any shuffle.

Formalizing it. The theorem is a finite inequality with explicit constants, so it is a natural target for machine checking. A proof would certify the partial-to-full transfer used by the Thorp mixing arguments, and would require reusable infrastructure: isotypic decompositions of restrictions to products of subgroups, Schur averaging, Hilbert–Schmidt and operator norms of group-algebra elements, and uniform bounds on symmetric-group Witten zeta sums. None of this is formalized yet.

Difficulty

The natural approach decomposes ρ\rho restricted to H1×⋯×HbH_1\times\dots\times H_b into tensor products of irreducibles of the blocks and bounds f^(ρ)\widehat f(\rho) on each piece. This fails when a block type occurs with large multiplicity: a dimension count that pays for every copy gives no decay in DD. The bound must count each irreducible type of a block subgroup once, regardless of multiplicity, and must hold uniformly over all block sizes, which is why the constant CuC_u is a supremum over every symmetric group. The Hilbert–Schmidt bound is harder than the operator bound, because it must control the whole Fourier matrix rather than its action on one vector.

Formalization scope

  • XX is an arbitrary Fintype with decidable equality; blocks are M : Fin b → Set X, nonempty, pairwise disjoint and covering. The block subgroup is blockSubgroup (M i), the permutations fixing each point outside M i.
  • The coset cap is LeftCosetCap f H B: for every gg, ∑h∈Hf(gh)≤B/[G:H]\sum_{h\in H}f(gh)\le B/[G:H], with the index H.index.
  • ρ\rho is any irreducible representation on a finite-dimensional complex inner-product space with ⟨ρ(g)x,ρ(g)y⟩=⟨x,y⟩\langle\rho(g)x,\rho(g)y\rangle=\langle x,y\rangle; the Fourier transform is complexFourier ρ f; hsNormSq is Re⁡tr⁡(A∗A)\operatorname{Re}\operatorname{tr}(A^*A); the operator norm is that of the associated continuous linear map; DD is Module.finrank ℂ V and the exponent is a real power.
  • Irreducible representations of SmS_m are indexed by the isotypic components of the regular representation of Equiv.Perm (Fin m), and CuC_u is symmetricDegreeConstant u, an sSup over m≥1m\ge1. The supremum is finite for every u>0u>0; a solver must prove this boundedness, since sSup of an unbounded real set would be 00.
  • Needed infrastructure: isotypic decomposition and Schur's lemma for finite groups, degree bounds for SmS_m (hook-length or tableau counting), and uniform Witten zeta bounds. The degree layer is reusable for any random walk on SnS_n.

Selected references

46 thms2 active usersReviewed
Completed
Markov ChainProbabilityRepresentation Theory·Captain: wurtle

Random-subspace tests and trace smoothing for coordinate sweepsResearch Paper

Motivation: optimal-order mixing for the Thorp shuffle

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

Timeline

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

Setting

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

(x1,x2,…,xd)⟼(x2,…,xd,  x1+ξx2,…,xd)(x_1,x_2,\dots,x_d)\longmapsto(x_2,\dots,x_d,\;x_1+\xi_{x_2,\dots,x_d})

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

For a partition λ⊢n\lambda\vdash n let VλV_\lambda be the Specht module (the irreducible representation of SnS_n indexed by λ\lambda), of dimension DλD_\lambda, and let Qn(λ)=∑gμd(g) λ(g)Q_n(\lambda)=\sum_g \mu_d(g)\,\lambda(g) be the average of the sweep in VλV_\lambda. For an operator YY, ∣Y∣=(Y∗Y)1/2|Y|=(Y^*Y)^{1/2} and traces are unnormalized. The regular trace of the PP-th power is

Tr⁡reg∣Qn∣P=∑λ⊢nDλTr⁡Vλ∣Qn(λ)∣P,\operatorname{Tr}_{\rm reg}|Q_n|^P=\sum_{\lambda\vdash n}D_\lambda\operatorname{Tr}_{V_\lambda}|Q_n(\lambda)|^P ,

in which the trivial representation contributes exactly 11. Total variation is ∥μ−ν∥TV=12∑g∣μ(g)−ν(g)∣\|\mu-\nu\|_{\rm TV}=\tfrac12\sum_g|\mu(g)-\nu(g)|.

Formalization targets

Goal: regular-trace smoothing (Theorem 1.1)

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

Tr⁡reg∣Qn∣P≤1+n−10,\operatorname{Tr}_{\rm reg}|Q_n|^P\le 1+n^{-10},

and for every integer vv with 2v≥P2v\ge P and every initial deck σ\sigma,

12∑g∈Sn∣μvd(gσ−1)−1n!∣≤12 n−5.\tfrac12\sum_{g\in S_n}\Bigl|\mu_{vd}(g\sigma^{-1})-\tfrac1{n!}\Bigr|\le\tfrac12\,n^{-5}.

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

5 thms2 active usersReviewed
Markov ChainProbabilityRepresentation Theory·Captain: wurtle

Conditional coordinate sweeps and analytic transferResearch Paper

Motivation: a dimension saving for the binary coordinate sweep

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

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

Timeline

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

Setting

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

Kλ=Eg∼BNρλ(g).K_\lambda=\mathbb E_{g\sim B_N}\rho_\lambda(g).

Write BN∗wB_N^{*w} for the law of ww independent sweeps and ∥μ−ν∥TV=12∑g∣μ(g)−ν(g)∣\|\mu-\nu\|_{\rm TV}=\tfrac12\sum_g|\mu(g)-\nu(g)|.

For the conditional estimate, an ordered product grid is Ω=Ω1×⋯×Ωb\Omega=\Omega_1\times\dots\times\Omega_b with each ∣Ωj∣=mj|\Omega_j|=m_j a power of two in [R,R2][R,R^2]; a sweep permutes the lines parallel to coordinate 11, then coordinate 22, and so on, each line independently with law Lm(z)=(1−z)Um+zBmL_m(z)=(1-z)U_m+zB_m. A family H\mathcal H of hh prescribed trajectories (disjoint at every layer) is conditioned on; the remaining random bijection of the s−hs-h free slots has average KλHK^{\mathcal H}_\lambda in each irreducible λ⊢s−h\lambda\vdash s-h, with line cost C(H)=∑Llog⁡(∣L∣hL/(∣L∣)hL)C(\mathcal H)=\sum_{L}\log\bigl(|L|^{h_L}/(|L|)_{h_L}\bigr).

Formalization targets

Milestone: conditional sweep moment estimate (Theorem 3.1)

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

log⁡∥KλH∥2q2q≤−c(s)log⁡Dλ+e(s) hlog⁡s−C(H),\log\|K^{\mathcal H}_\lambda\|_{2q}^{2q}\le -c(s)\log D_\lambda+e(s)\,h\log s-C(\mathcal H),

with c(s)=c0+1/log⁡sc(s)=c_0+1/\sqrt{\log s}, e(s)=e0−1/log⁡se(s)=e_0-1/\sqrt{\log s}, c0=e0=10−4c_0=e_0=10^{-4}, and log⁡0=−∞\log 0=-\infty.

Goal: binary sweep contraction (Theorem 1.1)

There are absolute constants g>0g>0 and d0d_0 such that for all d≥d0d\ge d_0 and every irreducible unitary representation of S2dS_{2^d} of dimension DD,

∥Kλ∥op≤D−g;\|K_\lambda\|_{\rm op}\le D^{-g};

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

sup⁡τ∈SN∥BN∗w(⋅ τ−1)−UN∥TV→d→∞0.\sup_{\tau\in S_N}\bigl\|B_N^{*w}(\cdot\,\tau^{-1})-U_N\bigr\|_{\rm TV}\xrightarrow[d\to\infty]{}0 .

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

5 thms1 active userReviewed
Completed
Mathematical LogicModel Theory·Captain: wurtle

A CH obstruction to a prescribed categoricity thresholdResearch Paper

Motivation: categoricity transfer beyond first-order logic

A class of structures is categorical in a cardinal λ\lambda if it has exactly one model of size λ\lambda up to isomorphism. Morley's theorem (1965) says that a complete first-order theory in a countable language categorical in one uncountable cardinal is categorical in all of them. Abstract elementary classes (AECs), introduced by Shelah in the 1970s, axiomatize classes of structures with a well-behaved notion of strong substructure (closure under isomorphism, coherence, unions of chains, a Löwenheim–Skolem number) without requiring first-order axiomatizability; they cover classes defined in infinitary logics and many classes of modules. Shelah's categoricity conjecture for AECs, in its eventual form, asks whether categoricity in one sufficiently large cardinal transfers to all sufficiently large cardinals. A sharper, prescribed-threshold form names the threshold explicitly: with H(K)=ℶ(2LS(K))+H(K)=\beth_{(2^{\mathrm{LS}(K)})^+} (the Hanf number for existence of arbitrarily large models), categoricity in some λ≥H(K)\lambda\ge H(K) should imply categoricity in every μ≥H(K)\mu\ge H(K). Deciding which form holds is a central question in non-elementary model theory.

Timeline

  • 1965 — Morley proves the categoricity theorem for countable first-order theories (Trans. AMS 1965).
  • 1970s — Shelah introduces abstract elementary classes (see the survey of Boney–Vasey 2017, §2).
  • 1990 — Hart and Shelah show categoricity in Lω1,ωL_{\omega_1,\omega} can stop at ℵk\aleph_k while holding for ℵ0,…,ℵk−1\aleph_0,\dots,\aleph_{k-1}, using finite-support group constructions (Israel J. Math. 1990).
  • 1999 — Shelah proves categoricity transfer for AECs with amalgamation and records H(K)H(K) as the existence bound (APAL 1999).
  • 2016 — Kolesnikov and Lambie-Hanson study Hanf numbers for amalgamation of coloring classes (JSL 2016).
  • 2017 — Vasey proves downward transfer from a successor cardinal ≥H(K)\ge H(K) under amalgamation and tameness (APAL 2017).
  • 2021 — Grossberg distinguishes the prescribed-bound and eventual forms of the conjecture (A Course in Model Theory I, draft, Ch. 2 §4).
  • 2022–2023 — Espíndola announces a proof of eventual categoricity and, for arbitrary AECs, a transfer at the prescribed bound via accessible categories (arXiv:1906.09169, arXiv:2301.13167).
  • 2024 — Šaroch and Trlifaj state the prescribed-threshold formulation with both endpoints included (Bull. LMS 2024, §2.3).
  • 2026 — An OpenAI preprint, A CH obstruction to a prescribed categoricity threshold (OpenAI Math Release, September 24, 2026), claims that under CH there is an AEC with LS(K)=ℵ0\mathrm{LS}(K)=\aleph_0, categorical on a tail but with two nonisomorphic models at H(K)=ℶω2H(K)=\beth_{\omega_2}; this conflicts with the transfer claimed in Espíndola 2023 (Theorem 4.1). The preprint has not been peer reviewed and its theorem is not formally verified.

Setting

Work with relational structures in a finitary relational language LL (a set of relation symbols, each with a finite arity). An abstract elementary class is a class KK of LL-structures with a relation M⪯KNM\preceq_K N ("strong substructure") such that: ⪯K\preceq_K is a partial order on KK refining substructure; KK and ⪯K\preceq_K are closed under isomorphism; coherence holds (M0⊆M1M_0\subseteq M_1, M0⪯KM2M_0\preceq_K M_2, M1⪯KM2M_1\preceq_K M_2 imply M0⪯KM1M_0\preceq_K M_1); unions of ⪯K\preceq_K-chains are in KK, are ⪯K\preceq_K-extensions of each member, and are ⪯K\preceq_K-below any common strong extension (Tarski–Vaught chain axioms); and there is a Löwenheim–Skolem number LS(K)≥ℵ0+∣L∣\mathrm{LS}(K)\ge\aleph_0+|L|, the least θ\theta such that every subset AA of a model MM lies in some N⪯KMN\preceq_K M with ∣N∣≤∣A∣+θ|N|\le|A|+\theta.

KK is categorical in μ\mu if it has a model of size μ\mu and any two models of size μ\mu are isomorphic. The beth numbers are ℶ0=ℵ0\beth_0=\aleph_0, ℶα+1=2ℶα\beth_{\alpha+1}=2^{\beth_\alpha} and suprema at limits. CH is 2ℵ0=ℵ12^{\aleph_0}=\aleph_1.

Formalization targets

Goal: the CH counterexample (Theorem 1.1)

Assume CH. There is a countable finitary relational language LL and an AEC KK in LL such that

LS(K)=ℵ0,ℶω2=H(K)=ℶ(2ℵ0)+,\mathrm{LS}(K)=\aleph_0,\qquad \beth_{\omega_2}=H(K)=\beth_{(2^{\aleph_0})^+},

KK has two nonisomorphic models of cardinality ℶω2\beth_{\omega_2}, and, with Λ=ℶ(2ℵ1)+\Lambda=\beth_{(2^{\aleph_1})^+},

K is categorical in every cardinal μ≥Λ.K\ \text{is categorical in every cardinal } \mu\ge\Lambda .

Hence Λ+>H(K)\Lambda^+>H(K) is a categoricity cardinal from which downward transfer to H(K)H(K) fails, while eventual categoricity holds for this KK. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. Combined with Gödel's relative consistency of CH, the theorem shows that, if ZFC is consistent, the prescribed-threshold form of Shelah's categoricity conjecture is not provable in ZFC (Corollary 6.1 of the source). The example has no amalgamation or joint embedding, which explains why transfer theorems that assume these properties are unaffected, and it is compatible with qualitative eventual categoricity. It also bears directly on a published claim of transfer at the prescribed bound for arbitrary AECs.

Formalizing it. Because the result contradicts a claimed theorem in the literature, an independent machine check is especially valuable. The formal statement verifies every AEC axiom explicitly, not just the two cardinal-arithmetic conclusions. Mathlib has cardinal and ordinal arithmetic, beth numbers and ZFC sets; the AEC framework built here would be reusable for further formal work in non-elementary model theory.

Difficulty

Most known non-transfer examples (Hart–Shelah) fail categoricity at small cardinals; here the failure must happen exactly at the Hanf-type bound ℶω2\beth_{\omega_2} while categoricity holds on a tail, with LS(K)=ℵ0\mathrm{LS}(K)=\aleph_0. One must build two nonisomorphic models at ℶω2\beth_{\omega_2} and simultaneously rule out any two nonisomorphic models above Λ\Lambda, without appealing to a general eventual-categoricity theorem. All AEC axioms — in particular coherence and smoothness of unions of arbitrary directed chains — must survive the exceptional sets used to separate models, which is where naive constructions break.

Formalization scope

  • Structures are RelModel L with carrier a ZFSet (so cardinalities are cardinals of genuine sets in universe u) and relations indexed by arity; L:N→L:\mathbb N\to Type with ΣnLn\Sigma_n L_n countable.
  • ClassData packages a predicate of objects and a strong-substructure relation; IsAEC lists the axioms above, including invariance under isomorphisms compatible with inclusion, coherence, and the union axioms for chains indexed by any nonzero ordinal.
  • HasLSNumber ℵ₀ asserts both that ℵ0\aleph_0 is a Löwenheim–Skolem bound and that it is the least one.
  • hanf κ = beth (succ (2^κ)).ord, endpoint = beth (ω_2), tailThreshold = beth (succ (2^{ℵ₁})).ord. The equality endpoint = hanf ℵ₀ is part of the goal (it follows from CH).
  • Categorical μ includes existence of a model of size μ\mu; TwoModels asks for two nonisomorphic models of the given size.
  • CH is a hypothesis of the theorem, in the same universe; the consistency corollary is not part of the goal.

Selected references

26 thms3 active usersReviewed
Mathematical LogicTheory of Computation·Captain: wurtle

Rigidity of the Turing degreesResearch Paper

Motivation

Turing reducibility compares sets of natural numbers by their information content: A≤TBA\le_TB if an oracle Turing machine with oracle BB computes the characteristic function of AA. Identifying mutually reducible sets gives the Turing degrees DT\mathcal D_T, partially ordered by ≤T\le_T. A central question of computability theory since the 1970s is how much of the underlying computational structure the abstract order remembers. The strongest possible answer is rigidity: the order has no nontrivial automorphisms, so every degree is determined by its position in the order.

Timeline

  • 1939. Turing introduces oracle machines and relative computability (doi:10.1112/plms/s2-45.1.161).
  • 1977. Jockusch and Solovay prove that every jump-preserving automorphism fixes all degrees above 0(4)\mathbf0^{(4)} (doi:10.1007/BF03007659).
  • 1980. Nerode and Shore prove that every automorphism fixes some cone of degrees, whose base may depend on the automorphism (doi:10.1016/0003-4843(80)90004-2).
  • 1999. Shore and Slaman prove that the Turing jump is definable from the order, so every automorphism preserves it (Math. Res. Lett., 1999).
  • 2005. Slaman and Woodin's manuscript Definability in Degree Structures shows that every automorphism fixes all degrees above 0′′\mathbf0'', that the automorphism group is countable, that every automorphism has an arithmetic representation on sets of integers, and that rigidity is equivalent to their biinterpretability conjecture; see also Slaman's survey (doi:10.1142/9789812794055_0002).
  • 2007. Shore gives direct degree-theoretic definitions of the jump (J. Math. Log., 2007).
  • 2018. Kjos-Hanssen shows that automorphisms induced by permutations of the integers are trivial (doi:10.1017/bsl.2018.15).

After these results the remaining problem was rigidity at degrees outside the known fixed cone. The source of this mission, an OpenAI preprint dated September 24, 2026, proves full rigidity.

Setting

An oracle is a function A:N→{0,1}A:\mathbb N\to\{0,1\} (a set of natural numbers). A≤TBA\le_TB means that the characteristic function of AA is partial recursive relative to BB. This is a preorder; its quotient by A≡TB  ⟺  (A≤TB∧B≤TA)A\equiv_TB\iff(A\le_TB\wedge B\le_TA) is the set DT\mathcal D_T of Turing degrees, partially ordered by ≤T\le_T. An automorphism of (DT,≤T)(\mathcal D_T,\le_T) is a bijection π:DT→DT\pi:\mathcal D_T\to\mathcal D_T with

a≤Tb  ⟺  π(a)≤Tπ(b).\mathbf a\le_T\mathbf b\iff\pi(\mathbf a)\le_T\pi(\mathbf b).

No definability, Borel or continuity hypothesis is imposed on π\pi.

Formalization targets

Goal: Theorem 1.1

∀π∈Aut⁡(DT,≤T)  ∀a∈DT:π(a)=a.\forall\pi\in\operatorname{Aut}(\mathcal D_T,\le_T)\ \ \forall\mathbf a\in\mathcal D_T:\qquad \pi(\mathbf a)=\mathbf a.

The Lean statement OAI.TuringRigidity.ManuscriptMain.rigidity is open on the platform.

Significance

Rigidity says that the order ≤T\le_T alone determines every Turing degree. By the theorem of Slaman and Woodin, it is equivalent to their biinterpretability conjecture: the degrees are biinterpretable without parameters with full second-order arithmetic (Corollary 5.1). Consequently every relation on degrees that is definable in second-order arithmetic and invariant under Turing equivalence is definable in the degree order, which settles a family of definability questions at once.

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. Its proof relies on the Slaman–Woodin representation theorem, whose cited source is an unpublished 2005 manuscript; a formalization would either need to formalize that input as well or isolate it as an explicit hypothesis, and would make the dependence fully transparent.

Difficulty

Earlier methods fix cones of degrees: coding arguments work above a sufficiently high base such as 0′′\mathbf0'', where enough information can be coded and decoded. Below that base the coding machinery is not available, and an arbitrary automorphism carries no a priori regularity. The proof must turn the arithmetic (hence Borel) representation of an automorphism into recovery of every individual real, using a category argument that works for every irrational parameter, not only generic ones.

Formalization scope

  • Oracles are ℕ → Bool; reducibility is Mathlib's TuringReducible between the characteristic functions viewed as partial functions ℕ →. ℕ (values 00 and 11).
  • Degree is Antisymmetrization Oracle Reduces with the induced partial order; automorphisms are order isomorphisms Degree ≃o Degree, i.e. bijections preserving and reflecting ≤T\le_T.
  • The statement quantifies over all order isomorphisms, with no measurability or definability assumption, as in the paper.

A complete development needs relativized computability (oracle machines, joins, the jump), Borel and Baire-category arguments on 2N2^{\mathbb N} and R\mathbb R, and the Slaman–Woodin representation theorem (Theorem 3.1). Formalizing that theorem would itself be a substantial and reusable contribution. Contributions formalizing Proposition 4.1 (recovery of an irrational from four values of a Borel subadditive map with countable fibers) are welcome.

Selected references

2 thms1 active userReviewed
Completed
Complexity TheoryMathematical LogicTheoretical Computer Science·Captain: wurtle

Choiceless polynomial time with counting does not capture polynomial timeResearch Paper

Motivation

Descriptive complexity asks whether complexity classes can be characterized by logics, without reference to machines. Immerman and Vardi (1982) showed that on ordered finite structures, first-order logic with a least fixed-point operator expresses exactly the polynomial-time queries. On unordered structures, such as graphs given only up to isomorphism, an algorithm must not depend on an arbitrary ordering of the input, and whether some logic captures polynomial time there is a central open question (Chandra–Harel 1982, Gurevich 1988).

Choiceless polynomial time with counting (CPT), introduced by Blass, Gurevich and Shelah (1999), was for decades the strongest candidate: it computes with hereditarily finite sets built over the input elements, can count, and is invariant under automorphisms by construction. Blass, Gurevich and Shelah conjectured that CPT is still a proper fragment of polynomial time. This mission concerns a proof of that conjecture.

Timeline

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

Setting

Fix the field F=F3\mathbb F=\mathbb F_3 and the vocabulary of eight binary relation symbols τ={Ed,Cf,EB,VB,I,Z0,Z1,Z2}\tau=\{\mathrm{Ed},\mathrm{Cf},\mathrm{EB},\mathrm{VB},I,Z_0,Z_1,Z_2\}. For a finite τ\tau-structure AA put

Y={y:Ed(y,y)},X={a:Cf(a,a)},Xt={a∈X:VB(t,a)} (t∈X),Y=\{y:\mathrm{Ed}(y,y)\},\quad X=\{a:\mathrm{Cf}(a,a)\},\quad X_t=\{a\in X:\mathrm{VB}(t,a)\}\ (t\in X), C(y,a)=∑x∈Y, I(a,x) ∑δ∈F, Zδ(y,x)δ.C(y,a)=\sum_{x\in Y,\ I(a,x)}\ \sum_{\delta\in\mathbb F,\ Z_\delta(y,x)}\delta .

With unknowns (λa)a∈X(\lambda_a)_{a\in X} and (μy)y∈Y(\mu_y)_{y\in Y} (separate families), the system consists of

∑a∈Xtλa=1(t∈X),μy=∑a∈Xtλa C(y,a)\sum_{a\in X_t}\lambda_a=1\quad(t\in X),\qquad \mu_y=\sum_{a\in X_t}\lambda_a\,C(y,a)

for every (t,y)∈X×Y(t,y)\in X\times Y such that some a∈Xta\in X_t and x∈Yx\in Y satisfy I(a,x)I(a,x) and EB(y,x)\mathrm{EB}(y,x). The query Q(A)Q(A) says this system is consistent over F3\mathbb F_3. No promise is imposed on the input.

A CPT program is a fixed finite set of rules that updates dynamic functions whose values are hereditarily finite sets over the atoms of AA, using pairing, union, comprehension, equality, membership, the input relations, and the cardinality operation (which returns a von Neumann ordinal). A program defines QQ if for fixed polynomials T,ST,S, on every input of size nn it halts within T(n)T(n) steps, touches at most S(n)S(n) hereditarily finite objects, and accepts exactly when Q(A)Q(A) holds. No bound on set rank is imposed.

Formalization targets

Goal: Theorem 1

Q is isomorphism-invariant,Q∈P (from an ordered encoding),Q∉CPT.Q\ \text{is isomorphism-invariant},\qquad Q\in\mathrm{P}\ \text{(from an ordered encoding)},\qquad Q\notin\mathrm{CPT}.

The Lean statement OAI.CPTSeparation.main is the conjunction of these three clauses. It is open on the platform.

Significance

The theorem confirms the Blass–Gurevich–Shelah noncapture conjecture for the full counting formalism: CPT does not capture polynomial time on unordered structures. It removes the leading candidate logic from Gurevich's question, which itself remains open. Because QQ is expressible in fixed-point logic with a solvability or rank operator over F3\mathbb F_3 (Corollary 3, p. 3), it also shows that neither of those logics is contained in CPT. The lower bound holds for programs of arbitrary set rank, unlike the bounded-rank lower bounds of Dawar–Richerby–Rossman.

The result is proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists.

Difficulty

The polynomial-time upper bound is Gaussian elimination. The obstacle is the lower bound against every CPT program, including those that build sets of unbounded rank. Bounded-variable counting games handle fixed-point logic with counting but do not by themselves control CPT, which is strictly stronger (it decides CFI queries over ordered base graphs). Rank-dependent support arguments give lower bounds only for each fixed rank. The paper needs support bounds independent of rank, for which it uses a nonabelian automorphism group acting on grid structures, then a counting equivalence for all supported objects, and finally a transfer to complete computations via an interpretation characterization of CPT.

Formalization scope

  • Input A gives a Boolean-valued binary relation for each Symbol (Ed, Cf, EB, VB, I, Z δ with δ : ZMod 3). Input.query is the existence of λ, μ satisfying the normalization and consistency equations exactly as above; an empty system is consistent.
  • OrdinaryPolynomialTime asks for a function on ordered tables and a Turing.TM2ComputableInPolyTime machine with finite alphabets computing it from the cell-by-cell table encoding, agreeing with the query for every ordering of every structure.
  • FullCPT defines terms and rules over hereditarily finite sets (Lists quotient), a state of finitely many nonempty locations, synchronous consistent updates, halt/accept flags, and the set of occurring objects (active elements plus roots of evaluated terms). EvaluationDefinable Q asks for one program and polynomials time, space that accept exactly the inputs satisfying Q, halting within time and with at most space occurring objects.
  • This is the original operational formulation; the paper's proof passes through the interpretation characterization of CPT (Grädel–Pakusa–Schalthöfer–Kaiser), which a formal proof must either formalize or bypass.

A complete development needs: hereditarily finite sets and automorphism actions on them, support theory, counting equivalence games, the grid structures with their automorphism group, and a CPT-to-interpretation translation. Contributions formalizing Proposition 2 (polynomial-time decidability), Proposition 8 (small-orbit support bound), Proposition 13 (quantitative homogeneity) and Theorem 14 (transfer through small supports) are welcome.

Selected references

4 thms2 active usersReviewed
Complexity TheoryMathematical LogicTheoretical Computer Science·Captain: wurtle

Witnessed symmetric choice is strictly stronger than choiceless polynomial time with countingResearch Paper

Motivation

A logic for unordered finite structures (graphs, databases, relational inputs given up to isomorphism) must give answers that do not depend on how the input elements are named. Many polynomial-time algorithms nevertheless make arbitrary intermediate choices, for example the pivot in Gaussian elimination, without changing their final answer. Choiceless polynomial time with counting (CPT), introduced by Blass, Gurevich and Shelah (1999), forbids such choices entirely: it computes with hereditarily finite sets over the input elements and can count, but can never pick one element from a set merely because the set is nonempty.

Witnessed symmetric choice (WSC), in the form of Lichter and Schweitzer (2022, arXiv version 3), adds a controlled form of choice: the logic may pick an element of a set provided it also constructs automorphisms of the input showing that all elements of that set are interchangeable, so the answer cannot depend on which one was picked. Lichter and Schweitzer asked whether CPT + WSC is strictly more expressive than CPT. This mission concerns a proof that it is.

Timeline

The source of this mission is an OpenAI preprint dated September 24, 2026; its companion preprint (September 23, 2026) proves that CPT does not capture polynomial time.

Setting

Let AA be a finite set of atoms and HF(A)\mathrm{HF}(A) the hereditarily finite sets over AA. CPT terms are built from variables, ∅\emptyset, Atoms\mathrm{Atoms}, Pair(a,b)={a,b}\mathrm{Pair}(a,b)=\{a,b\}, Union\mathrm{Union}, Unique\mathrm{Unique} (the member of a singleton, else ∅\emptyset), Card\mathrm{Card} (the von Neumann ordinal ∣a∣|a|), comprehensions {s(aˉ,u):u∈t(aˉ), θ(aˉ,u)}\{s(\bar a,u):u\in t(\bar a),\ \theta(\bar a,u)\} and iteration from ∅\emptyset; formulas use input relations, equality and Boolean connectives. A sentence (Φ,p)(\Phi,p) pairs a closed formula with a polynomial pp that bounds the number of iteration steps and the hereditary size of all intermediate objects on inputs with nn atoms; exceeding the bounds yields a default or a failure value †\dagger.

A WSC operator iterates a step term in which, at each stage, a choice term proposes a nonempty set DD; one element is chosen, and a witness term must produce automorphisms of the entire input that fix the parameters and all earlier stages and map any element of DD to any other. If the witnesses are valid along every possible choice sequence, the output formula's value on the terminal state is returned; otherwise the value is †\dagger.

The true-model class of a sentence is the set of finite structures on which it returns true; false and †\dagger are both outside it.

Formalization targets

Goal: Theorem 1.1

For the fixed vocabulary τ\tau of eight binary relations there is a CPT + WSC sentence (Φ,p)(\Phi,p) with exactly one WSC occurrence such that

(i) (Φ,p) returns true or false on every finite τ-structure;(ii) TrueModels(Φ,p)≠TrueModels(Ψ,q) for every CPT sentence (Ψ,q).\text{(i)}\ (\Phi,p)\ \text{returns true or false on every finite }\tau\text{-structure;}\qquad \text{(ii)}\ \mathrm{TrueModels}(\Phi,p)\neq\mathrm{TrueModels}(\Psi,q)\ \text{for every CPT sentence }(\Psi,q).

The Lean statement OAI.WitnessedChoice.main (via BGS.MainStatement) is open on the platform.

Significance

Since every CPT sentence is a CPT + WSC sentence, Theorem 1.1 gives a strict inclusion of definable Boolean queries and answers the expressiveness question posed by Lichter and Schweitzer in the true-model sense. The separation holds against CPT with counting and sets of arbitrary finite rank, not a rank-restricted fragment. It leaves open whether CPT + WSC captures polynomial time and the effect of nesting WSC operators.

The result is proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists.

Difficulty

Two different tasks must be done. The upper bound requires a legal WSC definition on all inputs, not only on the intended grid structures: witnesses must be genuine automorphisms of the whole input fixing the full history, which the sentence must check, with a fallback when the input is not of the intended shape. The lower bound must defeat every CPT sentence, including those that build nested sets of large rank; rank-sensitive support arguments (Dawar–Richerby–Rossman) do not suffice. The paper uses a nonabelian automorphism group whose central subgroup has rank-independent small supports, then a counting equivalence and a bounded-width description of complete CPT evaluations.

Formalization scope

  • Syntax is a mutual inductive Term n / Formula n with de Bruijn-style Fin n variables, including iterate and the wsc formula; wscCount counts WSC occurrences.
  • Evaluation returns Option (none is †\dagger). resource p n = ⌊p(n)⌋ bounds iteration length and transitive-closure size.
  • WSC validity (GoodWSC) quantifies over all choice prefixes; witnesses are permutationGraph g for permutations g that are input automorphisms, fix the free parameters and every earlier stage, and act transitively on the choice set.
  • FiniteInput packs any finite carrier type with the eight-symbol relations (Ed, Cf, EB, VB, I, Z δ, δ : ZMod 3). Sentence.isCPT means wscCount = 0.

A complete development needs hereditarily finite sets with permutation actions, support and counting-equivalence theory, and the grid structures; much of this is shared with the companion CPT noncapture mission. Contributions formalizing Proposition 4.4 (a total all-input definition), Proposition 5.3 (transitivity for every parameter tree), Theorem 5.5 (opposite grid answers), Proposition 6.3 (small-orbit support bound), Theorem 8.1 (transfer through small supports) and Theorem 9.3 (eventual equality for every CPT sentence) are welcome.

Selected references

2 thms1 active userReviewed
Mathematical LogicTheoretical Computer Science·Captain: wurtle

Weak and strong normalization in pure type systemsResearch Paper

Motivation: does having a normal form imply termination?

Pure type systems (PTSs) are a uniform framework covering the simply typed λ-calculus, System F, the calculus of constructions and the type theories behind proof assistants such as Coq and Lean. A system is specified by its sorts (like ∗\ast and □\square), axioms (∗:□\ast:\square) and product rules (which dependent function types may be formed). Normalization is the key metatheoretic property: it underlies logical consistency and decidability of type checking. There are two versions. A term is weakly normalizing if some sequence of β-reductions reaches a normal form, and strongly normalizing if every reduction sequence is finite. Strong normalization is what implementations need (any evaluation strategy terminates) but it is much harder to prove. The Barendregt–Geuvers–Klop conjecture asserts that, for pure type systems, the system-wide weak property already implies the strong one.

Timeline

  • 1989 — Girard's Proofs and Types presents the Tait–Girard reducibility method for strong normalization (book).
  • 1993 — Geuvers states the system-wide conjecture for β and βη reduction in his thesis (Logics and Type Systems, Nijmegen, Conjecture 8.1.2) (thesis).
  • 1997 — Sørensen proves the implication for generalized nondependent, clean, negatable systems via continuation-passing translations (thesis, Copenhagen, Theorem 3.5.20).
  • 2001 — Barthe, Hatcliff and Sørensen prove a uniform nondependent version (TCS 2001).
  • 2006 — Barthe and Coquand show that erasing λ-domain annotations can identify non-convertible terms in non-normalizing PTSs (JFP 2006), a constraint on erasure-based approaches.
  • 2014 — Roux and van Doorn develop a structural theory of PTSs, preserving weak normalization under sums and added rules (RTA–TLCA 2014).
  • 2023 — Mull reduces the conjecture within tiered systems to an irrelevance-eliminating translation (TYPES 2022, LIPIcs 2023) and extends the nondependent results in his thesis (Chicago, 2023).
  • 2025 — Roux proposes internal strong-normalization proofs for specific systems (TYPES 2025 abstract).
  • 2026 — An OpenAI preprint, Weak and strong normalization in pure type systems (OpenAI Math Release, September 25, 2026), claims the β-version of the conjecture for every PTS, with no functionality assumption. The preprint has not been peer reviewed and its theorem is not formally verified.

Setting

A specification consists of a type SS of sorts, an axiom relation A⊆S2\mathcal A\subseteq S^2 and a rule relation R⊆S3\mathcal R\subseteq S^3; neither is assumed functional. Expressions are

M,N,A,B::=x∣s∣MN∣λx:A. M∣Πx:A. B,s∈S,M,N,A,B ::= x\mid s\mid MN\mid \lambda x{:}A.\,M\mid \Pi x{:}A.\,B,\qquad s\in S,

up to renaming of bound variables. β-reduction is the compatible closure of (λx:A.M)N→βM[x:=N](\lambda x{:}A.M)N\to_\beta M[x:=N], with steps allowed everywhere, including inside the annotation AA of a λ and both parts of a Π. Typing Γ⊢M:A\Gamma\vdash M:A is generated by the seven standard PTS rules (axiom, variable, weakening, product, abstraction, application, conversion up to =β=_\beta). A context is valid if each declared type is typed by a sort in the preceding prefix, and MM is legal in Γ\Gamma if Γ⊢M:A\Gamma\vdash M:A or Γ⊢A:M\Gamma\vdash A:M for some AA.

The system is weakly (strongly) normalizing if every legal expression in every valid context is weakly (strongly) normalizing.

Formalization targets

Goal: β-Barendregt–Geuvers–Klop (Theorem 1)

For every specification P=(S,A,R)\mathcal P=(S,\mathcal A,\mathcal R),

(∀Γ valid, ∀M legal in Γ: M is weakly β-normalizing) ⟹ (∀Γ valid, ∀M legal in Γ: M is strongly β-normalizing).\bigl(\forall \Gamma\ \text{valid},\ \forall M\ \text{legal in }\Gamma:\ M\ \text{is weakly }\beta\text{-normalizing}\bigr) \ \Longrightarrow\ \bigl(\forall \Gamma\ \text{valid},\ \forall M\ \text{legal in }\Gamma:\ M\ \text{is strongly }\beta\text{-normalizing}\bigr).

Both quantifiers range over the whole system; the theorem does not claim that an individual weakly normalizing term is strongly normalizing, and it says nothing about η-reduction. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. For any PTS, a proof that every legal term has a normal form now yields termination of every β-reduction strategy, including reductions inside types and annotations that may continue after the computational body is normal. Earlier results needed nondependent products, cleanliness, negatability, a tiered sort hierarchy, or a translation requiring extra product rules; the general case — arbitrary sorts and nonfunctional rules — was not covered by any earlier result since Geuvers' 1993 formulation.

Formalizing it. The statement is entirely syntactic and finitary, so it is a natural target for a proof assistant, and the relevant objects (de Bruijn syntax, substitution, typing derivations) are standard formalization material. The proof in the source is long (over 70 pages) and combines reducibility candidates with a fixed-point construction over sort profiles; a machine check would substantially raise confidence. A formal PTS metatheory library (substitution lemmas, confluence, subject reduction) would be reusable for other type-theory formalizations.

Difficulty

The obvious route — reducibility candidates à la Tait–Girard — needs a model of types built by recursion on sorts, which fails for impredicative or nonfunctional specifications where a type can have several sorts and no hierarchy is available. Translation methods (CPS or irrelevance elimination) need specific product rules to preserve typing, which a general specification may lack. Weak normalization of one term cannot be used alone; the argument must exploit normal forms of other open expressions. Annotations add a further complication: erasing them can change the equational theory (Barthe–Coquand), so reduction inside annotations must be tracked rather than erased.

Formalization scope

  • Expressions use de Bruijn indices (Expr S with var, sort, app, lam, pi), so α-equivalence is syntactic; substitution is parallel substitution with lifting.
  • Beta is full compatible closure, including lam_domain, pi_domain and pi_body steps; conversion is Relation.EqvGen Beta.
  • HasType has exactly the seven PTS rules; contexts are lists stored newest-first, each declaration typed in its prefix (ValidContext). Legal includes expressions occurring as types.
  • Weak normalization is reduction to a normal form; strong normalization is accessibility for the converse of Beta.
  • The sort type S is arbitrary (any universe), and axioms and rules are arbitrary relations: no functionality, finiteness or hierarchy assumptions.
  • Needed infrastructure: renaming/substitution lemmas, confluence of β, subject reduction for PTSs, reducibility candidates. All are reusable for any PTS formalization.

Selected references

2 thms1 active userReviewed
Geometry & TopologyGroup Theory·Captain: wurtle

A Modulus Proof of Cannon’s ConjectureResearch Paper

Motivation

A finitely generated group is (word-)hyperbolic if the geodesic triangles in its Cayley graph are uniformly thin, as in the hyperbolic plane. Such a group has a boundary at infinity ∂G\partial G, a compact space of asymptotic directions. The fundamental group of a closed hyperbolic 3-manifold is hyperbolic with boundary the 2-sphere. Cannon's conjecture asks for the converse: if a hyperbolic group has boundary homeomorphic to S2S^2, does it act geometrically on hyperbolic three-space H3\mathbb H^3? An affirmative answer characterizes, purely in terms of coarse geometry, which groups arise from closed hyperbolic 3-manifolds; it is one of the central problems of geometric group theory and is closely tied to the geometrization program for 3-manifolds.

Timeline

  • 1981, 1980. Sullivan and Tukia show that groups of uniformly quasiconformal maps of the sphere are conjugate to Möbius groups (Sullivan, Stony Brook 1978 proceedings; Tukia, doi:10.5186/aasfm.1980.0530).
  • 1989. Pansu introduces conformal dimension of boundaries (doi:10.5186/aasfm.1989.1424).
  • 1994. Cannon's combinatorial Riemann mapping theorem recovers quasiconformal coordinates from discrete moduli (doi:10.1007/BF02398434).
  • 1998. Cannon and Swenson state the group-boundary conjecture and relate geometric actions to conformality of boundary coverings (doi:10.1090/S0002-9947-98-02107-2).
  • 1999. Cannon, Floyd and Parry reduce the problem to bounded discrete moduli of annuli at small scales (Ann. Acad. Sci. Fenn. Math., 1999).
  • 2002, 2005. Bonk and Kleiner develop quasisymmetric uniformization of metric spheres and prove the conjecture when the Ahlfors-regular conformal dimension is attained (doi:10.1007/s00222-002-0233-z, doi:10.2140/gt.2005.9.219).
  • 2012–2013. Kahn–Marković, Bergeron–Wise, Agol and Marković connect surface subgroups, cubulation and Kleinian realizations (doi:10.4007/annals.2012.175.3.4, doi:10.4171/DM/421, doi:10.1007/s00039-013-0228-5). Bourdon and Kleiner give a combinatorial-modulus criterion for uniformization (doi:10.4171/GGD/177).
  • 2015. Haïssinsky proves a virtual Kleinian criterion for cubulated hyperbolic groups with planar boundary (doi:10.1007/s00222-014-0552-x).
  • 2026. Groves, Haïssinsky, Manning, Osajda, Sisto and Walsh reduce the residually finite case to the Toral Relative Cannon conjecture (arXiv:2406.14667).

The source of this mission, an OpenAI preprint dated September 23, 2026, follows the analytic route and proves the conjecture.

Setting

Let GG be a group with a finite symmetric generating set SS and Cayley graph Γ(G,S)\Gamma(G,S) with graph distance dd. GG is hyperbolic if there is δ\delta such that every point on a side of a geodesic triangle lies within d≤δd\le\delta of the union of the other two sides. A geodesic ray based at 11 is a sequence r0=1,r1,…r_0=1,r_1,\dots with d(ri,rj)=∣i−j∣d(r_i,r_j)=|i-j|; two rays are equivalent if d(rn,sn)d(r_n,s_n) stays bounded. The boundary ∂G\partial G is the set of equivalence classes with the quotient of the topology of pointwise convergence.

H3\mathbb H^3 is the upper half-space {x∈R3:x3>0}\{x\in\mathbb R^3: x_3>0\} with distance arcosh⁡(1+∣x−y∣2/(2x3y3))\operatorname{arcosh}\bigl(1+|x-y|^2/(2x_3y_3)\bigr), and Isom⁡(H3)\operatorname{Isom}(\mathbb H^3) is its full isometry group, including orientation-reversing isometries. A homomorphism ρ:G→Isom⁡(H3)\rho:G\to\operatorname{Isom}(\mathbb H^3) gives a proper action if {g:ρ(g)K∩K≠∅}\{g:\rho(g)K\cap K\ne\varnothing\} is finite for every compact KK, and a cocompact action if translates of one compact set cover H3\mathbb H^3.

Formalization targets

Goal: Theorem 1.1

G hyperbolic, ∂G≅S2 ⟹ ∃ ρ:G→Isom⁡(H3) proper, cocompact, with ker⁡ρ finite.G\ \text{hyperbolic},\ \partial G\cong S^2\ \Longrightarrow\ \exists\,\rho:G\to\operatorname{Isom}(\mathbb H^3)\ \text{proper, cocompact, with }\ker\rho\ \text{finite}.

The Lean statement OAI.CannonRelease.cannon is open on the platform.

Significance

The theorem identifies hyperbolic groups with 2-sphere boundary, up to finite kernels, with uniform lattices in Isom⁡(H3)\operatorname{Isom}(\mathbb H^3). For torsion-free GG, the quotient H3/G\mathbb H^3/G is a closed hyperbolic 3-manifold, possibly nonorientable (Corollary 8.1), and the work of Kahn–Marković, Bergeron–Wise and Agol then gives virtual structure results (Corollary 8.2). It also settles the hypotheses of the reductions of Marković and of Groves et al. in full generality.

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. A formal proof would require formal infrastructure for hyperbolic groups and their boundaries, quasiconformal analysis and combinatorial modulus, very little of which is currently in Mathlib.

Difficulty

By the Cannon–Floyd–Parry and Bourdon–Kleiner criteria, the theorem reduces to a uniform upper bound on the combinatorial 2-modulus of curve families at all scales of the boundary. The bound is easy to state but there is no a priori reason why moduli of coverings of a topological sphere should stay bounded; Bonk–Kleiner needed the extra hypothesis that the conformal dimension is attained. A proof must extract analytic control (a nonconstant limit function with controlled oscillation) from a hypothetical sequence of coverings with unbounded modulus and contradict it using only hyperbolicity and the topology of the boundary.

Formalization scope

  • CayleyData G is a finite symmetric generating set with connected SimpleGraph.mulCayley; ThinTriangles asks for one natural number δ\delta working for all geodesic triangles given as walks of length equal to graph distance.
  • Rays are ℕ → G with r 0 = 1 and dist (r i) (r j) = |i-j|; the boundary is the quotient by bounded synchronous distance. GG carries the discrete topology, rays the subspace product topology, and the boundary the quotient topology, which coincides with the visual topology for hyperbolic groups.
  • S2S^2 is the unit sphere in EuclideanSpace ℝ (Fin 3); H3\mathbb H^3 is the upper half-space with the explicit arcosh distance and subspace topology; isometries are self-homeomorphisms preserving that distance.
  • The kernel is only required to be finite, and orientation-reversing elements are allowed, matching the paper.

A complete development needs Gromov hyperbolic groups and visual metrics, approximately self-similar spheres, combinatorial modulus and the Bonk–Kleiner/Bourdon–Kleiner uniformization criterion, and the Sullivan–Tukia straightening of uniformly quasiconformal groups. Contributions formalizing Proposition 2.6 (from a round boundary action to a geometric action on H3\mathbb H^3) or Theorem 2.5 (the uniformization criterion) are welcome.

Selected references

2 thms1 active userReviewed
Completed
Functional AnalysisGroup Theory·Captain: wurtle

Thompson's group F is nonamenableResearch Paper

Motivation

Thompson's group FF consists of the increasing piecewise linear homeomorphisms of [0,1][0,1] with finitely many pieces, dyadic rational breakpoints, and slopes that are integer powers of 22. It is finitely presented, has strong topological finiteness properties, and appears across group theory, dynamics and logic. Whether FF is amenable, i.e. whether its bounded functions admit a translation-invariant mean, is one of the best-known open questions about a single explicit group. It is a natural test case because the two classical routes to deciding amenability both fail: FF contains no nonabelian free subgroup (Brin–Squier 1985), so the free-subgroup obstruction is unavailable, yet FF is not elementary amenable (Cannon–Floyd–Parry 1996, Theorem 4.10). Geoghegan conjectured in 1979 that FF is nonamenable. The problem has attracted claimed resolutions in both directions, several later withdrawn or found to contain errors.

This mission asks for a formal proof of nonamenability as stated in an OpenAI preprint dated September 23, 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

Setting

A homeomorphism ff of [0,1][0,1] is a dyadic PL map if there are dyadic rationals 0=x0<x1<⋯<xk=10=x_0<x_1<\dots<x_k=1 and integers eie_i such that on each [xi−1,xi][x_{i-1},x_i], f(x)=f(xi−1)+2ei(x−xi−1)f(x)=f(x_{i-1})+2^{e_i}(x-x_{i-1}). The group FF is the set of increasing dyadic PL homeomorphisms of [0,1][0,1], with multiplication hg=h∘ghg=h\circ g, regarded as a discrete group. Let ℓ∞(F;R)\ell^\infty(F;\mathbb R) be the bounded real functions on FF. A left-invariant mean is a linear functional M:ℓ∞(F;R)→RM:\ell^\infty(F;\mathbb R)\to\mathbb R with M(1)=1M(\mathbf 1)=1, M(φ)≥0M(\varphi)\ge0 whenever φ≥0\varphi\ge0, and M(g↦φ(hg))=M(φ)M(g\mapsto\varphi(hg))=M(\varphi) for every h∈Fh\in F. FF is amenable if such a mean exists.

Formalization targets

Goal: Theorem 1.1 (p. 1)

Thompson's group FF is not amenable: there is no positive, normalized, left-invariant mean on ℓ∞(F;R)\ell^\infty(F;\mathbb R).

Significance

The result itself. It settles Geoghegan's conjecture and the amenability problem for FF. Because FF has no free subgroups, FF becomes a finitely presented, torsion-free example of a nonamenable group without free subgroups. Through companion results the preprint derives that FF has uniformly bounded representations that are not unitarizable (Corollary 3.1, p. 7) and that Bernoulli percolation on every Cayley graph of FF has a nonuniqueness phase (Corollary 3.2, p. 8). The proof is short (Section 2) and uses an infinite-dimensional fixed-point phenomenon: the Benyamini–Sternfeld theorem that the unit ball of an infinite-dimensional Hilbert space admits a Lipschitz self-map moving every point by at least a fixed δ>0\delta>0 (Lemma 1.2, p. 2; Proc. AMS 1983).

Formalizing it. Given the length of the published argument, this is a realistic target for a complete formal proof of a result that had been open for over forty years. It needs the dyadic-partition model of FF, the Følner criterion (forward direction), and a Lipschitz map on a Hilbert ball with no approximate fixed points (Appendix A of the preprint constructs one on L2([0,1];R2)L^2([0,1];\mathbb R^2) with δ=1/2\delta=1/2). The Følner direction from invariant means to Følner sets is reusable infrastructure for amenability in Mathlib.

Difficulty

Neither standard obstruction applies: there is no free subgroup to produce a paradoxical decomposition, and no structural closure property shows amenability. Følner sets, if they existed, would have to grow extremely fast (Moore's tower bounds), so explicit counting is ineffective. The preprint's argument converts approximate invariance of a finite set A⊂FA\subset F into an approximate fixed point of a Lipschitz map on a Hilbert ball, via recursively defined Hilbert-valued colours of dyadic partitions. The delicate points are exact covariance of normalized restrictions under the group action (equation (2.2), p. 4) and controlling the diagonal and nested pairs in the correlation expansion, which yields a uniform lower bound on the relative boundary of every finite set (Proposition 2.3, p. 5).

Formalization scope

  • UnitInterval is Set.Icc (0:ℝ) 1; an element of F is a homeomorphism of it that is StrictMono and has a DyadicPLWitness: finitely many strictly increasing dyadic knots from 00 to 11 and integer exponents with the affine formula on each piece.
  • The goal asserts that some group structure on F exists whose multiplication is composition ((h * g) x = h (g x)); since multiplication is fixed, this structure is unique.
  • InvariantMean F is a real-linear functional on lp (fun _ : F => ℝ) ∞ that is positive, sends the constant 11 to 11, and is invariant under leftPull h, φ↦(g↦φ(hg))\varphi\mapsto(g\mapsto\varphi(hg)); the goal is ¬ Nonempty (InvariantMean F).
  • No generating set, Følner constant or boundary bound is fixed in the statement, so the goal is stable under improved constants.

Selected references

7 thms2 active usersReviewed
Algebraic TopologyGroup Theory·Captain: wurtle

A finitely generated counterexample to the Eilenberg–Ganea conjectureResearch Paper

Motivation: algebraic versus geometric dimension of groups

Two numbers measure how "large" a discrete group Γ\Gamma is. The cohomological dimension cd⁡Γ\operatorname{cd}\Gamma is algebraic: the length of the shortest projective resolution of the trivial module Z\mathbb Z over the group ring Z[Γ]\mathbb Z[\Gamma]. The geometric dimension gd⁡Γ\operatorname{gd}\Gamma is topological: the least dimension of a CW complex with fundamental group Γ\Gamma and contractible universal cover (a classifying space or K(Γ,1)K(\Gamma,1)). Cellular chains of a classifying space give a free resolution, so cd⁡Γ≤gd⁡Γ\operatorname{cd}\Gamma\le\operatorname{gd}\Gamma. Eilenberg and Ganea proved in 1957 that equality holds whenever cd⁡Γ≥3\operatorname{cd}\Gamma\ge3, and Stallings and Swan settled dimension one. The remaining case — must a group of cohomological dimension two have a two-dimensional classifying space? — is the Eilenberg–Ganea conjecture, closely tied to Whitehead's asphericity conjecture in low-dimensional topology.

Background

  • 1941 — Whitehead asks whether every connected subcomplex of an aspherical 2-complex is aspherical (Ann. of Math. 1941).
  • 1957 — Eilenberg and Ganea prove cd⁡=gd⁡\operatorname{cd}=\operatorname{gd} for cd⁡≥3\operatorname{cd}\ge3 and pose the dimension-two question (Ann. of Math. 1957).
  • 1968–1969 — Stallings proves that finitely generated groups of cohomological dimension one are free (Ann. of Math. 1968); Swan removes finite generation (J. Algebra 1969).
  • 1997 — Bestvina and Brady introduce height kernels of right-angled Artin groups and show that for suitable flag triangulations of a spine of the Poincaré homology sphere at least one of the Eilenberg–Ganea and Whitehead conjectures fails (Invent. Math. 1997, Thm 8.7).
  • 1999 — Dicks and Leary give presentations of these kernels (Proc. AMS 1999); Howie studies them via plus constructions (Math. Proc. Camb. Phil. Soc. 1999).
  • 2026 — Leary and Petrosyan compare Coxeter and Bestvina–Brady candidates for the problem (arXiv:2605.07853).
  • 2026 — An OpenAI preprint, A finitely generated counterexample to the Eilenberg–Ganea conjecture (OpenAI Math Release, September 23, 2026), claims a finitely generated residually finite group with cd⁡=2\operatorname{cd}=2 and gd⁡=3\operatorname{gd}=3. The preprint has not been peer reviewed and its theorem is not formally verified.

Setting

For a finite simplicial graph Δ\Delta with vertex set VV, the right-angled Artin group is

AΔ=⟨aq (q∈V) ∣ aqaraq−1ar−1=1 whenever q,r are adjacent⟩,A_\Delta=\bigl\langle a_q\ (q\in V)\ \bigm|\ a_qa_ra_q^{-1}a_r^{-1}=1\ \text{whenever } q,r \text{ are adjacent}\bigr\rangle ,

and the height homomorphism λ:AΔ→Z\lambda:A_\Delta\to\mathbb Z sends every aqa_q to 11. Its kernel is a Bestvina–Brady group.

The specific graph comes from the presentation complex KK of ⟨x,y∣x2y−5, x2(yx−1)3⟩\langle x,y\mid x^2y^{-5},\ x^2(yx^{-1})^{3}\rangle, which is integrally acyclic and has a nontrivial representation of its fundamental group into SU(2)\mathrm{SU}(2). Subdivide each of the two loops of KK into three edges, cone the boundary of each relator polygon to a new interior vertex (keeping one radial edge per boundary occurrence), and take the order complex of the resulting regular cell structure (7 vertices, 51 edges, 45 triangular sectors). This is a flag triangulation LL of KK; Δ\Delta is its 1-skeleton, i.e. the comparability graph of the cells. The group is G=ker⁡λ≤AΔG=\ker\lambda\le A_\Delta.

A group is residually finite if every nontrivial element survives in some finite quotient.

Formalization targets

Goal: the counterexample (Theorem 1.1)

For the group GG above,

G is finitely generated and residually finite,cd⁡G=2,G has a 3-dimensional K(G,1),G has no 2-dimensional K(G,1).G\ \text{is finitely generated and residually finite},\qquad \operatorname{cd}G=2,\qquad G \text{ has a 3-dimensional } K(G,1),\qquad G \text{ has no 2-dimensional } K(G,1).

In particular gd⁡G=3≠2=cd⁡G\operatorname{gd}G=3\ne2=\operatorname{cd}G. The non-existence clause holds for classifying spaces with any number of cells. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. The theorem disproves the Eilenberg–Ganea conjecture with a finitely generated (indeed type FL\mathrm{FL}, but not finitely presented) residually finite group, so the conjecture fails even for countable groups with strong finiteness properties. By Bestvina–Brady's dichotomy the Whitehead conjecture is not directly decided by this example, but the gap between the algebraic and geometric dimensions in dimension two is now exhibited concretely.

Formalizing it. The statement is concrete: an explicit finite graph, its Artin group and height kernel, a projective dimension, and existence/non-existence of CW models. The non-existence clause ranges over all CW complexes of arbitrary cardinality, which is exactly the kind of universally quantified topological claim where a machine check is valuable. Groundwork includes classifying spaces in Mathlib's CW-complex framework, projective dimension over group rings, and Bestvina–Brady Morse theory.

Difficulty

The kernel acts freely on an acyclic 2-complex, which gives cd⁡G≤2\operatorname{cd}G\le2, but an acyclic complex need not be contractible, and showing that one particular 2-dimensional model fails to be a K(G,1)K(G,1) says nothing about other models. The obstacle is to rule out every hypothetical two-dimensional classifying space, with arbitrarily many cells, and to do so for a group that is not finitely presented. Homological invariants cannot see the difference, since they agree with those of a genuine 2-dimensional model.

Formalization scope

  • The seed complex is encoded combinatorially: signed relator words seedWord, rose vertices, circle edges and sectors; seedGraph is the comparability graph of the cell face relation. ArtinGroup is a PresentedGroup on commutators of adjacent vertices, height sends each generator to 11 in Multiplicative ℤ, and SourceGroup is its kernel.
  • cohomologicalDimension is the categorical projective dimension (in WithBot ℕ∞) of the trivial Z[G]\mathbb Z[G]-module in ModuleCat.
  • HasClassifyingSpace G n asks for a Hausdorff, path-connected CW complex with no cells above dimension nn, fundamental group isomorphic to GG, and a surjective covering map from a contractible space. The positive clause is stated in universe 0; the negative clause is universe-polymorphic, so no restriction on the cardinality of cells is imposed.
  • Needed infrastructure: Bestvina–Brady level complexes, presentations of height kernels, residual finiteness of RAAG subgroups, SU(2)\mathrm{SU}(2) representations and degree arguments.

Selected references

2 thms1 active userReviewed
Completed
AlgebraGroup TheoryMathematical Logic·Captain: wurtle

Finite algebraic envelopes and the Boone–Higman conjectureResearch Paper

Motivation

The word problem for a group with a finite generating set asks whether a given word in the generators and their inverses represents the identity; it is decidable if one algorithm answers this for every word. Since Higman's embedding theorem (1961), a recurring theme in combinatorial group theory has been to characterize algorithmic properties of groups by embeddings into groups with good algebraic properties. Boone and Higman (1974) proved that a finitely generated group has decidable word problem if and only if it embeds in a simple subgroup of a finitely presented group, and asked whether the simple group can itself be taken finitely presented. This is the Boone–Higman conjecture.

This preprint states a proof of the conjecture: a finitely generated group has decidable word problem if and only if it embeds in a finitely presented simple group.

Background

  • 1961. Higman characterizes finitely generated subgroups of finitely presented groups as the recursively presented groups.
  • 1974. Boone and Higman prove the characterization G≤H≤KG \le H \le K with HH simple and KK finitely presented, and ask whether HH can be finitely presented.
  • 1980. Thompson embeds every finitely generated group with decidable word problem into a finitely generated simple group with decidable word problem; a later proof is given by Darbinyan and Steenbock (2022).
  • 2022. Belk and Zaremsky introduce twisted Brin–Thompson groups, which embed an acting group in a simple group; Zaremsky (2024) gives a finite-presentation criterion requiring a finitely presented acting group with finitely generated point stabilizers and finitely many orbits on unordered pairs.
  • 2023–2026. The conjecture is verified for hyperbolic groups and contracting self-similar groups (Belk, Bleak, Matucci, Zaremsky), Baumslag–Solitar and free-by-cyclic groups (Bux, Llosa Isenrich, Wu), and Aut(Fn)\mathrm{Aut}(F_n) and mapping class groups of punctured surfaces (Belk, Fournier-Facio, Hyde, Zaremsky); see the survey of Belk, Bleak, Matucci and Zaremsky.
  • 2026. The OpenAI preprint Finite algebraic envelopes and the Boone–Higman conjecture (dated September 23, 2026) states a proof of the conjecture in general. It has not been peer reviewed; the Lean goal is open on this platform.

Setting

A group GG is finitely generated if some finite tuple g1,…,gng_1, \dots, g_n generates it. A word is a finite list of letters gi±1g_i^{\pm1}; GG has decidable word problem if for some finite generating tuple the set of words evaluating to 11 is computable. A group is finitely presented if it has a presentation with finitely many generators and relations, and simple if it is nontrivial with no normal subgroups other than 11 and itself. An embedding is an injective homomorphism.

In Lean (OAI.FiniteAlgebraicEnvelopes, definitions BooneHigman), words are List (Fin n × Bool), evalWord multiplies generators or their inverses, HasDecidableWordProblem G asserts a generating tuple whose identity predicate is ComputablePred, and EmbedsInFinitelyPresentedSimpleGroup G asserts a group in the same universe that is Group.IsFinitelyPresented and IsSimpleGroup, with an injective homomorphism from GG.

Formalization targets

Goal: Theorem 1.1 (Boone–Higman conjecture)

For every finitely generated group GG,

G has decidable word problem  ⟺  G embeds in a finitely presented simple group.G \text{ has decidable word problem} \iff G \text{ embeds in a finitely presented simple group.}

The implication from right to left is classical (a finitely presented simple group has decidable word problem, and the property passes to finitely generated subgroups); the content is the forward implication.

Significance

The result. Theorem 1.1 gives a purely algebraic characterization of decidability of the word problem and settles a question open since 1974. Its intermediate result, Theorem 1.2, embeds every finitely generated group with decidable word problem in a finitely presented group with a faithful two-transitive action on a countably infinite set with finitely generated point stabilizers, which feeds Zaremsky's criterion for twisted Brin–Thompson groups.

Formalizing it. No machine-checked proof exists, and the source is an unrefereed preprint. Formalizing it requires computability of word problems, finite presentations (available in Mathlib as Group.IsFinitelyPresented), Steinberg groups over noncommutative rings, and twisted Brin–Thompson groups, which are not in Mathlib. The proof also uses Zaremsky's finite-presentation theorem (Theorem 2.3) from the literature, which a complete formalization must include.

Difficulty

Finite presentation does not pass to subgroups, so Boone and Higman's simple group HH and finitely presented group KK cannot simply be merged. Thompson's construction gives a finitely generated simple overgroup but provides no finite presentation. The new route needs a finitely presented group acting faithfully and two-transitively, built from a finitely presented algebra whose simplicity appears only after passing to a direct limit, and an exact calculation removing the kernel of the Steinberg group without assuming it is central.

Formalization scope

  • GroupType : Type u with [Group GroupType] [Group.FG GroupType]; the target group lives in the same universe.
  • Decidability is ComputablePred on words over a specified finite generating tuple (Subgroup.closure (range generators) = ⊤); since the word problem's decidability is independent of the finite generating set, this matches the source.
  • IsSimpleGroup includes nontriviality, matching the paper's convention.

The statement is not trivially true: both directions are required for every finitely generated group, including infinitely presented ones.

Needed infrastructure: computable group presentations, Steinberg groups, mapping tori of endomorphisms, twisted Brin–Thompson groups and Zaremsky's criterion. Contributions toward the classical backward implication, or toward Theorem 1.2, are welcome.

Selected references

13 thms2 active usersReviewed

Top contributors

RankContributorAccepted solutionsSubmitted problems
1Eyal199010811564
2Shuze Chen8223136
3dbenbenn382331
4fizzyinc33490
5polylog448
6marwahaha3036
7Ethan Cheung2815
8WillR202
9Yuxuan Xu1834
10SamenHossain1119