All missions

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.

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.

Motivation

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

Setting

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

Formalization targets

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

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

The goal is OAI.DilutedSpinGlass.mezard_parisi.

Significance

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Motivation

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.

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.

Motivation

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

Setting

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

Formalization targets

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

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

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

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

Significance

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Motivation

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

Setting

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

Formalization targets

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

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

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

• gamma differentiability.

Significance

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Motivation

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.

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.

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.

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.

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.

Motivation

The linear Fourier coefficients measure a Boolean function’s correlation with individual inputs. The source studies whether their sum can be controlled solely by the square root of the function’s real polynomial degree. The source is OpenAI's September 2026 manuscript.

Setting

A Boolean function here takes values in $\{-1,1\}$ on a finite sign cube. Fourier coefficients use the uniform distribution. The Fourier degree is the largest support size of a nonzero coefficient; it is unrelated to degree over a field of characteristic two.

Formalization targets

$$\forall C>0\ \exists f:\quad\sum_i\widehat f(\{i\})>C\sqrt{\deg f},\qquad \left\{\frac{\sum_i|\widehat f(\{i\})|}{\sqrt{\deg f}}:\deg f>0\right\}\text{ is unbounded above}.$$

Two things about real Fourier analysis on Boolean cubes, where a Boolean input is read as a sign (false is +1, true is -1), averages are uniform, and degree is the ordinary real Fourier degree, meaning the largest size of a subset s with nonzero Fourier coefficient, the coefficient being the average of f(x) times the product of the signs of the coordinates in s. First, SignedViolations holds: for every real C>0 there is a positive integer n and a function f from {false,true}^n to the reals that takes only the values -1 and 1, is nonconstant, and satisfies C·√(deg f) < Σᵢ f̂({i}), the plain signed sum of its degree-one Fourier coefficients over single coordinates. Second, the set of ratios (Σᵢ |f̂({i})|)/√(deg f), taken over all positive n and all Boolean-valued f on n coordinates with positive Fourier degree, is not bounded above in the reals, so the supremum of these ratios is infinite.

The goal is OAI.SquareRootDegree.main.

Significance

Both signed violations and unbounded absolute ratios are retained. The result concerns failure of every constant multiple, which is stronger than exhibiting one violation of a proposed constant-one inequality. 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 large ambient dimension is not itself a violation: the denominator depends on degree. The function must remain Boolean and nonconstant while its linear coefficient sum outgrows that denominator.

Formalization scope

Inputs are Fin n → Bool, with false interpreted as $+1$ and true as $-1$. The first clause requires positive dimension and a nonconstant function. The second restricts to positive Fourier degree and uses ¬ BddAbove, avoiding a real-valued infinity convention.

The shared definitions are supplied by SquareRootDegree. 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, Unbounded Violations of the Square-Root Degree Bound, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

The Heilbronn triangle problem asks how large the smallest triangle in an $n$-point set can be. A positive improvement in the exponent would contradict bounds at every scale arbitrarily close to $n^{-2}$. The source is OpenAI's September 2026 manuscript.

Setting

Points lie in the closed unit square in the real plane. Triangle area is half the absolute determinant of the two displacement vectors, and the lower-bound condition quantifies over all triples of distinct points.

Formalization targets

$$\delta>0,\quad n_j\to\infty,\quad |P_j|=n_j\ge3,\quad\min_{p,q,r\in P_j\text{ distinct}}\operatorname{Area}(pqr)\ge n_j^{-2+\delta}.$$

The Heilbronn exponent δ is positive and that there exist a sequence of natural numbers n(j) tending to infinity and finite sets P(j) of points in the plane, such that for every j, n(j) ≥ 3, P(j) has exactly n(j) points, all lying in the closed unit square [0,1]×[0,1], and every triple of three distinct points of P(j) spans a triangle of area at least n(j)^(−2+δ). Triangle area is |(q₁−p₁)(r₂−p₂)−(q₂−p₂)(r₁−p₁)|/2. Here δ = 1/(100000·K) with K = T²+1, where T = C(M,3), M = C(4·41−1, 41) = C(163,41), so δ is an explicit but extremely small positive rational constant. Thus the statement asserts an infinite family of point sets whose smallest triangle area is at least a power n^(−2+δ).

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

• almost n minus two refuted.

Significance

The formal goal gives an unbounded sequence of configurations with a fixed explicit power improvement. An attached companion target rules out an eventual almost-$n^{-2}$ upper bound at half that exponent. 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

Avoiding collinear triples is insufficient: every nonzero triangle must also satisfy one uniform quantitative area bound. The exponent must stay positive independently of the size of the configuration.

Formalization scope

The selected goal asserts a sequence tending to infinity, rather than the stronger all-sufficiently-large-sizes statement in the manuscript. The explicit exponent is heilbronnExponent, built from fixed binomial coefficients. Finite sets eliminate repeated points; real powers specify the area scale.

The shared definitions are supplied by HeilbronnTriangle. 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 power improvement in the Heilbronn triangle lower bound, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

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

Setting

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

Formalization targets

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

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

The goal is OAI.SharpTerminalLeave.sharp_terminal_leave.

Significance

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Motivation

Finite matroid packing and covering principles connect disjoint spanning sets with independent covers. The source seeks a concrete obstruction to extending the unrestricted principle to infinite ground sets. The source is OpenAI's September 2026 manuscript.

Setting

A matroid records independent subsets and their closure. A packing/covering partition divides the common ground set into a part with disjoint spanning sets in restrictions and a part covered by independent sets in contractions. Self-duality means equality with the dual on the same labelled ground set.

Formalization targets

$$\exists M_0,M_1\text{ on a countably infinite }E:\quad M_i^*=M_i,\quad I_0\cup I_1\ne E\text{ for every independent pair},\quad\neg\operatorname{HasPackingCovering}(M_0,M_1).$$

The ground type E = ℤ × D, where D is the type of pairs consisting of a natural number m and a Boolean function on Boolean m-tuples, is countable and infinite, and that there exist two matroids M₀ and M₁ on E, each with ground set all of E, each equal to its own dual, such that no independent set of M₀ and independent set of M₁ have union all of E. Yet the pair fails HasPackingCovering. That predicate asks for a partition of the common ground set into P and C, two disjoint subsets S₀ and S₁ of P that are spanning in the restrictions M₀|P and M₁|P respectively, and subsets I₀ and I₁ of C that are independent in the contractions of M₀ and M₁ onto C (the dual of the restriction of the dual to C), with I₀ ∪ I₁ = C. So the theorem asserts a countably infinite pair of self-dual matroids with no such packing-covering decomposition.

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

• partitional intersection counterexample.
• separate covering packing counterexamples.

Significance

The goal simultaneously supplies a countable infinite example, failure of a full independent cover, and failure of every mixed partition. Additional attached statements treat partitional matroids, intersection, and the separate packing and covering assertions. 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

Failure of a full independent cover does not by itself exclude a mixed partition. The matroids must satisfy the infinite independence axioms, including maximal extension, throughout the construction.

Formalization scope

The ground type is the fixed product of integers with finite Boolean-function data. Mathlib matroids have ground set equal to the entire type in the goal. The two source definition groups have overlapping declarations and remain separate reference groups, with no aggregate import.

The shared definitions are supplied by InfiniteMatroid, InfiniteMatroidCorollaries. 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 Infinite Matroid Packing/Covering Conjecture, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

Excluding a fixed clique should force independent sets larger than those guaranteed by average degree alone. The source asks for the full logarithmic improvement uniformly across graph sizes. The source is OpenAI's September 2026 manuscript.

Setting

An independent set contains no adjacent pair. Write $n$ for the number of vertices, $d=2|E|/n$ for average degree, and $α(G)$ for the largest independent-set size. A graph is clique-free of order $r$ when it contains no $r$ pairwise adjacent vertices.

Formalization targets

$$\forall r\ge4\ \exists c_r>0:\quad \alpha(G)\ge c_r\frac{n\log d}{d}\qquad(d\ge2,\ G\text{ is }K_r\text{-free}).$$

For every natural number r ≥ 4, there is a real constant c > 0 such that the following holds for every finite simple graph G on a vertex type V (a Fintype). Here the average degree d(G) is defined as 2|E(G)|/|V|, twice the number of edges divided by the number of vertices (as a real number). If G contains no clique of size r (it is r-clique-free) and d(G) ≥ 2, then the independence number α(G), the maximum size of an independent set, satisfies α(G) ≥ c · |V| · log(d(G)) / d(G), where log is the natural logarithm of real numbers. The constant c may depend on r but not on G.

The goal is OAI.CliqueFreeLog.logarithmic_independence_bound.

Significance

The bound improves the general inverse-degree scale by a factor of natural logarithmic size. The constant may depend on the forbidden clique but must work for every input graph. 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 condition forbids ordinary cliques rather than imposing bounded complexity on every neighborhood. Estimates using maximum degree alone do not establish the stated average-degree bound.

Formalization scope

The representation is Mathlib SimpleGraph on a finite type. Real.log is the natural logarithm and the hypothesis $d\ge2$ keeps its argument and the denominator positive. The empty graph is excluded by that hypothesis.

The shared definitions are supplied by CliqueFreeLog. 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 logarithmic independence bound for clique-free graphs, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

A spanning subgraph in which every vertex has degree two may split into several cycles. Barnette’s question asks when planarity, bipartiteness, and connectivity force those vertices onto one cycle. The source is OpenAI's September 2026 manuscript.

Setting

A cubic graph has degree three at every vertex. A bipartite graph has two vertex classes with every edge crossing between them. A Hamiltonian cycle visits all vertices exactly once before returning to its starting point. Planarity is represented by a drawing using injective continuous edge arcs in the real plane.

Formalization targets

$$G\text{ finite, simple, cubic, bipartite, planar, and 3-vertex-connected}\ \Longrightarrow\ G\text{ has a Hamiltonian cycle}.$$

Every finite simple graph with decidable vertex equality and adjacency has a Hamiltonian cycle if each vertex has degree three, the vertices can be partitioned into two classes with every edge joining different classes, the graph is planar, and it is three-vertex-connected. Here planarity means that vertices can be placed at distinct points of the real plane and edges drawn as injective continuous arcs whose interiors contain no vertices and whose interiors are disjoint for distinct undirected edges; reversing an edge reverses its arc. Three-vertex-connectivity means that the graph has at least four vertices and remains connected after deletion of any set of at most two vertices. The conclusion is the existence of one closed cycle visiting every vertex exactly once before returning to its starting vertex.

The goal is OAI.Barnette.main.

Significance

A proof would turn the source’s Hamiltonicity claim into a result available for arbitrary finite graphs satisfying these exact hypotheses. It would also provide a reusable bridge between geometric embeddings and combinatorial walks. 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

Degree constraints do not guarantee that a spanning cycle cover is connected. The target requires a single cycle and must handle unrestricted face sizes, so verifying local degree conditions is insufficient.

Formalization scope

The published goal unfolds MainStatement. Three-vertex-connectivity requires at least four vertices and connectedness after deletion of any set of at most two vertices. The Hamiltonian object is a closed graph walk satisfying the cycle and vertex-coverage conditions. Stronger edge-avoidance conclusions from the paper are not attached as targets.

The shared definitions are supplied by BarnetteHamiltonian. 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, Paired states and Hamiltonian cycles in cubic bipartite planar graphs, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

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

Setting

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

Formalization targets

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

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

The goal is OAI.TalagrandDiscreteConvexity.talagrand_discrete_convexity.

Significance

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Motivation

Drawing all edges between two vertex classes creates unavoidable intersections. The Zarankiewicz target asks for the exact best crossing count with both part sizes variable. The source manuscript presents the surrounding research claim.

Setting

The complete bipartite graph has vertex type Fin m⊕Fin n and one edge for every pair in Fin m×Fin n. Admissible plane drawings use simple continuous arcs, distinct vertices, finitely many proper double crossings and no triple crossings.

Formalization target

For every m,n>0, prove there is a drawing with exactly

$$Z(m,n)=\left\lfloor\frac m2\right\rfloor\left\lfloor\frac{m-1}2\right\rfloor\left\lfloor\frac n2\right\rfloor\left\lfloor\frac{n-1}2\right\rfloor$$

crossing points, and every admissible drawing has at least Z(m,n) crossings.

The selected formal target is OAI.Zarankiewicz.mainTarget_proof.

Significance and status

The formal target includes both an attaining drawing and the universal lower bound. Small positive part sizes remain in scope. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

The best known construction alone cannot establish optimality. The lower bound must allow arbitrary continuous edge arcs and repeated crossings of a pair of edges.

Formalization scope

Proper intersections use local coordinate-axis charts. Counted objects are crossing points, not merely pairs of edges that meet. The formula is implemented by axisPairs(r)=(r/2)((r−1)/2) in natural arithmetic. Tangencies, overlaps and triple crossings are excluded by the drawing model.

Selected references

• OpenAI, The crossing number of complete bipartite graphs, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

The complete graph forces many crossings in any plane drawing. The mission seeks the exact ordinary crossing number rather than one drawing’s upper bound. The source manuscript presents the surrounding research claim.

Setting

An admissible drawing uses distinct vertex points and injective continuous edge paths whose interiors avoid vertices. Intersections are finitely many proper double crossings, with no triple crossing. Every crossing point is counted, including repeated meetings of a pair of edges.

Formalization target

For n≥3, prove

$$\operatorname{cr}(K_n)=\frac14\left\lfloor\frac n2\right\rfloor\left\lfloor\frac{n-1}2\right\rfloor\left\lfloor\frac{n-2}2\right\rfloor\left\lfloor\frac{n-3}2\right\rfloor.$$

The selected formal target is OAI.Paper170.complete_graph_crossing_number.

Significance and status

The target fixes the exact minimum across the full continuous-drawing class. It does not restrict edges to straight segments or impose a special layout. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

An explicit drawing establishes only an upper bound. The equality also requires a bound valid for all admissible topological drawings.

Formalization scope

The graph uses ordered endpoint pairs with increasing indices. Proper crossings are defined through local open partial homeomorphisms taking the two traces to coordinate axes. The ordinary crossing number is the natural infimum of crossing counts; hill uses natural subtraction and division. The selected theorem starts at n=3.

Selected references

• OpenAI, The crossing number of complete graphs, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

Graph homomorphism inequalities compare the frequency of a fixed pattern with what edge density predicts. The mission asks for one finite host graph violating the proposed bound for a specified bipartite pattern. The source manuscript presents the surrounding research claim.

Setting

The pattern H is the incidence graph between thirteen points and twenty-two explicitly listed triples, giving thirty-five vertices and sixty-six edges. Homomorphism density counts all edge-preserving maps, including noninjective maps, divided by the number of all vertex maps.

Formalization target

Construct a positive-size finite simple host G with at least one edge such that

$$t(H,G)<p(G)^{66},\qquad p(G)=\frac{2|E(G)|}{|V(G)|^2}.$$

The selected formal target is OAI.SidorenkoCounterexample.main.

Significance and status

The counterexample uses the exact supplied pattern rather than an unspecified bipartite graph. A finite host makes the density comparison an ordinary finite counting statement. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

The required strict inequality concerns all homomorphisms, not only embeddings. The host must have an edge so the assertion cannot be replaced by a zero-density degeneracy.

Formalization scope

H is built from the published table of twenty-two triples. Hosts use Fin size, and both graph counts and real density normalizations are fixed. The manuscript’s forcing-conjecture consequence is not an attached formal target.

Selected references

• OpenAI, A counterexample to Sidorenko's conjecture, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

List coloring permits each vertex to have different allowable colors. The mission asks whether the size of the largest clique minor still controls the required list size up to a universal linear factor. The source manuscript presents the surrounding research claim.

Setting

A clique minor of order t is represented by disjoint connected vertex sets, with an edge between every pair. The Hadwiger number h(G) is the largest possible t. The list chromatic number is the least k for which every assignment of at least k colors per vertex admits a proper selection.

Formalization target

Prove one integer C≥1 works for every finite nonempty simple graph:

$$\chi_{list}(G)\le C\,h(G).$$

The constant is chosen before the graph, the vertex type and all color lists.

The selected formal target is OAI.LinearListHadwiger.main_theorem.

Significance and status

The assertion controls list coloring rather than only a common-color-set chromatic number. It is a linear-factor statement, without coefficient-one optimality. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

A coloring from one chosen palette need not respect independently assigned lists. The proof must cover arbitrary color types and list assignments.

Formalization scope

The definitions use finite graph vertex types, arbitrary finite color sets, induced-subgraph connectivity and natural-number infima/suprema. Nonemptiness of the vertex type is explicit. Only the main inequality and its definition block are attached.

Selected references

• OpenAI, A linear list-coloring bound in terms of the Hadwiger number, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

A tile may admit a translation tiling while forcing every such tiling to lack a full lattice of periods. The mission asks for this phenomenon in dimension three and its persistence under Euclidean thickening. The source manuscript presents the surrounding research claim.

Setting

A finite nonempty integer tile T⊆ℤᵈ tiles with complement A when addition T×A→ℤᵈ is bijective. Full periodicity means invariance under a finite-index subgroup. The thickening is the union of closed unit cubes based at T; Euclidean tiling means unique covering almost everywhere.

Formalization target

Construct T⊆ℤ³ that tiles but has no fully periodic complement, and whose thickening tiles ℝ³ but has no complement invariant under any full-rank lattice. Also prove

$$\min\{d:\text{an integer tile without a periodic complement exists in }\mathbb Z^d\}=3.$$

The selected formal target is OAI.PeriodicTilingThree.periodic_tiling_counterexample_and_minimality.

Significance and status

The goal includes both discrete and arbitrary-real-translation Euclidean assertions, plus minimality among all natural dimensions. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

Excluding periodic integer translation sets does not automatically exclude Euclidean tilings with noninteger shifts. The latter universal quantifier is a separate clause.

Formalization scope

Discrete tilings are exact bijections, whereas Euclidean tilings are almost-everywhere unique representations relative to Lebesgue measure. Euclidean full periodicity uses the integer span of a real basis. Closed-cube overlaps are handled by the almost-everywhere convention.

Selected references

• OpenAI, A translational tile with no fully periodic tiling in dimension three, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

A measure-preserving system may have low information production yet fail to admit a smooth realization. The target asks for a single ergodic system excluding every finite-dimensional smooth positive-volume model. The source manuscript presents the surrounding research claim.

Setting

The system is a measurable equivalence T of a standard nonatomic probability space. Standard nonatomic is expressed by an isomorphism with the unit interval after removing null sets. A smooth model is a compact smooth manifold, a smooth diffeomorphism and an invariant probability measure with strictly positive smooth local coordinate density.

Formalization target

Construct a system satisfying

$$T\text{ is ergodic},\qquad h_{KS}(T)<\infty,\qquad T\text{ has no smooth positive-volume model}.$$

The formal finite-entropy predicate requires every finite-partition entropy rate to converge, with one finite real upper bound.

The selected formal target is OAI.SmoothObstruction.main.

Significance and status

The obstruction ranges over every finite dimension, nonorientable manifolds and positive-dimensional smooth boundary models. The manuscript asserts zero entropy; the selected published theorem requires finite entropy only. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

Failure of a particular embedding does not exclude all measure-theoretic conjugacies and all dimensions. Conjugacy is allowed after discarding invariant null sets.

Formalization scope

The goal quantifies over measurable equivalences and uses conull measurable conjugacy, not topological conjugacy. Entropy is measured in bits by the supplied finite-partition definition. Closed models include dimension zero, boundary models require positive dimension, and no orientation hypothesis is imposed.

Selected references

• OpenAI, A zero-entropy system without a smooth positive-volume model, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.