OAI Math

All of openAI's results.

317 missions

Missions

241–260 of 317

Algebra·Captain: marwahaha

Lech's multiplicity conjectureOpen Problem

Motivation

Multiplicity measures the growth of infinitesimal neighborhoods in a local ring. The manuscript addresses Lech’s flat-local-map inequality; the available formal target isolates its complete-domain Frobenius-complex component. The source is OpenAI's September 2026 manuscript.

Setting

For a local domain $D$ of dimension $d$ , Hilbert–Samuel multiplicity is the limit of $d!\,\ell(D/\mathfrak m^N)/N^d$ . A short complex has finite free terms in degrees $-d$ through zero, finite-length homology, and nonzero zeroth homology. Its Frobenius scalar extensions define a normalized Euler-characteristic sequence.

Formalization targets

a_n=p^{-nd}\chi(F_n)\longrightarrow\chi_\infty(F),\qquad e(D)\le\chi_\infty(F).

The defined proposition DuttaDomainClaim holds, in universe u. That claim says: let D be a commutative Noetherian local domain (in universe u) that is complete in the adic topology of its maximal ideal, with prime characteristic p, and let F be a cochain complex of D-modules indexed by the integers that is a short complex. Short means every term F^i is free and finitely generated, F^i is zero whenever i < -dim D or i > 0, every homology module of F has finite length, and the homology of F in degree 0 is nonzero. Here dim is the Krull dimension (taken as 0 if it is the bottom value). Let F_n denote F after extending scalars along the n-fold iterate of the Frobenius map of D. The conclusion has three parts. First, every homology module of every F_n has finite length. Second, the sequence a_n = p^(-n dim D) * chi(F_n) converges as n tends to infinity, where chi(G) is the alternating sum, over i from 0 to dim D, of (-1)^i times the length of the homology of G in degree -i; this limit is the Dutta multiplicity of F. Third, the Hilbert-Samuel multiplicity of D, defined as the limit of (dim D)! times the length of D/m^N divided by N^(dim D) as N tends to infinity, is at most the Dutta multiplicity of F.

The goal is OAI.Lech.dutta_domain.

Significance

The goal formalizes the lower bound by Dutta multiplicity together with the convergence and finite-length statements needed to interpret it. This is a precise component of the paper’s multiplicity program. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Lengths of homology after Frobenius extension must be controlled before normalized Euler characteristics can be used. A definition by a chosen limit does not by itself establish convergence.

Formalization scope

The ring is a complete Noetherian local domain in prime characteristic. The goal is DuttaDomainClaim, not the unrestricted flat local homomorphism inequality. Dimensions and lengths use the natural-number conversions in the supplied definitions, and convergence is an explicit conclusion.

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

Selected references

OpenAI, Lech's multiplicity conjecture, preprint, September 2026. Manuscript.
OpenAI, accompanying Lean statement. Pinned source.

2 thms1 active userReviewed

Completed

Algebra Group Theory·Captain: marwahaha

A Counterexample to Kaplansky's Direct-Finiteness Conjecture in Characteristic TwoOpen Problem

Motivation

Finite-dimensional linear algebra makes a one-sided inverse two-sided. The source asks whether finite support in a group algebra can replace finite dimension and presents a characteristic-two counterexample. The source is OpenAI's September 2026 manuscript.

Setting

The group algebra $K[G]$ consists of finitely supported functions on a group with convolution multiplication. A ring is directly finite if $ab=1$ always implies $ba=1$ .

Formalization targets

\exists K,G,a,b:\quad\operatorname{char}K=2,\quad |K|<\infty,\quad G\text{ finitely presented},\quad ab=1\ne ba.

There exist a finite field K of characteristic 2 and a finitely presented group G such that G contains an element g of odd prime order ℓ (that is, orderOf g = ℓ with ℓ prime and odd), and the group algebra K[G] (the monoid algebra of G over K) contains elements a_out and b_out with a_out · b_out = 1 but b_out · a_out ≠ 1. Thus K[G] fails to be directly finite, giving a counterexample to direct finiteness. The statement is existential: it does not name a specific K, G, or prime ℓ, and the proof is admitted in the source.

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

main theorem.

Significance

The selected statement includes finite presentation and an element of odd prime order in the group. The weaker finitely generated formulation is included as a separate supporting target. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

A matrix counterexample does not automatically provide scalar elements in a group algebra. The formal target requires genuine finitely supported scalar elements and verification of both products.

Formalization scope

The field and group are existentially quantified, with the finite-field, characteristic, and finite-presentation structures carried explicitly. No claim that the field is exactly the two-element field is made. Odd-prime torsion is part of the conclusion.

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

Selected references

OpenAI, A Counterexample to Kaplansky's Direct-Finiteness Conjecture in Characteristic Two, preprint, September 2026. Manuscript.
OpenAI, accompanying Lean statement. Pinned source.

6 thms2 active usersReviewed

Completed

Algebra Functional Analysis·Captain: marwahaha

A Counterexample to the Group-Ring Determinant ConjectureOpen Problem

Motivation

The determinant of a nonsingular integer matrix has absolute value at least one. The source examines the proposed counterpart for integer matrices over group rings, where the determinant is defined by an operator trace. The source is OpenAI's September 2026 manuscript.

Setting

The left regular operator associated to a group-ring matrix acts on $\ell^2(G)^n$ by finite convolution. Its Fuglede–Kadison determinant in the invertible case is the exponential of half the real trace of the logarithm of its positive square.

Formalization targets

\exists A\in M_n(\mathbb Z[G]),\quad A\text{ invertible over }\mathbb Q[G],\quad 0<\det_{\mathcal N(G)}(T_A)<1.

The defined proposition MainStatement holds, i.e. there exist a group G that is finitely generated, an integer n ≥ 1, an n×n matrix A with entries in the integral group ring ℤ[G], and a bounded ℂ-linear operator T on the Hilbert space l²(G)^n (square-summable complex functions on Fin n × G) such that four conditions hold. First, the image of A in the rational group ring ℚ[G] (obtained by applying the integer-to-rational map to every coefficient) is an invertible matrix over ℚ[G]. Second, T is exactly the left-regular operator of A, meaning (Tξ)(i,h) = Σ_j Σ_g a_{ij}(g) ξ(j, g⁻¹h), where a_{ij}(g) ∈ ℤ is the coefficient of g in the entry A_{ij}. Third, T is invertible as a bounded operator on l²(G)^n. Fourth, its Fuglede–Kadison determinant fkDet(T) = exp(Re tr(log(T*T))/2) satisfies 0 < fkDet(T) < 1, where tr(S) = Σ_i ⟨e_i, S e_i⟩ is the unnormalized trace summing over the basis vectors e_i supported at the identity element of G in component i, and log is the continuous functional calculus logarithm.

The goal is OAI.GroupRingDeterminant.main.

Significance

The goal gives a square-matrix obstruction with both a rational group-ring inverse and a bounded operator inverse. This keeps the logarithm in the invertible setting. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

The trace logarithm is not an ordinary finite-dimensional determinant polynomial. The algebraic matrix and bounded regular operator must be shown to match exactly before the determinant estimate is meaningful.

Formalization scope

The group is finitely generated and $n\ge1$ . Lean uses complex square-summable functions on Fin n × G, the unnormalized matrix trace, and continuous functional calculus for the logarithm. Invertibility is explicit on both the rational matrix and the operator.

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

Selected references

OpenAI, A Counterexample to the Group-Ring Determinant Conjecture, preprint, September 2026. Manuscript.
OpenAI, accompanying Lean statement. Pinned source.

5 thms2 active usersReviewed

Completed

Algebra Group Theory·Captain: marwahaha

A Counterexample to Kaplansky's Direct-Finiteness Conjecture in Odd CharacteristicOpen Problem

Motivation

The odd-characteristic version of direct finiteness has different coefficient constraints from the binary case. The source fixes one odd prime and links a group-algebra counterexample to a cellular automaton. The source is OpenAI's September 2026 manuscript.

Setting

For a finitely supported coefficient function $b$ on a group, the cellular map sends a configuration $x:G\to K$ to $g\mapsto\sum_u b(u)x(gu)$ . The prime is the smallest prime factor of $(m!)^2+1$ , where $m$ is a fixed central binomial coefficient.

Formalization targets

p=\min\operatorname{PrimeDiv}\!\left((\binom{1200}{600}!)^2+1\right),\quad |K|=p^4,\quad ab=1\ne ba,\quad \operatorname{cellular}(b)\text{ injective and not surjective}.

The defined proposition MainClaim holds. Here sourceM is the central binomial coefficient C(1200,600), and sourcePrime is the smallest prime factor of (sourceM!)²+1. MainClaim asserts that this number p is prime and odd, and that there exist a finite field K of characteristic p with exactly p⁴ elements and a finitely generated group G containing a nontrivial element of finite order, together with two elements a and b of the group algebra K[G] such that ab = 1 but ba ≠ 1. Moreover, for the map cellular(b) sending x : G → K to g ↦ Σ_u b(u)·x(g·u), the sum running over the support of b, this map is injective but not surjective. The formal statement is admitted in the source rather than proved here.

The goal is OAI.OddKaplansky.main_theorem.

Significance

The conclusion combines a scalar one-sided inverse with failure of surjectivity of a finite-memory linear map. It specifies the characteristic and field size without claiming the construction works at every odd prime. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

The group must retain nontrivial torsion while supporting the required finite sums. Matrix-level relations and an arbitrary choice of characteristic do not meet this target.

Formalization scope

The goal unfolds MainClaim. It proves primality and oddness of the fixed sourcePrime, then existentially supplies the finite field, finitely generated group, nontrivial finite-order element, and algebra elements. The cellular convention uses right-translated inputs $gu$ .

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

Selected references

OpenAI, A Counterexample to Kaplansky's Direct-Finiteness Conjecture in Odd Characteristic, preprint, September 2026. Manuscript.
OpenAI, accompanying Lean statement. Pinned source.

2 thms2 active usersReviewed

Completed

Algebra Mathematical Logic·Captain: marwahaha

Finite congruence lattices: characterization and undecidabilityOpen Problem

Motivation

A finite algebra has a lattice of congruences, ordered by inclusion. The source studies which finite lattices arise in this way, and the available goal captures its colored-graph characterization. The source is OpenAI's September 2026 manuscript.

Setting

A congruence is an equivalence relation preserved by every basic operation of an algebra. A graph witness assigns lattice-valued colors to pairs of finitely many vertices, with symmetry, diagonal, triangle, separation, and seed-connectivity conditions.

Formalization targets

\operatorname{Representable}(L)\quad\Longleftrightarrow\quad\operatorname{HasGraphWitness}(L).

For any finite type Lat carrying a lattice structure with a least element ⊥, Lat is Representable if and only if it HasGraphWitness. Representable means that there is a positive size n and an algebra on Fin n (a finite list of operations, each of some finite arity, acting on the carrier) such that Lat is order-isomorphic to the poset of congruences of that algebra, where a congruence is an equivalence relation compatible with every operation: if corresponding arguments are related coordinatewise, the outputs are related; congruences are ordered by the inherited order on equivalence relations. HasGraphWitness means that there is a positive size n and a Lat-valued coloring color of ordered pairs from Fin n satisfying five conditions: color is symmetric; color(a,b)=⊥ exactly when a=b; color(a,b) ≤ color(a,m) ⊔ color(m,b) for all a, b, m; whenever lower ≰ upper in Lat, some pair has color ≤ lower but not ≤ upper; and for every nonempty finite set of seed pairs, any pair whose color is at most the join of the seed colors is connected to the seeds. Connected is the equivalence closure of the relation Marked, where a,b are Marked if some self-map p of the vertices satisfies color(p x,p y) ≤ color(x,y) for all x,y and sends some seed pair (s,t) to (a,b).

The goal is OAI.FiniteCongruence.graph_criterion.

Significance

The equivalence provides a finite combinatorial certificate for representation as an entire congruence lattice. It is the characterization component of the manuscript. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Representing a lattice inside a congruence lattice is weaker than obtaining all congruences. The witness’s seed-connectivity condition must capture this fullness and work in both directions.

Formalization scope

The lattice is finite and has a least element. The algebra carrier and graph witness carrier each have positive finite size. Operations have finite arities, and representation is an order isomorphism. The manuscript’s undecidability conclusions are not among the attached targets.

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

Selected references

OpenAI, Finite congruence lattices: characterization and undecidability, preprint, September 2026. Manuscript.
OpenAI, accompanying Lean statement. Pinned source.

2 thms2 active usersReviewed

Analysis Probability·Captain: marwahaha

Strict convexity and differentiability of the planar exponential first-passage limit shapeOpen Problem

Motivation

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

Setting

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

Formalization targets

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

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

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

gamma differentiability.

Significance

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

Difficulty

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

Formalization scope

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

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

Selected references

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

8 thms2 active usersReviewed

Graph Theory Probability·Captain: marwahaha

Nonuniqueness of percolation on nonamenable quasi-transitive graphsOpen Problem

Motivation

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

Setting

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

Formalization targets

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

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

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

Significance

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

Difficulty

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

Formalization scope

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

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

Selected references

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

6 thms1 active userReviewed

Completed

Mathematical Physics Probability·Captain: marwahaha

Buffered comparison and stopping-band resolution in critical IsingOpen Problem

Motivation

Conditioning on an explored Ising interface fixes many spins and can create alternating signs. The source develops comparison estimates that remain valid with arbitrary common pinned spins. The source is OpenAI's September 2026 manuscript.

Setting

A ferromagnetic Ising law weights sign configurations by the exponential of nonnegative pair couplings plus real external fields. Two probability mixtures prescribe source spins on $J$ , while the same spins are pinned on $F$ and a target event is prescribed on $I$ .

Formalization targets

e^{-4\operatorname{artanh}q_0}\le\frac{\mu_{\mathrm{mix}}(\sigma_I=a\mid\sigma_F=\tau)}{\mu_{\mathrm{mix}'}(\\sigma_I=a\\mid\\sigma_F=\\tau)}\\le e^{4\\operatorname{artanh}q_0}.

A comparison bound for a ferromagnetic Ising model on a finite graph with n vertices and m separately indexed edges (parallel edges allowed, no loops, nonnegative couplings K_e) and an arbitrary real external field h. A configuration σ has energy equal to the sum over edges of K_e σ_u σ_v plus the sum over vertices of h_v σ_v, with spins ±1, and weight exp(energy). Take pairwise disjoint vertex sets I, J, F, and kept vertices i ∈ I and j ∈ J that lie outside F. Fix spin configurations a and τ. For a configuration b, the conditional probability of σ_I = a given σ_J = b and σ_F = τ is the ratio of the total weight of configurations satisfying all three agreements to the total weight of those agreeing with b on J and τ on F. For any two probability mixtures mix and mix' on configurations (nonnegative weights summing to 1), the mixture probability is the mix-weighted average of these conditional probabilities over b; only the restriction of b to J matters. Let q be the terminal connection probability in the zero-field random-cluster (FK) model with q=2 on the graph with F deleted (not pinned): edges e are open with probability 1-exp(-2K_e), the vertices of I are identified together and those of J are identified together, and q is the probability that i and j lie in the same cluster. Then the ratio of the mixture probability under mix to that under mix' lies between exp(-4 artanh q) and exp(4 artanh q), for every such pair of mixtures, uniformly in h, a and τ. The theorem is stated with its proof admitted (sorry).

The goal is OAI.BufferedIsing.finite_graph_comparison.

Significance

The estimate controls likelihood ratios uniformly over mixtures, fields, and common signs. It is the finite-graph comparison component of the manuscript. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Pinning a vertex changes neighboring fields; deleting it does something different. The comparison probability must come from the graph with the common pins deleted, with each terminal class contracted separately.

Formalization scope

The graph is finite with indexed edges, allowing parallel edges and excluding loops before contraction. The sets $I,J,F$ are pairwise disjoint and each terminal class contains a supplied vertex. The zero-field random-cluster weight has cluster parameter two. The stopping-band approximation theorem is not an attached target.

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

Selected references

OpenAI, Buffered comparison and stopping-band resolution in critical Ising, preprint, September 2026. Manuscript.
OpenAI, accompanying Lean statement. Pinned source.

28 thms2 active usersReviewed

Completed

Probability Stochastic Systems·Captain: marwahaha

A directional zero–one law under strict ellipticityOpen Problem

Motivation

A random environment can favor different directions at different sites. The source asks whether escape in one prescribed real direction can have an intermediate probability after averaging over the environment. The source is OpenAI's September 2026 manuscript.

Setting

A transition row assigns probabilities to the nearest-neighbor steps of the integer lattice. Rows at different sites are independent and have the same law. Strict ellipticity means every step probability is positive almost surely, without a common positive lower bound.

Formalization targets

\mathbb P_0\!\left(\langle X_n,\ell\rangle\to+\infty\right)\in\{0,1\}\qquad(d\ge3,\ \ell\ne0).

For every dimension d ≥ 3, a random walk in an i.i.d. random environment on the lattice ℤ^d obeys a directional zero-one law. Here a row at a site is a probability vector p on the 2d nearest-neighbour steps (coordinate direction i in Fin d, sign + or −), with each p(e) in [0,1] and the entries summing to 1. The environment assigns an independent row to every site, each drawn from a probability measure μ on rows, and the strict ellipticity hypothesis on μ says that μ-almost every row gives every one of the 2d steps strictly positive probability. Given the environment, the walker at site x moves to x plus the unit vector of step e with probability p_x(e); the annealed law of the path started at 0 averages over both the environment and the walk. For any nonzero real vector ℓ in ℝ^d, the escape event is that the path X satisfies Σᵢ Xₙ(i)·ℓᵢ → +∞ as n → ∞, that is, the walk tends to infinity in the direction ℓ. The conclusion is that the annealed probability of this event, starting from 0, is either exactly 0 or exactly 1.

The goal is OAI.DirectionalZeroOne.directional_zero_one.

Significance

The target gives a directional zero–one law under positivity alone. It makes no moment or uniform ellipticity assumption. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Revisiting sites reuses the same random transition row, so path increments are not independent under the averaged law. Ordinary zero–one laws for independent increments do not directly apply.

Formalization scope

Lean builds the annealed path measure through a Markov kernel on environment-position pairs. The starting site is the origin, the direction is any nonzero real vector, and escape means the scalar projection tends to positive infinity.

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

Selected references

OpenAI, A directional zero–one law under strict ellipticity, preprint, September 2026. Manuscript.
OpenAI, accompanying Lean statement. Pinned source.

2 thms2 active usersReviewed

Probability Stochastic Systems·Captain: marwahaha

Directional transience implies ballisticityOpen Problem

Motivation

Escape to infinity can be arbitrarily slow for a general stochastic process. The source asks whether independent uniformly elliptic lattice environments force a positive deterministic speed whenever a direction is transient. The source is OpenAI's September 2026 manuscript.

Setting

Uniform ellipticity provides one positive lower bound for all step probabilities, almost surely at every site. Directional transience means the position projected onto a fixed unit vector tends to positive infinity almost surely under the law averaging environment and walk.

Formalization targets

\langle X_n,\ell\rangle\to+\infty\ \text{a.s.}\quad\Longrightarrow\quad\exists v:\ X_n/n\to v\ \text{a.s.},\quad\langle v,\ell\rangle>0.

The theorem (admitted, not proved here) states that, for every dimension d ≥ 2 and every Borel probability measure ν on the set of transition rows (a row is a probability vector p over the 2d nearest-neighbour directions ±e_i of ℤ^d, with entries nonnegative and summing to 1), the following holds. Suppose ν is uniformly elliptic, meaning there is κ > 0 with p(e) ≥ κ for every direction e, for ν-almost every row p. Let ℓ be a unit vector in ℝ^d (ℓ·ℓ = 1), and suppose the walk is directionally transient in direction ℓ. Here the environment assigns to each site of ℤ^d an independent ν-distributed row, the walk starts at the origin and at each step moves from its current site x in direction e with probability given by the row at x, and the annealed law averages over the environment and the walk. Directional transience means that, almost surely under this annealed law, the inner product of the walk position X_n with ℓ tends to +∞ as n → ∞. The conclusion is that there exists a vector v ∈ ℝ^d with v·ℓ > 0 such that the walk has asymptotic velocity v, that is, X_n/n → v as n → ∞ almost surely under the annealed law. In other words, directional transience of an i.i.d. uniformly elliptic random walk in random environment in dimension at least two implies ballisticity with a nonzero velocity having positive component along ℓ.

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

positive probability transience velocity hemisphere.

Significance

The chosen central target converts almost-sure transience to a velocity statement in every dimension at least two. The separate dimension-at-least-three statement starts from positive probability and identifies the transient hemisphere. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Transience controls eventual direction but not the time spent in traps. A law of large numbers with positive projected velocity needs quantitative control of these delays.

Formalization scope

The main statement assumes $d\ge2$ , a unit direction, and an independent identically distributed uniformly elliptic environment. The supporting hemisphere target assumes $d\ge3$ and a nonzero direction. Their original definition groups stay separate.

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

Selected references

OpenAI, Directional transience implies ballisticity, preprint, September 2026. Manuscript.
OpenAI, accompanying Lean statement. Pinned source.

6 thms2 active usersReviewed

Mathematical Physics Probability·Captain: marwahaha

The Mézard–Parisi formula for diluted spin glassesOpen Problem

Motivation

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

Setting

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

Formalization targets

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

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

The goal is OAI.DilutedSpinGlass.mezard_parisi.

Significance

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

Difficulty

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

Formalization scope

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

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

Selected references

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

2 thms1 active userReviewed

Mathematical Physics Probability·Captain: marwahaha

The free energy of the Ising random perceptronOpen Problem

Motivation

The Ising perceptron weights binary configurations by their projections onto random patterns. The paper develops a variational description of its pressure; the available formal target checks that the proposed variational value is finite. The source is OpenAI's September 2026 manuscript.

Setting

An overlap path is an almost-everywhere class on $(0,1)$ with a monotone representative taking values in $[0,1]$ . The variational expression combines a Gaussian pattern functional with an Ising entropy, defined as a supremum over monotone nonnegative field steps.

Formalization targets

\alpha\ge0,\quad f\in C_b(\mathbb R)\quad\Longrightarrow\quad\exists p\in\mathbb R:\ \operatorname{variationalValue}(\alpha,f)=p\text{ in }\overline{\mathbb R}.

For every real α ≥ 0 and every continuous function f : ℝ → ℝ that is bounded (there is K with |f(x)| ≤ K for all x), the variational value of the Ising perceptron model is a finite real number, i.e. variationalValue(α,f) equals the extended real (p : EReal) for some real p. Here variationalValue(α,f) is the infimum, over all admissible overlap paths q (almost-everywhere-defined functions on (0,1) that agree a.e. with a monotone function taking values in [0,1]), of α times the pattern functional of f at q plus the Ising entropy of q. The pattern functional is the limit as n→∞ of uniformPattern, a nested Gaussian transform over a uniform grid with n+1 cells built from cell averages of q and applied to f at 0, where each transform is either a Gaussian average or a log-exponential-moment average divided by d, depending on whether d is zero. The Ising entropy is the supremum, over field steps (a partition of [0,1] with nonnegative monotone step values), of the field recursion value plus half the integral of the step function against q. The statement asserts that this infimum is neither +∞ nor −∞.

The goal is OAI.IsingPerceptron.variationalValue_real_of_continuous.

Significance

The goal rules out both infinite extended-real values for continuous bounded potentials. This is a well-definedness component needed before a real-valued limit formula can be used. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

The entropy is a supremum over an unbounded family of fields and the outer expression is an infimum over paths. Boundedness of the input potential alone does not syntactically make this extended-real expression finite.

Formalization scope

The target is variationalValue_real_of_continuous, with nonnegative density and continuous bounded potential. It does not assert convergence of finite-system pressure or the manuscript’s broader bounded-Borel result. Gaussian recursion and almost-everywhere path conventions are kept as published.

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

Selected references

OpenAI, The free energy of the Ising random perceptron, preprint, September 2026. Manuscript.
OpenAI, accompanying Lean statement. Pinned source.

2 thms1 active userReviewed

Mathematical Physics Probability·Captain: marwahaha

The free energy of the spherical random perceptronOpen Problem

Motivation

The spherical perceptron assigns random rewards to vectors of fixed length. The source asks for an exact pressure formula without a convexity or symmetry condition on the single-pattern potential. The source is OpenAI's September 2026 manuscript.

Setting

Configurations lie on the sphere of radius $\sqrt n$ , equipped with uniform probability measure. There are $\lfloor\alpha n\rfloor$ independent Gaussian patterns. The variational value minimizes a Brownian stochastic-control functional plus an extended nonnegative entropy over monotone trials.

Formalization targets

\exists p\in\mathbb R:\quad\mathcal V(\alpha,\beta,\varphi)=p,\qquad\mathbb E p_n\to p,\qquad p_n\xrightarrow{\mathbb P}p.

For a probability measure P on continuous paths ℝ≥0→ℝ under which the evaluation process is a real Brownian motion, and for parameters α>0, β>0 and a bounded continuous function φ:ℝ→ℝ, there is a real number p with three properties. First, the variational value equals p (as an extended real). That value is the infimum over all trials m of α times the control value of βφ at m, plus the entropy of m. A trial is a nondecreasing measurable function m:[0,1]→[0,1]. Its entropy is one half of the integral over t of 1/∫ₜ¹ m(s)ds minus 1/(1−t), taken in [0,∞]. The control value of f at m is the supremum, over progressively measurable controls v with finite cost E∫ m(t)v(t)²dt, of E f(B₁+∫₀¹ m(t)v(t)dt) minus half that cost. Second, the expected spherical-perceptron pressure E[pressure(N+1)] converges to p as N→∞. For dimension n, pressure is (1/n) log ∫ exp(β Σₐ φ(⟨gₐ,x⟩/√n)) dx, with x uniform on the sphere of radius √n in ℝⁿ. The gₐ are the rows of a pattern matrix with ⌊αn⌋ rows and n i.i.d. standard Gaussian entries per row. Third, the pressure concentrates: for every ε>0, the Gaussian probability that |pressure(N+1)−p|>ε tends to 0 as N→∞.

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

spherical linear field formula.

Significance

The selected main target proves finiteness of the variational value, convergence of expected pressure, and concentration around the same number. The linear-field formula is attached as a supporting result. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

An infimum involving a possibly infinite entropy must be connected with the actual finite-dimensional spherical integral. The potential is only bounded and continuous, so smoothness cannot be assumed.

Formalization scope

Density and inverse temperature are strictly positive. Controls are progressively measurable for the stated Brownian filtration and have finite cost. Dimension is written as $N+1$ to stay positive. The Brownian and cascade-based linear-field definition groups are independent references.

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

Selected references

OpenAI, The free energy of the spherical random perceptron, preprint, September 2026. Manuscript.
OpenAI, accompanying Lean statement. Pinned source.

4 thms1 active userReviewed

Markov Chain Probability·Captain: marwahaha

Cutoff throughout the high-temperature Sherrington–Kirkpatrick phaseOpen Problem

Motivation

Cutoff means that a Markov chain’s transition from far from equilibrium to near equilibrium occurs in a negligible fraction of its mixing time. The source studies heat-bath dynamics for a disordered mean-field Ising model. The source is OpenAI's September 2026 manuscript.

Setting

The Sherrington–Kirkpatrick model has independent centered Gaussian pair couplings with variance $\beta^2/n$ and zero external field. One discrete update picks a site uniformly and resamples its spin from its conditional Gibbs law. Mixing time uses worst-case total variation distance.

Formalization targets

\mathbb P_g\!\left(\frac{t_{\mathrm{mix}}(g,\varepsilon)}{t_{\mathrm{mix}}(g,1-\varepsilon)}>1+\eta\right)\to0\qquad(0\le\beta<1/2,\ 0<\varepsilon<1/2,\ \eta>0).

For real parameters β with 0 ≤ β < 1/2, ε with 0 < ε < 1/2, and η > 0, two things hold for the Sherrington–Kirkpatrick model with n spins, where a disorder g is a real coupling for each pair i < j of sites and the Gibbs measure at zero external field has weight proportional to exp((1/2) Σᵢ Σⱼ σᵢ gᵢⱼ σⱼ) on spin configurations σ ∈ {±1}ⁿ (couplings symmetrized, diagonal zero). The dynamics is a heat-bath single-site chain: choose a site uniformly at random, then keep or flip its spin with probabilities proportional to the Gibbs masses of the two configurations (for n = 0 the transition matrix is the identity). The distance after k steps is the maximum over starting configurations of the total variation distance (half the ℓ¹ distance) between the k-step distribution and the Gibbs measure, and mixingTime(g, δ) is the least k whose distance is at most δ (the infimum of the set, so 0 if that set is empty). The disorder law makes the couplings independent centered Gaussians with variance β²/n. First, the probability under this law that the ratio mixingTime(g, ε) / mixingTime(g, 1 − ε) exceeds 1 + η tends to 0 as n → ∞. Second, for all sufficiently large n, every disorder g satisfies mixingTime(g, 1 − ε) > 0.

The goal is OAI.SKRatio.ratio_cutoff.

Significance

The available target gives ratio cutoff in probability over the disorder and eventual positivity of the denominator for every disorder. It isolates a precise mixing-time comparison. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Fast relaxation estimates alone do not prove that all fixed total-variation thresholds become asymptotically equivalent. The worst starting configuration and the random couplings both enter the comparison.

Formalization scope

The attached range is $0\le\beta<1/2$ , narrower than the full high-temperature range discussed in the manuscript. The target does not specify the cutoff location. Dynamics is discrete single-site updating; the exceptional $n=0$ transition is the identity.

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

Selected references

OpenAI, Cutoff throughout the high-temperature Sherrington–Kirkpatrick phase, preprint, September 2026. Manuscript.
OpenAI, accompanying Lean statement. Pinned source.

2 thms1 active userReviewed

Completed

Information Theory Probability·Captain: marwahaha

The exact reconstruction threshold for the three-state symmetric channelOpen Problem

Motivation

Broadcasting a label through noisy tree edges models how information decays with distance. The source studies when observations far from the root retain information about its three-state label. The source is OpenAI's September 2026 manuscript.

Setting

The symmetric channel preserves the input with probability $(1+2\lambda)/3$ and sends it to each other state with probability $(1-\lambda)/3$ . Reconstruction advantage is the expected total variation between the posterior root law and the uniform prior.

Formalization targets

b\ge2,\quad-1/2\le\lambda\le1,\quad b\lambda^2>1\quad\Longrightarrow\quad\operatorname{Advantage}_n\to L>0.

For every natural number b ≥ 2 and every real λ that is admissible, meaning −1/2 ≤ λ ≤ 1, if b·λ² > 1 then the sequence of regular-tree advantages reconstructs. Here a three-state spin (an element of Fin 3) is passed through a symmetric channel that keeps the spin with probability (1+2λ)/3 and moves to each other spin with probability (1−λ)/3. The observation at depth 0 is the root spin, and the observation at depth n+1 is a multiset of depth-n observations, one for each of the offspring of the root, where the offspring count is the constant b (the regular case) and each child spin is obtained by passing the parent spin through the channel and then observed recursively. With a uniformly random root spin, the posterior of each spin given an observation is its conditional probability, defaulting to 1/3 when the observation has probability zero. The advantage of a family of laws indexed by the root spin is the sum over observations y of the marginal probability of y times half the sum over spins i of |posterior(y,i) − 1/3|. The regular advantage at depth n is this advantage for the regular b-ary observation law. Reconstructs means that this sequence in n converges to some limit L > 0. The statement is an admitted theorem, with its proof left as sorry.

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

Significance

The selected goal is the regular-tree supercritical direction. Supporting published targets give Poisson reconstruction and equivalent supercritical formulations in a second definition group. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

The observation contains the full nested collection of descendants, and the posterior depends on correlated information inherited from their common ancestor. A single root-to-leaf correlation is insufficient to describe reconstruction.

Formalization scope

Observations are nested multisets with a uniform three-state root. The attached targets establish reconstruction above the displayed threshold; non-reconstruction at or below equality and stochastic-block-model recovery are outside this draft’s formal scope.

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

Selected references

OpenAI, The exact reconstruction threshold for the three-state symmetric channel, preprint, September 2026. Manuscript.
OpenAI, accompanying Lean statement. Pinned source.

48 thms2 active usersReviewed

Analysis Probability·Captain: marwahaha

An explicit exact Hausdorff gauge for SLEOpen Problem

Motivation

Hausdorff dimension identifies a critical power of scale but need not give a positive measure at that power. The source proposes an iterated-logarithm correction for ordinary chordal SLE curves. The source is OpenAI's September 2026 manuscript.

Setting

A Hausdorff gauge is continuous, nondecreasing on nonnegative radii, zero at zero, and positive at positive radii. Its metric measure charges a covering set according to its diameter. Chordal SLE is represented by a capacity-two Loewner trace driven by scaled Brownian motion.

Formalization targets

h(r)=r^{1+\kappa/8}\bigl(\log\log(1/r)\bigr)^{(1-\kappa/8)/2}\quad\text{for small }r>0,\qquad\mathcal H^h(\gamma([s,t]))>0\quad(0<s<t).

For every probability space (Ω, P) and every κ with 0<κ<8, if γ is an ordinary chordal SLE_κ family of curves on Ω, then almost surely the explicit Hausdorff gauge measure of every positive-time segment of the curve is positive. Here γ being an ordinary chordal SLE_κ means that each γ(ω,t) is measurable in ω and that there is a standard real Brownian motion B on (Ω,P) such that, for almost every ω, the curve t↦γ(ω,t)∈ℂ with driving function U(t)=√κ·B_t(ω) is a capacity-two trace: γ is continuous, starts at 0, stays in the closed upper half-plane, and there are conformal-type maps G_t from the unbounded component of the upper half-plane minus γ[0,t] to the upper half-plane and inverse maps F_t back, holomorphic, mutually inverse, with G_0 the identity, satisfying the Loewner equation ∂_t G_t(z)=2/(G_t(z)−U(t)) (one-sided at t=0), the normalization z(G_t(z)−z)→2t as z→∞, and F_t(U(t)+iy)→γ(t) as y→0⁺. The gauge h:ℝ→ℝ is any function that is continuous, nondecreasing on [0,∞), zero at 0 and positive for r>0, and that coincides, for all sufficiently small r>0, with r^{1+κ/8}·(log log(1/r))^{(1−κ/8)/2}. The gauge measure is the Hausdorff-type metric measure on ℂ built from r↦h(r) (with the ENNReal-valued radius cast through its real part). The conclusion is that, for almost every ω, simultaneously for all times 0<s<t, this measure of the image set γ(ω)([s,t]) is strictly positive.

The goal is OAI.SLEExactGauge.sourceLowerMain_proved.

Significance

The formal goal establishes simultaneous positivity for every nontrivial positive-time compact segment. It is the lower-positivity component of the manuscript’s exact-gauge claim. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

A dimension statement only determines a critical exponent; it does not decide the effect of a slowly varying correction. Positivity must hold for all segment times on one probability-one event.

Formalization scope

The parameter satisfies $0<\kappa<8$ . The goal does not assert finite measure, finite expected disk mass, or non-sigma-finiteness for a different gauge. The name sourceLowerMain_proved is a declaration name; its current theorem status is Open.

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

Selected references

OpenAI, An explicit exact Hausdorff gauge for SLE, preprint, September 2026. Manuscript.
OpenAI, accompanying Lean statement. Pinned source.

2 thms1 active userReviewed

Mathematical Physics Probability Random Matrix Theory·Captain: marwahaha

All-temperature pressure for orthogonally invariant Ising spin glassesOpen Problem

Motivation

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

Setting

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

Formalization targets

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

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

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

Significance

The selected goal is the all-positive-temperature zero-field pressure theorem. The attached results also cover field laws, random spectra, Gaussian-pattern pressure and ground energy, and related norm limits under their stated assumptions. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

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

Formalization scope

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

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

Selected references

OpenAI, All-temperature pressure for orthogonally invariant Ising spin glasses, preprint, September 2026. Manuscript.
OpenAI, accompanying Lean statement. Pinned source.

12 thms1 active userReviewed

Completed

Combinatorics Probability·Captain: marwahaha

Polynomial vacuum representations and bridge mass for honeycomb walksOpen Problem

Motivation

Critical self-avoiding walks have weights balanced between exponential path growth and decay. The source studies bridge-length scaling; the available target establishes summability of the bridge sums used to define these quantities. The source is OpenAI's September 2026 manuscript.

Setting

A honeycomb bridge is a self-avoiding vertex list crossing a strip from a fixed initial port to any terminal port on the opposite layer. A path with $L$ vertices has critical weight $\lambda^L$ , with $\lambda=(2\cos(\pi/8))^{-1}$ .

Formalization targets

\sum_{\gamma}w(\gamma)<\infty,\qquad\sum_{\gamma}L(\gamma)w(\gamma)<\infty\qquad(h\ge1),

For every integer h ≥ 1, six families of sums over self-avoiding bridge paths in a honeycomb strip are absolutely summable. Vertices of the honeycomb lattice are of two kinds, up(i,j) and down(i,j) with integer i and j, and the layer of a vertex is its second index j; an up vertex (i,j) is adjacent to the down vertices (i,j−1), (i,j) and (i−1,j), and adjacency is symmetric. A bridge path of height h is a list of distinct vertices, consecutive ones adjacent, starting at up(0,0), ending at some down(i,h−1), with every vertex in layers 0 through h−1. Its weight is λ^L, where L is the number of vertices and λ = 1/(2cos(π/8)) is the critical activity, and its first-length weight is L·λ^L. Let bridgeMass(h) be the total weight of all bridge paths. A path is confined if every vertex has horizontal coordinate (i + j/2 for up vertices, i + j/2 + 1/2 for down vertices) of absolute value at most h(log h)², and confinedMass(h) is the total weight of confined paths. The theorem asserts summability over all bridge paths of the weight, of the first-length weight, and of the first-length weight divided by bridgeMass(h), and summability over confined paths of the weight, of the first-length weight, and of the first-length weight divided by confinedMass(h). The proof is admitted in the source, not established here.

The goal is OAI.PolynomialVacuumBridge.Corridor.finite_bridge_sums.

Significance

The full formal statement gives six summability assertions, including normalized first-length weights and their corridor-confined counterparts. These are prerequisites for interpreting bridge masses and mean lengths. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Each strip has unbounded horizontal extent and admits paths of arbitrarily large length. Finite strip height therefore does not by itself make the path family finite.

Formalization scope

The length convention counts vertices. Confinement means horizontal coordinate bounded by $h(\log h)^2$ . The target proves summability, without asserting the manuscript’s $h^{4/3+o(1)}$ asymptotic law. Normalized terms use the masses defined by tsum.

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

Selected references

OpenAI, Polynomial vacuum representations and bridge mass for honeycomb walks, preprint, September 2026. Manuscript.
OpenAI, accompanying Lean statement. Pinned source.

43 thms3 active usersReviewed

Completed

Combinatorics Probability·Captain: marwahaha

Renewal and changes of law for critical honeycomb walksOpen Problem

Motivation

An external force rewards self-avoiding walks whose endpoints move in a chosen direction. The source studies critical honeycomb scaling; the available formal goal supplies existence of the forced free-energy limit. The source is OpenAI's September 2026 manuscript.

Setting

For an $n$ -step self-avoiding walk, the endpoint displacement is embedded in the complex plane. Its projection onto $e$ is the real part of $\overline e$ times that displacement. The partition sum weights the walk by critical activity to the $n$ th power and an exponential force reward.

Formalization targets

\frac1n\log\!\sum_{\gamma\in\operatorname{SAW}_n(o)}\rho^n e^{s\operatorname{Re}(\overline e\,\Delta\gamma)}\longrightarrow F(o,e,s),\qquad\rho=(2+\sqrt2)^{-1/2}.

For every starting vertex o of the honeycomb lattice, every complex number e and every real number s, the sequence logPartition(o,e,s)(n) converges as n tends to infinity to freeEnergy(o,e,s). Here vertices are triangular-up or triangular-down sites labeled by integer column and row, each up vertex being adjacent to three down vertices and vice versa, with planar positions given in the complex plane. saws(o,n) is the set of self-avoiding walks of n steps from o, meaning vertex lists with no repetition. For such a walk γ, its displacement is the position of its endpoint minus the position of o, and its projection onto e is the real part of conj(e) times the displacement. The partition function is the sum over γ in saws(o,n) of ρ^n exp(s times that projection), with ρ = 1/√(2+√2). logPartition is log of this partition function divided by n, and freeEnergy is defined as the limit of logPartition at infinity, using Lean's limUnder convention. The statement therefore asserts that this limit exists and equals freeEnergy; it is a stated theorem whose proof is admitted in the source.

The goal is OAI.HoneycombForce.logPartition_tendsto.

Significance

The conclusion makes the defined free energy an actual convergent limit for every starting point, direction parameter, and real force. It establishes the thermodynamic quantity underlying later asymptotic questions. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Finite sums at each length do not guarantee convergence after normalization. Self-avoidance couples concatenated pieces, so ordinary independent-product arguments are unavailable without additional work.

Formalization scope

The target allows any complex $e$ and real $s$ , without a unit-direction restriction. Length counts steps, and walk lists contain $n+1$ distinct vertices. The spatial exponent, thermal laws, and small-force exponent from the manuscript are not attached conclusions.

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

Selected references

OpenAI, Renewal and changes of law for critical honeycomb walks, preprint, September 2026. Manuscript.
OpenAI, accompanying Lean statement. Pinned source.

4 thms2 active usersReviewed

Completed

Probability Representation Theory·Captain: marwahaha

Optimal-order mixing of the Thorp shuffleOpen Problem

Motivation

The full permutation of a deck can remain far from uniform after each individual card is nearly uniform. The source analyzes Thorp mixing through representation estimates; the available goal isolates a reciprocal-dimension estimate and its Fourier consequence. The source is OpenAI's September 2026 manuscript.

Setting

A Specht module is a complex representation of a symmetric group associated with a partition. Sum the reciprocals of these dimensions over all partitions of $n$ , and let $C_1$ be the supremum of these sums for positive $n$ . A permutation distribution is compared with uniform through its averaged action on an irreducible representation.

Formalization targets

\sup_{n\ge1}\sum_{\lambda\vdash n}\frac1{\dim S^\lambda}<\infty,\qquad\|\widehat\nu(\rho)\|\le\sqrt{32C_1}(\dim\rho)^{-5/16}.

A conjunction of two parts. First, for each n let reciprocalFirst(n) be the sum, over all partitions p of n, of 1/deg(p), where deg(p) is the complex dimension of the Specht module of shape p (the span of the permutation-group translates of the polytabloid built from the canonical tableau, inside the space of tabloids). Let C1 be the supremum of reciprocalFirst(n) over n ≥ 1. The theorem asserts that this set of values is bounded above, that reciprocalFirst(n) ≤ C1 for every n ≥ 1, and that exceptionalFirst(n) tends to 0 as n → ∞, where exceptionalFirst(n) is the same sum of 1/deg(p) restricted to partitions p whose defect n − max(first row length, first column length) is positive. Second, for every d ≥ 3, every bijection e between the set of positions {0,1}^d (functions Fin d → Bool) and Fin 8 × Fin(2^(d−3)), every finite-dimensional complex inner product space E, and every irreducible complex representation ρ of the symmetric group on the positions, acting on E by inner-product-preserving maps, the following holds. Let ν be a probability distribution on this symmetric group (nonnegative values summing to 1) such that, for each i in Fin 8 and each group element g, the total ν-mass of the coset g·B_i is at most 4·|Sym(2^(d−3))|/|Sym(positions)|, where B_i is the subgroup of permutations that act through e by an arbitrary permutation of the i-th block of 2^(d−3) points and fix all other points. Then the operator norm of Σ_g ν(g)ρ(g) is at most √(32·C1)·(dim E)^(−5/16).

The goal is OAI.Thorp.Current.first_reciprocal_main.

Significance

The goal also proves that the reciprocal sum over shapes of positive defect tends to zero. The Fourier bound applies to distributions satisfying the specified eight-block coset-mass condition. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

One-card mixing does not control high-dimensional permutation representations. The bound must account for small-dimensional exceptional shapes and quantify contraction in every admissible irreducible representation.

Formalization scope

The Fourier clause has $d\ge3$ , positions on a $d$ -bit cube, a bijection into eight equal blocks, and unitary irreducible complex representations. Its coset-mass hypothesis is retained exactly. The target is a supporting representation estimate, not the paper’s final $1600d$ -shuffle total-variation theorem.

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

Selected references

OpenAI, Optimal-order mixing of the Thorp shuffle, preprint, September 2026. Manuscript.
OpenAI, accompanying Lean statement. Pinned source.

40 thms2 active usersReviewed

Top contributors

Rank	Contributor	Accepted solutions	Submitted problems
1	Eyal1990	1098	1567
2	Shuze Chen	822	3136
3	dbenbenn	424	372
4	fizzyinc3	359	0
5	polylog	44	8
6	marwahaha	35	41
7	Ethan Cheung Wang	28	15
8	WillR	20	2
9	Yuxuan Xu	18	34
10	SamenHossain	11	19