Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A spanning tree keeps a graph connected with as few edges as possible. A spanning tree is thin if, in addition, it uses only a small fraction of the edges of every cut. Thin trees were introduced as a tool for the asymmetric traveling salesman problem (ATSP): Asadpour, Goemans, Mądry, Oveis Gharan and Saberi showed that thin trees, together with cost control, can be augmented cheaply into tours, which gave an -approximation (doi:10.1287/opre.2017.1603). Goddyn's thin tree conjecture asks whether high edge connectivity alone forces an -thin spanning tree, independently of the number of vertices; the strong form asks for thinness in a -edge-connected graph.
Background. Goddyn recorded the conjecture in a 2004 problem list. The Nash–Williams–Tutte theorem (1961) gives edge-disjoint spanning trees in a -edge-connected graph (doi:10.1112/jlms/s1-36.1.445, doi:10.1112/jlms/s1-36.1.221), so each cut is used about times on average, but no single tree need be good for every cut. Oveis Gharan and Saberi proved the bound for planar and bounded-genus graphs (2011, doi:10.1137/1.9781611973082.75). Anari and Oveis Gharan obtained thinness in general (2015, arXiv:1411.4613), using the Marcus–Spielman–Srivastava interlacing-families method (doi:10.4007/annals.2015.182.1.8). Klein and Olver handled any prescribed laminar family of cuts (2023, doi:10.1109/FOCS57990.2023.00011), and Klein, Olver and Yeoh controlled all near-minimum cuts (2026, doi:10.4230/LIPIcs.ICALP.2026.129). Constant-factor ATSP approximations were obtained by other means (Svensson–Tarnawski–Végh 2020, doi:10.1145/3424306; Traub–Vygen 2022, doi:10.1137/20M1339313), but the thin tree question stayed unresolved.
The source of this mission, an OpenAI preprint dated September 23, 2026, claims the strong thin tree conjecture.
Let be a finite undirected multigraph without loops; parallel edges are counted separately. For a nonempty proper subset , let be the set of edges with exactly one endpoint in . is -edge-connected if for every such . For an edge set , . A spanning tree is -thin if for every nonempty proper .
There is a universal constant such that for every , every finite loopless -edge-connected multigraph with at least two vertices has a spanning tree with
Lean: OAI.StrongThinTree.strongThinTree, open on the platform.
The order is optimal (two vertices joined by parallel edges). The theorem would settle both Goddyn's thin tree conjecture and its strong form, removing the loss of Anari–Oveis Gharan. It shows that connectivity alone controls all cuts at once, and gives a structural route to ATSP integrality-gap bounds through thin trees. An algorithmic version (deterministic polynomial-time construction) is the subject of the companion mission in this family. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists.
Averaging over a Nash–Williams–Tutte packing controls each cut on average but not all cuts simultaneously: there are exponentially many cuts and a union bound over them loses a factor depending on . Spectral approaches control all cuts via a matrix inequality, but spectrally thin trees need not exist when some edges have large effective resistance, which is why previous spectral arguments lost factors. One must instead keep a large tree packing on low-resistance edges through a sequence of sparsifications whose relative losses stay bounded.
MultiGraph n m: vertices Fin n, edges Fin m with endpoint maps and a looplessness proof; parallel edges are distinct edges.cut G T S: the edges of T with exactly one endpoint in S. Connected G T: every nonempty proper S is crossed by T. SpanningTree G T: T connected and every proper deletion disconnects.EdgeConnected G k: every nonempty proper cut has at least k edges.MainStatement: ∃ C > 0, ∀ k ≥ 1, ∀ n ≥ 2, ∀ G k-edge-connected, ∃ T spanning tree, ∀ S nonempty proper, |cut T S| ≤ (C/k)|cut G S| (real arithmetic).Needed infrastructure: graph Laplacians and effective resistance, the Nash–Williams–Tutte theorem, the Marcus–Spielman–Srivastava mixed-characteristic-polynomial bound, and a Brouwer-type fixed point theorem (the paper proves the finite-dimensional case via Sperner's lemma). Contributions formalizing Theorem 2.3 (Nash–Williams–Tutte), Theorem 3.2, Theorem 4.1, Proposition 6.2 or Theorem A.1 are welcome.
For integers the Ramsey number is the least such that every simple graph on vertices contains a clique of order or an independent set of order . Ramsey's theorem guarantees these numbers are finite. In the off-diagonal regime, is fixed and ; the classical upper bounds give , while for a long time lower-bound constructions did not reach the power . Once the power was settled, the remaining question was the power of .
A graph on vertices is a SimpleGraph (Fin N). The Lean development defines
RamseyProperty s t N: every graph on Fin N has an -clique, or its complement has a -clique (an independent set of size );ramsey s t := sInf {N | RamseyProperty s t N}, the Ramsey number .All logarithms are natural; real powers of use Real.rpow.
For every integer there is such that for every and every sufficiently large (threshold depending on )
This is Theorem 1.1 of the source, formalized as main (s) (hs : 6 ≤ s) : MainBounds s ∧ MainLimit s. The goal is published on the platform with status Open; no machine-checked proof exists.
The result itself. Together with the companion preprint and the earlier results for on the polynomial exponent, the theorem identifies the exact power of in up to for each fixed : the classical AKS upper bound is sharp in its logarithmic exponent. It does not give a matching constant-factor lower bound. The main new ingredient is a prime-indexed construction (Theorem 1.2 of the source): for fixed and large primes , a -free graph on vertices with independence number below , built from random incident point–hyperplane flags of .
Formalizing it. The upper half is classical (Proposition 7.3 of the source restates the AKS estimate for all fixed ). The lower half is a long argument combining finite projective geometry, entropy of a selected subsequence, and incidence bounds in positive characteristic; formal verification would independently check an unrefereed claim.
Bradač's projective graph has the right number of vertices but its independent sets were only controlled up to logarithmic exponent . Improving to requires bounding long independent sequences in a random stream of flags. A union bound over sequences loses too much, and a sequence selected from the random stream need not have independent or uniform flags. The source pays for this with an entropy lower bound on the selected sequence and a compression upper bound, which in turn requires a description theorem for sparse point–hyperplane pairs in arbitrary dimension (repeated projections and a high-rank two-row description based on a finite-field Zariski-closure inequality of Nie and Wang).
SimpleGraph (Fin N); independent sets are cliques of the complement graph. ramsey is an sInf, equal to because the defining set is nonempty by Ramsey's theorem.MainBounds s fixes one (depending on ) before quantifying over ; natural subtraction s - 1, s - 2 is harmless because . MainLimit s is a Filter.Tendsto over natural .For integers the Ramsey number is the least such that every simple graph on vertices contains either a complete subgraph or an independent set of vertices. Determining how grows when is fixed and is one of the central problems of extremal and probabilistic combinatorics: upper bounds come from counting and local density arguments, lower bounds require explicit or random constructions of -free graphs with no large independent set, and for decades the two sides did not even agree on the power of .
A graph on vertices is a SimpleGraph (Fin n). A -clique is a set of pairwise adjacent vertices and a -independent set a set of pairwise non-adjacent vertices. The Lean development defines
RamseyProperty s t n: every simple graph on Fin n has an -clique or a -independent set;ramsey s t := sInf {n | RamseyProperty s t n}, the Ramsey number .All logarithms are natural.
There is an absolute constant such that for every and all sufficiently large (threshold depending on )
and consequently
This is Theorem 1.1 of the source, formalized as SharpBounds ∧ SharpExponent. The goal is published on the platform with status Open; no machine-checked proof exists.
The result itself. The theorem determines up to a factor , the first case beyond in which the logarithmic exponent of a fixed off-diagonal Ramsey number is known. It shows that the classical upper-bound exponent is the truth for , and it leaves open only a constant-factor asymptotic for . The lower-bound construction (random incident point–hyperplane pairs in projective space , ordered by position) together with its entropy/compression analysis is the new part.
Formalizing it. The upper bound is an elementary argument (triangle-free independent-set bounds plus random sampling), stated separately in the source as Theorem 2.1 for all ; its formalization is a self-contained milestone. The lower bound is a long probabilistic and finite-geometric argument whose formal verification would independently certify an unrefereed claim.
The lower bound needs a -free graph on about vertices with no independent set of size . Random graph processes lose logarithmic factors and even the power of ; Bradač's projective graph has the right power but its independent sets were only controlled to logarithmic exponent . The obstacle is to bound long independent sequences in a random stream of flags: a direct union bound over sequences is far too weak, and the selected sequence can have a heavily biased law. The source handles this with an entropy lower bound and a matching compression (description) upper bound that relies on a new theorem about sparse point–hyperplane incidences.
SimpleGraph (Fin n); cliques and independent sets use Mathlib's IsNClique and IsNIndepSet. ramsey is an sInf, which is the true Ramsey number because the defining set is nonempty by Ramsey's theorem; a proof must use that nonemptiness rather than the junk value 0.SharpBounds fixes one before ; the threshold may depend on . The power is Real.rpow. SharpExponent is a Filter.Tendsto statement over natural with real logarithms.The chromatic symmetric function of a graph, introduced by Stanley, records all proper colorings of the graph with infinitely many colors as a symmetric function; it refines the chromatic polynomial. Whether it expands with nonnegative coefficients in the basis of elementary symmetric functions ("-positivity") is a central question in algebraic combinatorics. The Stanley–Stembridge conjecture (1993) predicted -positivity for incomparability graphs of -free posets; it arose from positivity questions for immanants of Jacobi–Trudi matrices. Shareshian and Wachs introduced a -graded refinement, the chromatic quasisymmetric function, which tracks ascents of colorings along edges, and conjectured that for natural unit interval graphs its elementary coefficients are polynomials in with nonnegative integer coefficients. The -refinement is tied to geometry: it describes the graded representation of the symmetric group on the cohomology of regular semisimple Hessenberg varieties.
Let be weakly increasing with . The natural unit interval graph has vertices and edges with . A proper coloring gives different colors to adjacent vertices, and counts edges with . The chromatic quasisymmetric function is
For a partition , with . Let be the set of permutations (as words ) such that every adjacent descent is an edge, and the number of inversions , , with an edge.
In Lean (namespace OAI.ElementaryPositivity), NaturalUnitIntervalGraph n stores a monotone extensive h : Fin n → Fin n; chromatic r is in variables as an MvPolynomial (Fin r) (Polynomial ℕ); Nondescent and graphInversions define and ; a PermutationWitness is a map together with the identity below in every number of variables, using Mathlib's MvPolynomial.esymmPart.
For every and every natural unit interval graph on there is a map with
In particular every elementary coefficient of lies in . The goal is published on the platform with status Open.
The result itself. The theorem resolves the elementary-positivity part of the Shareshian–Wachs conjecture, and at , via Guay-Paquet's reduction, recovers the Stanley–Stembridge conjecture first proved by Hikita. It is stronger than positivity: it gives a combinatorial witness, assigning each permutation of an elementary partition while preserving its graph-inversion weight. Through the Brosnan–Chow/Guay-Paquet identity, it implies that each graded piece of the cohomology of a regular semisimple Hessenberg variety is a direct sum of Young permutation modules with multiplicities counted by the witness (Corollary 1.2). Elementary unimodality, the other part of the Shareshian–Wachs conjecture, is not addressed.
Formalizing it. The statement is a finite polynomial identity for each , and , fully expressible with Mathlib's multivariate polynomials and elementary symmetric polynomials. A machine-checked proof would certify a long bijective argument (walls, triangle moves, witness completion) with many case distinctions.
The coloring definition already has nonnegative coefficients in the monomial basis, but rewriting in the elementary basis involves subtraction, so positivity is not visible from the definition. Earlier positive formulas (Schur expansions, power-sum expansions, the acyclic-orientation formula) group partitions or work at , and Hikita's probabilistic formula has rational -weights that are only positive at real , not coefficientwise. A proof over must produce, for each elementary partition and each power of , a nonnegative integer count, uniformly over all graphs.
h : Fin n → Fin n monotone with i ≤ h i (zero-indexed); edges are in either order.Fin r and the identity is required for every , which is equivalent to the identity of symmetric functions since both sides are homogeneous of degree .Polynomial ℕ, so nonnegativity in is built into the statement; the witness theta is an arbitrary function on the finite set . The source's additional assertion that is produced by a deterministic terminating procedure is not encoded, but any such function on a finite set is computable by search, so nothing of mathematical substance is lost.Kazhdan–Lusztig polynomials are integer polynomials attached to pairs of elements of a Coxeter group. They were introduced through the canonical basis of the Hecke algebra (Kazhdan–Lusztig, 1979). For Weyl groups they compute local intersection cohomology of Schubert varieties, and they enter the Kazhdan–Lusztig conjectures on characters of highest-weight representations. Their definition uses the simple generators of the group, yet in every known example seemed to depend only on the Bruhat interval as an abstract partially ordered set. The combinatorial invariance conjecture, attributed to Lusztig and Dyer, asserts this: if two Bruhat intervals, possibly in different Coxeter groups, are isomorphic as posets, their Kazhdan–Lusztig polynomials coincide.
This mission asks for a formal proof of the conjecture, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
A Coxeter system is a group with a generating set of involutions subject only to relations . Write for word length in . A reflection is a conjugate of an element of . Bruhat order is the partial order generated by whenever is a reflection and ; the interval is finite and graded of rank , even when is infinite. The equal-parameter R-polynomials and Kazhdan–Lusztig polynomials are the unique families with , unless , the recursion: for with ,
the degree bound for , and the inversion formula
Let and be arbitrary Coxeter systems, in and in . If is an isomorphism of posets (a bijection preserving and reflecting order), then
The isomorphism carries no labels or root data; the groups may be infinite and noncrystallographic.
The result itself. It shows that a Kazhdan–Lusztig polynomial, defined algebraically from the Hecke algebra, is determined by a finite poset. Restricting to subintervals gives the same for every with , and hence for the R-polynomials (Corollary 6.1, p. 29). For Weyl groups this means that local intersection cohomology of Schubert varieties is determined by the Bruhat poset. It settles a question open since the 1980s that had been verified only for lower intervals, short intervals, low ranks, and single coefficients.
Formalizing it. Mathlib has Coxeter systems and their length function but no Bruhat order, Hecke algebra, or Kazhdan–Lusztig theory. The proof uses reflection orders (Dyer's path formula, Theorem 2.2, p. 7), Braden–MacPherson moment-graph sheaves over a reflection-faithful real realization (Theorem 2.3, p. 8), and the Elias–Williamson character theorem as external inputs. Building these would be a substantial, reusable contribution to formal representation theory.
The defining recursion uses a simple generator with , but a poset isomorphism need not carry simple generators or reflections to anything recognisable, and need not respect root labels. Dyer's reconstruction recovers all reflection edges of the Bruhat graph from the order (Theorem 3.4, p. 12) but not their labels. Lanini's moment-graph invariance requires compatible label automorphisms, which an abstract isomorphism does not provide. The preprint therefore keeps the two realizations separate, transports reflection orders through maximal dihedral subintervals (Proposition 3.5, p. 13), counts later edges exactly, and compares images of edges in two different sheaves by a reciprocal inequality that is then forced to be an equality (Sections 5–6).
CoxeterSystem M W for arbitrary index types and groups; the two systems may live in different universes.BruhatLE is the reflexive–transitive closure of with a reflection and , i.e. strong Bruhat order (not weak order). Interval cs u b carries this order; ι is an order isomorphism ≃o.klPolynomial is the second component of Classical.epsilon (NormalizedKL cs), where NormalizedKL encodes exactly the normalization above (R-recursion with left multiplication, diagonal and vanishing conditions, , and the inversion formula with Polynomial.reflect). Existence and uniqueness of such families is the classical Kazhdan–Lusztig theorem, and a proof of the goal has to establish them, since otherwise Classical.epsilon returns an arbitrary pair.finsum; intervals are finite, so this is the ordinary sum.Welcome contributions: Bruhat order and its basic properties (subword property, finiteness of intervals), R-polynomials, and existence and uniqueness of Kazhdan–Lusztig polynomials for arbitrary Coxeter systems.
The unit-distance problem of Erdős asks how many pairs among points in the plane can be at distance exactly one. By rescaling, this is the same as asking how often a single distance can repeat. It is one of the central extremal questions of combinatorial geometry and a benchmark for incidence methods. The bound of Spencer, Szemerédi and Trotter (1984) has resisted improvement of its exponent for four decades, and the same exponent is sharp for the closely related Szemerédi–Trotter point–line incidence theorem, so any improvement must use geometry specific to circles in the Euclidean plane.
This mission formalizes the main theorem of an OpenAI preprint dated September 23, 2026 (source), which claims a fixed power saving: for some absolute . The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open (stated, not yet proved).
For a finite set let
the number of unordered pairs of distinct points at Euclidean distance one, and let
The maximum exists because .
There are absolute constants and such that
Equivalently, for an absolute . The goal leaves and unspecified, so it is stable under any later numerical improvement.
The result itself. It answers the long-standing question of whether the Spencer–Szemerédi–Trotter exponent can be lowered by a fixed amount. Combined with the recent lower bounds along a sequence, it confines the true exponent to an interval strictly inside . Because point–line incidences do attain , the result also isolates a genuine difference between unit circles and lines in incidence geometry.
Formalizing it. The proof combines random cuttings in the Clarkson–Shor framework, an entropy-based prediction lemma, the product formula and absolute heights of algebraic numbers, and an algebraic obstruction using derivations and valuations of function fields. A formal proof would add these to Mathlib and would also require the bound itself (via the crossing lemma) as background. No machine-checked unit-distance bound beyond trivial ones is known.
Every known proof of uses only two combinatorial properties of unit circles (two circles meet in at most two points; two points lie on at most two unit circles), and those properties are shared by systems attaining , so no argument using only them can save a power. The saving must exploit arithmetic or algebraic rigidity of the Euclidean metric. In the preprint the scheme is a contradiction argument on a hypothetical sequence with unit pairs among points: transfer to number fields, measure edge-jump profiles at all absolute values, and show that either a bounded-scale configuration violates a determinant identity (Proposition 4.4, p. 19) or a dense pair graph with low-height rectangle products arises, which is excluded algebraically (Proposition 8.1, p. 42). The hard step is transferring concentration from predicted states to actual points under the true edge and history laws (Lemma 6.2, p. 29).
EuclideanSpace ℝ (Fin 2); unitPairCount X counts elements of X.sym2 (unordered pairs, diagonal included but never at distance ) with dist = 1.u n is the natural-number sSup of unitPairCount X over -element Finsets; the set is nonempty and bounded by , so it is the true maximum.∃ C β : ℝ, 0 < C ∧ 1 ≤ β ∧ β < 4/3 ∧ ∀ n, (u n : ℝ) ≤ C * n ^ β with real-power exponent. At both sides vanish.Erdős's distinct-distance problems ask how few different distances points in the plane can determine. The global version, which counts all distances between all pairs, was essentially settled by Guth and Katz, who proved that every -point planar set determines at least distinct distances (Annals 2015), matching the square lattice up to a factor. The pinned version asks for many distances measured from a single point: given , is there a pin from which almost distinct distances are visible? The weak pinned Erdős conjecture asserts that for every some pin sees at least distinct distances. Erdős stated the question in 1957 (Michigan Math. J. 1957, Problem 16). Pinned bounds are a standard test for incidence-geometric methods, since Guth–Katz controls only the union of distances over all pins.
This mission formalizes the main theorem of an OpenAI preprint dated September 23, 2026 (source), which claims that large repeated-distance fibres are rare at almost every pin and deduces the weak pinned conjecture. The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open (stated, not yet proved).
Let be a finite set with . For distinct , the distance fibre size is
the number of points of at the same distance from the pin as (it counts itself). Each pair uses its own pin; pairs sharing a numerical distance but with different pins are not pooled. For define
the largest possible fraction of ordered distinct pairs that lie in a distance fibre of size at least .
For every fixed ,
The convergence is uniform over all configurations; no separation, general-position or coordinate hypothesis is imposed, and no rate is claimed.
The result itself. Corollary 1.2 (p. 2) follows in a few lines: for every , the fraction of pins with fewer than distinct distances tends to uniformly in , so all but points see at least distances. This settles the weak pinned conjecture, improving the previous best exponent to . An exceptional set is unavoidable: the centre of a circle carrying the other points sees one distance. The sharper conjecture of order at a pin is not addressed.
Formalizing it. The proof combines transfer for real closed fields (to move a configuration into a number field), the product formula over all places of a number field, random nested grids, and weak compactness of probability measures. A formal proof would exercise Mathlib's number-field and measure-theory libraries in combination, and the statement itself is elementary enough to audit easily. No machine-checked pinned-distance bound is known.
Incidence bounds (Szemerédi–Trotter type) and entropy inequalities give pinned exponents strictly below , and the obstruction is structural: they count incidences globally, while the pinned problem needs control at individual pins. The preprint (pp. 3–4) proceeds by contradiction and uses that squared distance factors as with , so on a fibre one coordinate is a fractional linear function of the other. Turning the product formula into usable information requires an exact additive overlap identity for nested partitions at every absolute value (Section 3), with the field and its degree unbounded along the sequence, and then a limiting argument that rules out non-atomic fibre maps (Lemma 7.1, p. 25).
EuclideanSpace ℝ (Fin 2); configurations are Finsets. k P x y counts (P.erase x).filter (dist z x = dist y x).richPairs P s is the set of ordered pairs with and ; pairFraction divides by as a real.F n s is the sSup over all -point sets of pairFraction for and is defined as 0 for . For the set of values is nonempty and contained in , so sSup is the true supremum.Tendsto (fun n => F n s) atTop (𝓝 0) for each fixed s > 0; it is not vacuous, since is a genuine supremum over all configurations.A vertex cover of a hypergraph is a set of vertices meeting every edge; the covering number is the minimum size of a cover, and the matching number is the maximum number of pairwise disjoint edges. In an -partite -uniform hypergraph the vertices are split into parts and every edge contains exactly one vertex from each part. Ryser's covering conjecture asserts
For it is Kőnig's theorem, so it proposes a higher-dimensional analogue of the most basic min–max theorem of bipartite matching theory. In the intersecting case () it asks for a cover of size , and it is equivalent to Gyárfás's conjecture that monochromatic trees cover any -edge-coloured complete graph.
Background. An equivalent formulation appears in Henderson's 1971 thesis (doi:10.7907/J1Z1-SK19). Aharoni proved the case in 2001 (doi:10.1007/s004930170001); Gyárfás and Tuza settled the intersecting case through ; Haxell and Scott (2012) proved for (doi:10.37236/1175); Francetić, Herke, McKay and Wanless (2017) handled linear intersecting hypergraphs through rank nine (doi:10.1016/j.ejc.2016.10.004); Bishnoi, Das, Morris and Szabó (2021) treated -intersecting hypergraphs (doi:10.1016/j.jcta.2020.105366). Truncated projective planes give equality whenever is a prime power; equality examples were studied by Mansour, Song and Yuster (2009, doi:10.1007/s00373-008-0821-9), Aharoni, Barát and Wanless (2016, doi:10.1007/s00373-015-1575-9) and Abu-Khazneh, Barát, Pokrovskiy and Szabó (2019, doi:10.1016/j.jcta.2018.07.011). Clow, Haxell and Mohar disproved Lovász's stronger matching-reduction conjecture at (doi:10.1007/s00493-026-00220-3), without contradicting Ryser's inequality.
The source of this mission, an OpenAI preprint dated September 23, 2026, claims intersecting counterexamples for ranks .
A finite hypergraph is a finite set of edges, each a finite set of vertices. It is -partite -uniform if there is a map assigning each vertex one of parts such that every edge contains exactly one vertex of each part. It is intersecting if it is nonempty and any two distinct edges share a vertex, so . Every edge of an intersecting hypergraph is itself a cover, so always; a counterexample to Ryser's conjecture in the intersecting case needs .
There are a prime with and such that for every prime , , an intersecting -partite -uniform hypergraph with and exists.
There is such that for every prime with there is such that for every odd , with , there is a finite intersecting -partite -uniform hypergraph with
In particular infinitely many ranks fail. Lean: OAI.RyserOdd.eventualOddFailures_and_infinite, open on the platform.
The theorem would disprove Ryser's conjecture in its intersecting case, and through the standard transfer (Corollary 1.2) also Gyárfás's monochromatic tree-cover conjecture, for the ranks . The value is the maximum possible. A companion preprint of the same family covers a different range of ranks (prime , with balanced parts); the two constructions are independent apart from three elementary estimates. Thresholds are not numerical. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists.
The truncated-plane examples sit exactly at , and covers may mix vertices from different parts, so enlarging individual parts does not help. One must insert exceptional edges that destroy every cover of size while preserving the intersecting property. Ruling out all small covers requires showing that any small cover contains almost a full pencil of lines, which over needs an incidence bound with a power saving (a Bourgain–Katz–Tao-type sum–product estimate) valid in fields whose proper subfields are small. This is where odd exponents and the congruence enter.
Hypergraph V := Finset (Finset V) over a finite type V with decidable equality.RPartiteUniform r H: some part : V → Fin r with exactly one vertex of each part in every edge. Uniform r H: every edge has r vertices.Intersecting: distinct edges meet. matchingNumber is the maximal size of a pairwise disjoint subfamily; coverNumber is sInf of cover sizes, and existence of a cover is asserted separately so the sInf is not the empty-set default.ExplicitFailureAt r packages all of these with , and ; the goal asserts it for the stated ranks and that the set of failing ranks is infinite.Needed infrastructure: finite fields and their projective planes, incidence and sum–product estimates, and probabilistic selection arguments. Contributions formalizing Theorem 2.1 (uniform incidence saving), Lemma 3.2 (line covers after random deletions) or Theorem 4.1 (compatible translates from independent pools) are welcome.
A vertex cover of a hypergraph is a set of vertices meeting every edge; the covering number is the minimum size of a cover, and the matching number is the maximum number of pairwise disjoint edges. An -partite -uniform hypergraph has disjoint vertex parts, and every edge takes exactly one vertex from each part. Ryser's covering conjecture asserts that every such hypergraph satisfies
For this is Kőnig's theorem for bipartite graphs, so the conjecture is a proposed higher-dimensional Kőnig theorem. Its intersecting case (, bound ) is equivalent to Gyárfás's conjecture that every -edge-coloured complete graph can be covered by monochromatic trees, which connects it to Ramsey-type covering problems.
The source of this mission, an OpenAI preprint dated September 27, 2026, claims counterexamples to the conjecture itself, already in the intersecting case and with all parts of equal size.
Fix . A -partite -uniform hypergraph on parts is given by its edge set, each edge choosing one vertex in every part. It is intersecting if it has at least one edge and any two edges share a vertex (necessarily in the same part). A vertex is nonisolated if it lies in some edge. For an intersecting hypergraph , so Ryser's conjecture predicts .
The natural extremal example comes from the affine plane : one part per direction, one vertex per line, one edge per point. It is intersecting with , attaining the conjectured bound.
There is such that for every prime there exists a finite intersecting -partite -uniform hypergraph with
and every vertex lies in an edge. Lean: OAI.Balanced.main_result, open on the platform.
Since and , the theorem would disprove Ryser's conjecture for infinitely many , in its intersecting case. The value is the largest possible for an intersecting -uniform hypergraph (any edge is a cover), and the part sizes are the smallest compatible with , so the examples are extremal in both respects. Via the standard transfer (Corollary 1.2) they also disprove Gyárfás's tree-cover conjecture for colours. The threshold is not explicit. A companion preprint of the same family gives counterexamples over extension fields without balance. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists.
The affine-plane example sits exactly at the conjectured bound, and its minimum covers are rigid (parallel classes). Raising by one requires adding edges that destroy every -element cover while keeping the hypergraph intersecting and keeping only vertices per part; adding a new part, as Abu-Khazneh et al. did, changes and only reaches equality. Verifying that no cover of size survives requires controlling all small sets of lines, which the paper does with stability results for line covers in prime-order planes and a probabilistic selection.
PartiteHypergraph r n has vertex set Fin r × Fin n and edges a Finset (Fin r → Fin n); an edge contains the vertices .Intersecting: edges nonempty and any two edges agree in some coordinate. Nonisolated: every lies in some edge. HasCoverNumber H k: some cover has exactly vertices and every cover has at least .MainResult: ∃ q₀, ∀ q ≥ q₀, q.Prime → ∃ H : PartiteHypergraph (q+1) (q+1), Intersecting ∧ Nonisolated ∧ HasCoverNumber (q+1).ZMod q.Contributions formalizing the deterministic reduction (Proposition 2.1), the stability of affine line covers (Lemma 3.3, building on Szőnyi–Weiner), or the selection step (Proposition 5.1) are welcome, as is the monochromatic tree-cover corollary.
Van der Waerden's theorem (1927) says that for every number of colours and every length , every -colouring of a long enough interval of integers contains a monochromatic arithmetic progression of length . The van der Waerden number is the least such interval length. Its upper bounds were for a long time not even primitive recursive (Shelah 1988 gave the first primitive recursive bound; Gowers 2001 gave a tower-type bound), while lower bounds stayed close to exponential, . Erdős asked whether , i.e. whether the growth is genuinely faster than any exponential. Lower bounds on correspond to long colourings with no monochromatic progression and are a central quantitative question in Ramsey theory.
For two colours, superexponential growth had not been established. The source of this mission, an OpenAI preprint dated September 23, 2026, claims a bound of the form uniformly in .
For positive integers , is the least positive integer such that every map is constant on some progression
Colourings may use fewer than colours.
There is an absolute such that for every and every ,
In particular for each fixed . The constant is the paper's and is not optimized. The Lean statement OAI.QuantitativeVanDerWaerden.uniform_lower_bound is open on the platform.
The theorem gives a quantitative positive answer to Erdős's superexponential-growth question for two colours, and is stronger than the statement settled by Campos–Fox–Schildkraut. It is uniform in the number of colours with a single threshold , which complements the Fox–Hunter bounds that require many colours relative to . The bound is still far from the best upper bounds, which are tower-type.
The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. A formal proof would certify an explicit colouring construction together with a probabilistic (local-lemma) argument.
Random colourings with the local lemma give only : the number of -term progressions in is of order , and each is monochromatic with probability , which caps the length at exponential size. Algebraic constructions such as Berlekamp's gain only a factor . A superexponential bound needs colourings with structure that kills most progressions deterministically, while the remaining progressions are few enough to be destroyed randomly, uniformly down to two colours.
MonoAP c k a d: the colour of equals the colour of for ; HasMonoAP c k N: some with .IsRamsey α k N: every colouring ℕ → α has a monochromatic -AP in (equivalent to the paper's after a shift).W r k is the sInf of positive Ramsey for colours Fin r. If no such existed this would be and the goal's strict inequality would fail, so the goal implicitly includes van der Waerden's theorem.Nat.log 2 r and the real constant 1/100000.A complete development needs van der Waerden's theorem (or at least finiteness), a finite asymmetric local lemma, and the paper's explicit adaptive-mesh colourings and counting of affine signatures. Contributions formalizing Lemma 4.1 (finite asymmetric local lemma) or Theorem 6.3 (a cyclic two-colouring) are welcome.
The Hadwiger–Nelson problem asks for the chromatic number of the plane : the least number of colours needed to colour every point of the Euclidean plane so that any two points at distance exactly receive different colours. Equivalently, it is the chromatic number of the infinite graph whose vertices are the points of the plane and whose edges are the unit-distance pairs. Since 1950 the answer has been known to lie between and , and it is one of the best known open problems in combinatorial geometry. Its difficulty is that the colour classes may be arbitrary sets: no measurability or regularity is assumed, so analytic tools that work for measurable colourings do not apply directly.
This mission asks for a formal proof that five colours do not suffice, as claimed in an OpenAI preprint dated September 23, 2026 (source), so that . The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
A proper -colouring of the plane is any function such that whenever , with the Euclidean norm. No measurability, continuity or regularity of the colour classes is assumed. is the least admitting a proper -colouring.
There is a proper -colouring of the plane: colour the Voronoi hexagons of a triangular lattice (circumradius ) by the seven cosets of an index-seven similar sublattice, assigning boundary points to any incident hexagon. This classical construction is reproved in the deduction of Theorem 1.1 (pp. 2–3), including all boundary points.
There is no function with whenever . Together with the milestone this gives .
The result itself. It raises the lower bound for the chromatic number of the plane from five (de Grey, 2018) to six, leaving only and . Unlike de Grey's bound it is not witnessed by a finite graph; the proof transfers the problem to measurable colourings for every number of colours (Theorem 1.3, p. 2) and then excludes weak measurable five-colourings (Theorem 1.4, p. 2). The transfer theorem is of independent interest: in ZFC, a proper -colouring exists iff a weak measurable -colouring does. The preprint also derives a positive lower bound on the invariant-mean frequency of monochromatic unit pairs for every five-colouring (Corollary 1.5, p. 5).
Formalizing it. The statements are elementary, but the proof uses ergodic theory (a Furstenberg–Zimmer compact-extension tower and rigidity of invariant measures on a character group, Theorem 2.3, p. 6), spectral theory, density points, Fourier decay of circle measure, and planar topology. A formal proof would remove any doubt about a long and varied argument. The finite-graph bound has been checked by SAT solvers, but no formal proof of a bound that is not witnessed by a finite graph is known.
By de Bruijn–Erdős, is equivalent to the existence of a finite unit-distance graph that is not -colourable, but no such graph is known, and SAT-based searches have not produced one. Measurable methods (Falconer's density-point argument) cannot be applied to arbitrary colour classes, and a measurable colouring can have boundaries far too irregular for map-type interface arguments such as Townsend's or Sokolov–Voronov's. The preprint must therefore (i) produce measurable data from an arbitrary colouring without losing the unit-distance exclusions, via invariant averaging over algebraic rotations and translations and the rigidity Theorem 2.3, and (ii) construct the connected interfaces needed for a geometric contradiction from measure estimates alone (Sections 5–7), before excluding label cycles of length , and (Section 8).
ℂ with ‖p - q‖ = 1; a colouring is any function ℂ → Fin 5. ProperColoring 5 c requires distinct colours at every unit-distance pair. No measurability is assumed, so the statement is about arbitrary colourings, as in the source.EuclideanSpace ℝ (Fin 2) with dist x y = 1 and asks for some c : Plane → Fin 7; the two planes are isometric.Welcome contributions: the de Bruijn–Erdős compactness theorem, the Moser spindle, Lebesgue density points in , and the measurable/unrestricted transfer of Theorem 1.3.
In 1933 Borsuk asked whether every bounded set of positive diameter in can be split into pieces of strictly smaller diameter. The answer is yes in dimensions and for smooth convex bodies, and a regular simplex shows that pieces may be necessary. Kahn and Kalai showed in 1993 that the answer is no in high dimensions, and since then the question has been: in which dimensions does Borsuk's assertion first fail? The smallest known counterexample dimension measures how far our understanding of diameter partitions extends; it has been reduced from to by combinatorial constructions, while the assertion is open in all dimensions between and the current record.
The source of this mission, an OpenAI preprint dated September 23, 2026, claims a counterexample in dimension .
For a bounded set of positive diameter, is the least number of subsets of strictly smaller diameter that cover (covers and partitions give the same number). Borsuk's assertion in is that for every such .
Let be the real symmetric matrices with the Frobenius norm . The trace-one hyperplane in is a -dimensional affine Euclidean space. For a unit vector , is the orthogonal projector onto the line . Two such projectors are at distance exactly when the lines are orthogonal.
The set
is compact, has Frobenius diameter , and cannot be covered by ten subsets of diameter strictly less than . Hence and Borsuk's assertion fails in dimension . The Lean statement OAI.BorsukNine.main_theorem is open on the platform.
The theorem lowers the smallest known counterexample dimension for Borsuk's conjecture from to , and the paper extends it to compact counterexamples in every dimension (Corollary 7.1). Unlike previous counterexamples, which are finite point sets built from codes or strongly regular graphs, the witness is a continuum: the image of real projective -space under the projector embedding. The theorem does not determine the smallest failing dimension (the assertion remains undecided in dimensions to ) or the exact value of .
The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. A formal proof would combine metric geometry, an algebraic-topological degree argument and a finite combinatorial obstruction.
Previous counterexamples use finite sets where a counting argument (Frankl–Wilson type) forces many parts; such counting gives nothing for a -dimensional continuum. For , a cover by ten small sets corresponds to ten nonnegative functions on summing to one, with orthogonal lines never sharing a positive coordinate. One would like to use the minimal number of vertices of a triangulation of (Walkup: eleven), but the positive-support complex arising from such functions is not a triangulation, so its face structure has to be derived from the map itself.
EuclideanSpace ℝ (Fin 4); matrices are EuclideanSpace ℝ (Fin 4 × Fin 4), whose norm is the Frobenius norm. projector u has entries .projectorSet is the image of the unit sphere; traceOneSymmetric is the set of symmetric matrices of trace .HasTenSmallCover: ten subsets of projectorSet covering it, each with Metric.diam < √2. Requiring the pieces to lie in loses no generality, and keeps Metric.diam away from its default value for unbounded sets.IsCompact projectorSet, containment in traceOneSymmetric, Metric.diam projectorSet = √2, and ¬ HasTenSmallCover.A complete development needs partitions of unity, mod-two degree of odd maps on spheres, local preimage counting, and a finite combinatorial case analysis on labelled supports. The finite combinatorial part (Sections 5–6) and Lemma 2.4 (reduction to strict gaps) are self-contained and welcome first contributions.
A billiard in a polygon is a point moving at unit speed inside the table and reflecting off the sides by the law "angle of incidence equals angle of reflection". It is one of the simplest Hamiltonian systems and a standard model in mathematical physics; triangles also model two point masses colliding on a segment. The natural invariant probability measure is normalized area times uniform direction, and the basic question is ergodicity: are the only flow-invariant sets of measure or ? For polygons with angles that are rational multiples of the answer is no (the phase space splits into invariant surfaces, one for each family of directions). For triangles with an irrational angle the question has been open for every individual triangle, with only generic or specially approximable examples known.
The source of this mission, an OpenAI preprint dated September 25, 2026, claims ergodicity for every triangle with at least one irrational angle.
Let be the open interior of a nondegenerate triangle in with angles . The phase space is (position and unit direction). The billiard flow moves a state in a straight line at unit speed; on reaching an open side it reflects the direction across that side (tangential component preserved, normal component reversed). Trajectories that hit a vertex, in either time direction, have no continuation and are discarded; they form a null set. The invariant probability measure is
is ergodic if every measurable with for all has .
If at least one of , , is irrational, then the billiard flow on is ergodic for :
The Lean statement OAI.TriangularBilliards.irrational_triangle_billiard also asks for the standard well-posedness facts (almost every state has a unique complete trajectory avoiding vertices, each preserves , and almost everywhere), so that the ergodicity clause is about the actual billiard flow. It is open on the platform.
The theorem settles ergodicity for the entire class of triangles with an irrational angle, including triangles with one rational and two irrational angles, with no genericity or Diophantine condition; earlier results gave ergodicity only for a residual set or for tables with exceptionally fast rational approximations. It also contradicts the non-ergodicity suggested by numerical experiments, which can now be attributed to slow convergence. The paper derives interior and boundary quantum ergodicity of Dirichlet and Neumann eigenbases and growth of nodal-domain counts for these triangles. The claim is ergodicity only, not mixing or unique ergodicity.
The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists.
Triangle sides are straight, so there is no dispersing curvature to drive hyperbolicity, and trajectories near vertices have no continuous continuation. Rational-approximation arguments (Kerckhoff–Masur–Smillie, Vorobets) only reach generic or specially approximable tables. The Forni–Moll framework shows that invariant functions with horizontal Sobolev regularity are constant under non-rational holonomy, but a bounded invariant indicator has no such regularity a priori: one obtains an gradient for each angular Fourier coefficient separately, not a square-summable family, and must show each of these gradients vanishes.
Triangle is three affinely independent points of ℂ; table is the interior of their convex hull; side i is an open segment; angle i is the interior angle at vertex i via InnerProductGeometry.angle.ℂ × Circle with the product of normalized area on the table and the uniform angular probability (pushforward of normalized Lebesgue measure on ).FlightChain is a bi-infinite strictly increasing sequence of collision times, unbounded in both directions, with collisions in open sides, straight flights through the open table, and specular reflection reflect across the side tangent. billiardFlow follows the unique chain if one exists and is the identity otherwise; the theorem must prove the singular set is null.A complete development needs the geometry of unfolding, the null measure of vertex-hitting trajectories, Liouville measure preservation for billiards, angular Fourier decomposition on the doubled triangle, and holonomy arguments. Formalizing the well-posedness clauses alone (measure preservation and the a.e. flow property) is reusable for all polygonal billiards and is a welcome first contribution.
Chemical reaction network theory studies the polynomial differential equations that describe concentrations of interacting species under mass-action kinetics, where each reaction proceeds at a rate proportional to the product of the concentrations of its reactants. A central theme is which properties of the dynamics are forced by the structure of the reaction graph alone, independently of the (usually unknown) rate constants. Weak reversibility — every reaction can be undone by some directed path of reactions — is the main structural condition in this theory. Two long-standing conjectures ask whether weak reversibility alone guarantees that no species dies out (persistence) and that no concentration grows without bound (boundedness). These questions matter for systems biology and chemical engineering, where extinction of a species or unbounded growth would contradict the modeled behavior, and they are closely tied to the global attractor conjecture for complex-balanced systems.
Fix species. A reaction network consists of a finite set of complexes and a set of reactions with , . It is weakly reversible if for every reaction there is a directed path of reactions from back to . Given positive rate constants , the mass-action system is
A positive trajectory is persistent if for every .
In Lean (namespace OAI.Problem326), a ReactionNetwork d has a Finset of complexes in Fin d → ℕ and a Finset of reactions between them with distinct source and target; WeaklyReversible is Relation.TransGen reachability from target back to source; massAction N κ is the vector field above; and IsGlobalForwardSolution N κ x0 x means and has derivative at every .
Let , let the network be weakly reversible and all rates positive. For every the solution with exists for all , and there is , depending on the network, the rates and , such that
The goal is published on the platform with status Open.
The result itself. The theorem proves the boundedness conjecture and the persistence conjecture together, for arbitrary constant positive rates, any number of linkage classes and any number of species; earlier results needed a single linkage class, two species, or a two-dimensional stoichiometric subspace. It applies whether or not the stoichiometric compatibility class is bounded. Combined with complex balance, it yields convergence to the unique positive equilibrium in each class (the global attractor conclusion; Remark 3.5, p. 15). The proof also produces, for each positive initial point, a compact convex forward-invariant polytope in the open orthant (Proposition 3.3, p. 13), which gives a short proof of Boros's existence theorem for positive equilibria (Corollary 3.4, p. 14).
Formalizing it. Statements about reaction networks quantify over all networks and all rates, so they are a natural fit for formal verification; the history includes a published proof with a gap in one step. A machine-checked proof would settle the status of the general theorem independently of that history.
The natural approach is to find a Lyapunov function or an invariant region whose boundary each reaction crosses inward. Individual reactions need not point inward across any fixed face, and near the orthant boundary and at infinity different monomials dominate in different regions, with ties between monomials that an arbitrary choice of face normal can reverse. The argument must control the combined flux across cuts of the reaction graph using the return paths given by weak reversibility, and must do so simultaneously for small and large concentrations; a naive comparison of monomials by total degree fails, as the source's example with shows.
Fin d → ℕ, so exponents are nonnegative integers and is a polynomial vector field on ; the reaction set is a Finset with source ≠ target. Empty reaction sets and isolated complexes are allowed, as in the source.∀ e, 0 < κ e; is a hypothesis.ℝ → (Fin d → ℝ) with HasDerivAt at every , including a two-sided derivative at .A self-similar measure on the line is the natural probability measure on the attractor of finitely many contracting similarities , chosen with probabilities . Self-similar measures are the basic test case for fractal dimension theory; Bernoulli convolutions, the laws of , are the classical example. When the pieces are well separated, the dimension is given by the entropy-to-Lyapunov formula . When they overlap, dimension can drop, and the question is exactly how much. If two compositions of the same length coincide as maps (an exact overlap), information is genuinely lost; the entropy-rate dimension conjecture, formulated in Varjú's survey, predicts that this is the only mechanism: the dimension equals , where is the entropy rate of the random walk on composed maps.
This mission asks for a formal proof of that formula, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
Let be a finite nonempty alphabet and with , ; different symbols may give the same map, and ratios may be negative and unequal. Let be a probability vector with all . The self-similar measure is the Borel probability measure with
For a word let , and let be the random affine map when the letters are independent with law . With logarithms in base ,
where is Shannon entropy of the distribution of the map (coinciding words are merged). The lower Hausdorff dimension of is . The system has no exact overlaps if distinct words of the same length give distinct maps.
If there are no exact overlaps, the attractor is compact and nonempty, the equation has a unique solution , and .
If for all and there are no exact overlaps, then .
For every such family and every strictly positive probability vector ,
No separation assumption is made; exact overlaps and repeated generators are allowed.
The result itself. It removes every arithmetic and separation hypothesis from the dimension theory of self-similar measures on the line: the only way dimension can drop below is through exact overlaps, and then the drop is exactly measured by the map entropy. Without exact overlaps it gives the classical formula (Corollary 6.2, p. 19), and hence the dimension of every self-similar set without exact overlaps (Corollary 6.3), which is the exact-overlaps conjecture for sets. It asserts nothing about absolute continuity.
Formalizing it. Hausdorff dimension and self-similar measures exist only partially in Mathlib, and the proof needs a quantitative entropy calculus for finite laws at multiple scales. A formal proof would certify the general theorem together with the consequences that previously required separate arithmetic hypotheses. The only external input is the Feng–Hu exact-dimensionality theorem.
Hochman's method yields the formula under exponential separation of cylinders, but Baker and Bárány–Käenmäki showed that without exact overlaps cylinders can still come superexponentially close, so no lower bound on the separation is available, and exact overlaps add further collisions. The proof must therefore detect entropy hidden at arbitrarily fine scales with no control on the smallest positive distance. The preprint does this with a finite-law pair estimate independent of minimal separation (Lemma 3.2, p. 9), conditioning on block types to recover the map-entropy rate when addresses collide (Lemma 4.1, p. 13), and disjoint windows of entropy gain whose depths are chosen adaptively (Section 5).
System ι over a nonempty Fintype ι carries ratio, offset, weight with , , . SelfSimilar S μ is the equation for a probability measure on .wordAffine composes maps as and records (slope, translation); mapMass merges words with equal complete maps; walkEntropy n is base-2 Shannon entropy of ; entropyRate is the sInf over of ; lyapunov is base-2.lowerHausdorffDimension μ is an iInf in ℝ≥0∞ of dimH E over measurable with ; the goal compares it to ENNReal.ofReal (min 1 (h/χ)).NoExactOverlaps is injectivity of wordAffine on all words; words of different lengths always differ in slope modulus, so this matches the same-length condition of the source. The homogeneous milestone allows a single map, a degenerate case where both sides are .codingPoint and word functions, equivalent to the definitions above.Mixing is the basic notion of asymptotic independence in ergodic theory: a measure-preserving transformation is mixing if the event at time and the event at time become independent as . Mixing of order asks the same for events at times whose gaps all tend to infinity. In 1949 Rokhlin introduced higher-order mixing and asked whether mixing (order ) already implies mixing of order , and hence of all orders. The question has been one of the oldest in ergodic theory. It matters because higher-order mixing is the property used to prove multiple recurrence and independence statements, and because for actions of the analogous implication is false.
The source of this mission, an OpenAI preprint dated September 23, 2026, claims an affirmative answer for a single invertible transformation.
Let be a probability space and an invertible measurable map with measurable inverse that preserves . is mixing if for all
For , is mixing of order if for all
whenever and ; by invariance one may take . The order counts the number of sets (so order is "multiplicity " in Rokhlin's and Ryzhikov's convention).
If is an invertible mixing probability-preserving transformation, then for every and all measurable ,
the ranging over positive integers. No standardness or countable-generation assumption is made on . The Lean statement OAI.Rokhlin.mixing_all_finite_orders is open on the platform.
The theorem resolves Rokhlin's multiple-mixing problem for one transformation: mixing implies mixing of all orders, with no structural hypothesis (rank, spectrum, algebraic form). It explains the difference between and : Ledrappier's example shows the implication fails for several commuting generators. The paper also derives the conclusion for mixing endomorphisms and for mixing flows with strongly continuous Koopman operators (Corollary 8.1).
The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. Given the age and prominence of the problem, an independent formal verification would be valuable.
A failure of threefold mixing produces, in the limit, a joining of three copies of the system that is pairwise independent but not the product. Pairwise independence alone does not force a joining to be a product, so soft joining arguments do not suffice; earlier positive results used rank, spectral or algebraic structure to exclude such joinings. A reduction to zero entropy is available (positive-entropy parts are handled separately), but in zero entropy the non-product joining must be ruled out with no structural information about . In addition, the general (non-standard) probability space prevents direct use of disintegration and Rokhlin–Halmos-type tools without first reducing to a separable factor.
MeasurableSpace; has IsProbabilityMeasure; is a MeasurableEquiv with MeasurePreserving T μ μ.timeMap T n is the -th power of as a permutation, ; IsMixing μ T uses the filter comap Int.natAbs atTop on .MixingOfOrder μ T k: for every family of measurable sets indexed by Fin k, the measure of tends to along atTop on Fin (k-1) → ℕ+, where layoutTime gives the partial sums of the gaps.A complete development needs joinings, factor maps and entropy (Pinsker factor), measurable selection or a reduction to standard spaces, and the paper's array and operator machinery. Contributions formalizing the reduction steps (Proposition 2.1, zero-entropy witness) or classical special cases (Kalikow's rank-one theorem) are welcome.
A measure-preserving transformation of a probability space acts on square-integrable functions by the Koopman operator , a unitary operator. Its spectral type (discrete, singular continuous, absolutely continuous) and its multiplicity are basic invariants of ergodic theory. The Lebesgue spectrum is the spectral type of the shift on , the type of Bernoulli shifts and other strongly chaotic systems, where it occurs with infinite multiplicity. Banach's problem asks whether Lebesgue spectrum can occur with multiplicity one: is there a transformation whose Koopman operator on the orthogonal complement of the constants is unitarily equivalent to multiplication by on ? Equivalently, is there a single function whose bilateral orbit under is an orthonormal basis of the mean-zero space? The problem combines spectral theory with the construction of explicit dynamics, and a smooth example would show this spectral behavior is compatible with the regularity of differentiable dynamics.
Let and let be normalized Lebesgue (Haar) measure on . A bijection is a diffeomorphism if and lift locally to maps of . It is volume preserving if for every measurable . Let be the closed subspace of complex square-integrable functions with integral zero, and . Let be Haar measure on the circle and the first Fourier character.
In Lean (namespace OAI.ThreeTorus), the torus is Fin 3 → UnitAddCircle with the product Haar measure, smoothness is local smooth lifting on Fin 3 → ℝ, is the subspace meanZero of Lp ℂ 2 μ, and MainConclusion packages the theorem below.
There exist a volume-preserving diffeomorphism of and a real-valued such that
moreover is ergodic, and there is a unitary with
The goal is published on the platform with status Open.
The result itself. The theorem answers the probability-preserving form of Banach's problem, with the strongest kind of example: the invariant measure is the standard smooth volume on a compact manifold, the map is , and the conclusion covers the whole mean-zero space, both spectral type and multiplicity. Earlier work produced Lebesgue components, Lebesgue spectrum of higher multiplicity, simple spectrum of other types, flows, or infinite-measure examples; time- maps of simple-Lebesgue flows have infinite multiplicity, so they do not answer the question. The source also derives from it mixing (of all orders, using a separate companion multiple-mixing theorem), zero Kolmogorov–Sinai entropy (via Rokhlin's finite-multiplicity entropy theorem) and vanishing Lyapunov exponents (Corollary 6.1, p. 28).
Formalizing it. The statement exercises Mathlib's spaces, Haar measure on the additive circle, ergodicity and Fourier characters together. A formal proof would certify a long quantitative construction (successive smooth passages, stationary-phase estimates, Fourier signals) whose convergence must be checked simultaneously in the topology and in spectral norms.
Smooth constructions by successive conjugation (Anosov–Katok type) naturally produce maps with singular or discrete spectral behavior, because each approximating map is close to a rotation or an integrable twist with pure point or very structured spectrum. Lebesgue spectral type requires the spectral measure of every function to be absolutely continuous with the right density, and simplicity requires a single orbit to span the whole space. Making both hold in the limit, while keeping the limit map , requires controlling spectral densities at every scale and approximating every target function by translates of one fixed vector — the step where generic perturbation arguments give no control.
Fin 3 → UnitAddCircle with Measure.pi of AddCircle.haarAddCircle; is an Equiv.Perm with Smooth T and Smooth T.symm (local lifts), and MeasurePreserving T μ μ.Lp ℂ 2 μ with zero integral; is real-valued almost everywhere. The orbit is required to be orthonormal with dense span, i.e. a Hilbert basis indexed by .W : H₀ ≃ₗᵢ[ℂ] CircleH intertwining composition with and multiplication by fourier 1. Ergodicity is Mathlib's Ergodic T μ.A limit cycle of a planar vector field is a periodic orbit that is isolated among periodic orbits. The second part of Hilbert's sixteenth problem asks how many limit cycles a polynomial vector field of a given degree can have, and it is open even for quadratic fields. The classical Liénard systems
equivalent to the oscillator equation , are the most studied restricted family. In 1977 Lins, de Melo and Pugh conjectured that for the maximum number of limit cycles is . The conjecture is now known to fail for , holds for , and degree five was the remaining undecided case, where it predicts exactly two.
This mission asks for a formal proof of the degree-five bound and its sharpness, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
For a real polynomial (the primitive of the damping), consider the vector field on . A solution is a differentiable with for all . A periodic orbit is the image of a nonconstant solution that is periodic with some period . A limit cycle is a periodic orbit having an open neighbourhood such that every periodic orbit contained in equals . Limit cycles are counted as sets: once each, regardless of multiplicity, stability or hyperbolicity. The periodic orbits of a centre are not limit cycles.
For every real polynomial with ,
and some with has exactly two limit cycles. No parity, coefficient-sign, hyperbolicity or amplitude restriction is imposed.
The result itself. It decides the last open degree of the Lins–de Melo–Pugh conjecture in the affirmative, so the conjecture is true exactly for . Unlike the slow–fast result of Li and Lu, it bounds all cycles of every quintic system, including degenerate (multiple) ones and cycles of large amplitude. The preprint also corrects a proposed four-cycle quintic example from the literature by identifying it with a family known to have exactly two periodic solutions (p. 2).
Formalizing it. The statement uses only polynomials, ODE solutions and planar topology, so it is well suited to formal verification, and it would be one of the first machine-checked global limit-cycle bounds for a nonlinear family. The proof's general comparison results for smooth profiles (Propositions 5.2 and 5.3, pp. 32–34) and the global quadratic fit (Theorem 3.6, p. 18) are independent of the polynomial application and reusable.
Small-amplitude (Hopf/Melnikov) calculations only control cycles near the origin or near a perturbation of a centre; they say nothing about distant cycles. The even coefficients of prevent the reduction to the odd quintic family settled by Rychkov. Generic-perturbation arguments that remove multiple cycles cannot be used, since the count must include degenerate cycles. The preprint keeps the two half-orbits separate, writes each as an arch in coordinates valid at every amplitude, fits each arch by a quadratic comparison profile (Theorem 3.6), and controls how the fitted parameters move with width through a Schwarzian-type model inequality (Theorem 4.1, p. 20). Periodic orbits then become zeros of a single matching function (Proposition 2.5, p. 10), whose isolated zeros are bounded using an integrating factor (Section 6).
ℝ × ℝ; vectorField F z = (z.2 - F.eval z.1, -z.1) with F : Polynomial ℝ and F.degree ≤ 5 (this includes constants and the zero polynomial, which have no limit cycles).IsSolution requires HasDerivAt at every real time; IsPeriodicOrbit asks for a solution, a period T > 0, non-constancy, and C = range z.IsLimitCycle F C is a periodic orbit with an open U ⊇ C such that every periodic orbit C' ⊆ U equals C.Set.encard on the set of limit cycles, so infinitely many would give ⊤; the goal asks for ≤ 2 for every admissible F and = 2 for some.Welcome contributions: existence and smooth dependence of return maps for planar polynomial flows, and the energy-identity first-order return calculation used for sharpness (Section 7, p. 39).
An exact linear equation can carry arbitrarily fine real information: independent Gaussian equations determine a vector almost surely. A streaming learner that keeps only finitely many persistent states cannot retain those equations at arbitrary precision. The question is how many fresh equations such a learner needs to estimate a direction to angular accuracy when the information passed between observations is bounded in bits.
This preprint proves an explicit answer for memory : at least samples, uniformly in . With real-valued registers, randomized Kaczmarz needs only order samples, so the bound shows that bounded memory cannot beat that scale.
Fix , , , and . For a signal the observations are independent and exactly. A finite-state Gaussian stream learner reads the pairs in order; at every index its persistent state has at most values. Transition and stopping rules may depend on the index, , the current state, the whole current pair and fresh randomness, with unrestricted computation. It stops at some and outputs from the terminal state, and fresh randomness. A shared seed may choose the rules; seed and initial state are independent of the signal and rows. The experiment is jointly measurable.
For a linear space and , with , the affine subsphere is a test set of dimension . A block of exact Gaussian rows leaves the target, conditionally, uniform on a random residual subsphere of dimension .
In Lean (OAI.SubsphereCurrent), learners are SeededLearner d M T Ω built from KernelLearners (Markov-kernel transitions on completed observations, states Fin (2^M)), with Admissible measurability, uniformSuccess and per-signal success.
full_current_main_scopeThe conjunction of the paper's main statements:
The result. Theorem 1.2 gives explicit constants for the memory–sample bound with exact Gaussian observations and memory, e.g. at accuracy . The block estimates are statements about uniform measures on random affine subspheres that are independent of the learning application.
Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. Companion missions on the same family of preprints (memory and precision, posterior replicas, projection moments) share the learner model; this one is distinguished by explicit constants.
Conditioning on an exact Gaussian block makes the posterior of the signal singular: it is uniform on a lower-dimensional residual subsphere determined by the data. Density-based information arguments therefore fail after one block. The bound must control the success probability of the remaining computation, started from any state, averaged over every affine subsphere of large dimension, uniformly over learners that may process each real-valued pair without limit.
Vector d = EuclideanSpace ℝ (Fin d), signals in the unit sphere with normalized surface measure, rows i.i.d. stdGaussian.ℝ≥0∞; the constant is written (2:ℝ)⁻¹ ^ 16 and the logarithm is Real.logb 2.d/16, d/32, d/8; the fixed-length estimate uses Fin (2^(d^2)) states.The goal cannot be satisfied vacuously: hypotheses range over all admissible learners and the success thresholds are attainable with large .
Needed infrastructure: Haar measure on Grassmannians or orthogonal groups, beta laws of projected directions, spherical caps, measurable selection of Borel rule versions. Contributions proving individual conjuncts are welcome.
A finite message chosen from data changes the conditional distribution of those data. In memory-constrained inference this matters directly: a learner observing a signal through exact Gaussian equations keeps a finite state , and after conditioning on the rows that were used to select it are biased. An independent Gaussian matrix has the same unconditional law as those rows, but once its labels are revealed it need not leave the same information about .
This preprint quantifies the cost of that replacement. For a uniform signal on the sphere and a message of entropy at most , replacing the actual rows by fresh independent rows increases the remaining conditional information by at most . As an application, learners with persistent bits need exact Gaussian observations to reach angular accuracy .
Let be uniform probability on , the law of a matrix with i.i.d. entries, discrete entropy and conditional mutual information, all in nats. Put
Let and be independent, and let be a countable message with an arbitrary joint law with .
In Lean (OAI.CurrentProjection), the joint law of is a probability measure P on (Sphere d × W) × Rows (d/10) d whose marginal is uniformSphere d ⊗ gaussianRows (d/10) d; alignedExperiment and P.fst.prod (gaussianRows ...) are the two experiments; exposedInformation is computed as a relative entropy via condKernel; shannonEntropy is .
There are an absolute and such that for and every such countable with ,
with an exact-density version when .
The result. Theorem 4.1 converts a statement about the actual, selection-biased rows into one about fresh rows at an additive cost of , which is the step that lets block-by-block information bounds be iterated along a stream. With the residual-sphere endpoint it gives the lower bound for learners with bits (Theorem 8.4, Corollary 8.7). The mixed projection moment (Theorem 3.1) is a reusable estimate on exact Gaussian projections of measures with local mass control.
Formalizing it. All results are in an unrefereed preprint, with no machine-checked proofs. The streaming theorems themselves (Theorem 8.4, Theorem 8.6, Corollary 8.7) are not among the published Lean targets and remain future work.
Conditioning on biases in a way that depends on the unknown signal, so the two experiments have different joint laws even though their and marginals agree. A direct comparison of densities fails because the exact label density under the actual law can be large on a selection-dependent set; controlling it requires a high moment of the projected density with the row-information charge entering only with coefficient .
Metric.sphere (0 : EuclideanSpace ℝ (Fin d)) 1 with normalized surface measure; rows are Fin k → EuclideanSpace ℝ (Fin d) with stdGaussian entries.ℝ≥0∞-valued.d/10, d/2 - d/10, d/32, d/8, d/4, d/3 as in each source statement.The goal is not vacuous: it quantifies over all joint laws with the stated marginal and entropy bound, and the right side is finite for many of them.
Needed infrastructure: conditional mutual information for standard Borel variables, chain rules, exact density versions of Gaussian projections, local mass bounds on the sphere. Contributions toward any milestone are welcome.
A linear projection can concentrate a measure even when the measure has no atoms; how much depends on how much mass sits near the affine subspaces that the projection collapses. Quantitative versions of this principle go back to the potential-theoretic projection method of Kaufman and Mattila, which relates ball-growth bounds to the behaviour of projections. This preprint proves explicit, dimension-dependent versions for random exact projections and applies them to a learning question: how many noiseless Gaussian measurements does a learner with bits of memory need to recover a unit vector to angular accuracy ?
The answer proved here is that bits force measurements, matching the real-valued randomized Kaczmarz scale, and more generally for every .
Let be uniform probability on . A finite measure on satisfies an all-ball mass bound with constants if for every ball. For an orthonormal -frame , is the image measure on and its density. The Riesz functional of is .
In the finite-state regression experiment, the signal ; at each step a row arrives with its exact label . A learner keeps one of states, may use arbitrary measurable randomized transitions of the current state and pair, stops by a deterministic horizon , and outputs a unit vector from its terminal state, stopping index and fresh randomness. Success means .
In Lean (OAI.ProjectionMoments, OAI.NoiselessRegression), learners are FiniteKernelLearner d M T (Markov-kernel transitions on completed observations, states Fin (2^M)), mixed over a seed space Ξ with probability ρ; seededSuccess is uniform-prior success; AllBallMass ν K β, coordinateDensity, frameLaw, capMeasure, rieszPotential encode the geometric objects.
OAI.ProjectionMoments.mainA conjunction of the paper's results, including:
also under an every-signal guarantee.
The result. The projection moment estimates are general statements about finite measures with ball-growth control and apply beyond learning. In the learning application they give three proofs, with different stopping and accuracy costs, that bits cannot beat the sample scale for exact Gaussian measurements, plus an explicit trade-off for all .
Formalizing it. The results are in an unrefereed preprint; there is no machine-checked proof. The conjunct FixedQuadraticMemory coincides with part of the goal of the companion mission on Memory and precision in noiseless Gaussian regression, so progress here is shared.
Integrated density norms do not determine density values on a matrix-dependent graph, so pointwise statements need an explicitly chosen density version. The high moments of projected densities require controlling collisions of independent points under projection, which leads to inverse affine heights whose integrability must be extracted from the ball-growth hypothesis at all scales. In the learning application, conditioning on an exact label produces a singular posterior, so arguments that track a posterior density fail.
EuclideanSpace ℝ (Fin d); frames are orthonormal families Fin k → E drawn by frameLaw; densities are ℝ≥0∞-valued with explicit measurable versions.d/4, d/8, d/16); block counts appear as (T+k-1)/k.FiniteKernelLearner with CompletedRules almost surely in the seed; success probabilities are ℝ≥0∞.The goal has no trivial reading: each conjunct quantifies over all measures or learners satisfying the stated hypotheses, and the hypotheses are satisfiable.
Needed infrastructure: Stiefel and Haar measures, Gaussian polar decomposition of matrices, Gram–Schmidt Jacobians, spherical caps, Riesz potentials. Contributions proving individual conjuncts (for example Theorem 3.3) are welcome.
An exact linear observation of a real signal can carry arbitrarily many bits. A finite message computed from a block of such observations cannot, but its information content is not controlled by the number of observations alone: if earlier messages have already concentrated the signal in a small region, the next block can exploit that concentration. Bounds of this kind are the engine of memory–sample lower bounds for noiseless Gaussian regression, where a learner with bits of memory must recover a unit vector to angular accuracy from a stream of exact Gaussian measurements.
This preprint asks how to restore a geometric spread condition on the posterior while paying for the information revealed in doing so, and proves that, for a cube-shaped prior on a spherical patch, blocks of exact measurements with messages of at most values reveal only nats.
Let be large, , , . The cube prior is normalized Lebesgue measure on the half-open cube , and the chart maps it into . Dyadic cells of level subdivide into half-open subcubes of side .
Draw . In block an independent standard Gaussian matrix is drawn, and is observed exactly. A message is drawn from a Borel probability kernel of the block data, whose choice may depend on the preceding messages . Information is measured in nats by mutual information , defined as a relative entropy.
In Lean (OAI.RepeatedLocalization), Coordinate n = Fin n → ℝ, cubePrior n is Lebesgue measure conditioned on initialCube n, chart is , a Cell n is a level with a multi-index in Fin (2^J), a BlockRule n N is a measurable probability vector on Fin N indexed by block data, Rules n N t chooses a rule for each block from the past history, and experimentLaw rules is the joint law of .
repeated_localizationThere is an absolute such that for every there is with the following property, for large. If
then one can reveal nested dyadic cells containing , with a finite-valued measurable function of and , such that the augmented transcript satisfies
where is the level of . An alphabet of size satisfies the hypothesis with depending only on .
The result. Theorem 3.2 is the first information estimate in the paper and the model for its later routes: it shows that revealing a nested dyadic cell after each block, which restores the spread condition needed by the projection estimate, costs only nats per block. Since the original message history is a function of , the bound also controls the information in the messages alone. Combined with the paper's endpoint arguments this yields the lower bound for learners with bits.
Formalizing it. These results are proved only in an unrefereed preprint; no machine-checked proofs exist. The milestones are independent analytic statements (an entropy regularization, a convex potential and its drift, an inverse-volume moment) that are reusable in the companion missions on exact Gaussian observations.
The information a block reveals depends on how concentrated the current posterior is, and earlier messages can make it arbitrarily concentrated. Simply conditioning on messages gives no control. Revealing a localizing cell restores spread, but naming a cell itself costs information, and the count of candidate cells at depth grows like ; the argument must show that confinement to a depth- cell (worth bits relative to the prior) pays for this, uniformly over all message rules.
Fin n → ℝ, and appears as n + 1.n / 16, n / 8. Gaussian entries are gaussianReal 0 1.Q : Disclosure n N t is valid when each cell map is measurable with finite range, contains , lies in , and the cells are nested. The goal asserts existence of a valid disclosure with mutualInformation (augmentedLaw rules Q) ≤ C (n+1) t and expected final level at most .klDiv of the joint law against the product of marginals, valued in ℝ≥0∞.The goal is not trivial: the trivial disclosure (always ) does not bound the information in arbitrary messages, and the quantifier order (absolute , then , then ) matches the source.
Needed infrastructure: Gaussian projections of measures on cells, density bounds, dyadic cell combinatorics, and relative-entropy chain rules. Contributions toward any milestone are welcome.
Suppose an unknown unit vector is observed through exact linear measurements with independent Gaussian rows . If every pair is kept, rows determine . A learner that can keep only a bounded number of bits between measurements must compress each exact real label into a state update, and the question is how many measurements this costs for a prescribed angular accuracy . Exact labels make the question delicate: a real label has no built-in bit precision, so noise-based arguments do not apply.
This preprint attacks the question through a conditional information bound for a single block of observations: how much information about can a finite message formed from exact Gaussian measurements carry, beyond what an independent Gaussian projection of (revealed only to the analyst) already reveals? Iterating such a block bound over a stream gives a memory–sample lower bound.
Let be uniform probability on . In a block experiment the signal has law with a Borel density . Independently draw a standard Gaussian matrix and observe . A message with values in a finite set is drawn from a measurable Markov kernel of . Finally an standard Gaussian matrix is drawn independently of everything. The quantity of interest is the conditional mutual information
in nats, and denotes the Shannon entropy of the message.
A finite-state learner with bits reads pairs once, in order, keeps a state in a set of size , may stop at any index up to a deterministic horizon , and outputs a unit vector from its terminal state, stopping index and fresh randomness only. Transitions and stopping may be arbitrary measurable randomized rules of the current state and current pair; shared randomness is independent of the signal and samples.
In Lean (OAI.PosteriorReplicas), sphereLaw d is normalized surface measure, gaussianRows d k is the product of stdGaussian, signalMessageLaw p κ is the law of , sideLaw ℓ appends , conditionalInformation is the relative entropy of the joint law from the conditionally independent coupling, and messageEntropy is . Learners are CompletedKernelLearner d M with Markov-kernel transitions on the completed observation space, wrapped in a JointKernelExperiment over a seed space .
OAI.PosteriorReplicas.source_mainThe goal is the conjunction of the paper's principal statements:
uniformly over the prior, , and the message kernel.
The result. Theorem 1.2 shows that with persistent bits, the sample scale of real-valued Kaczmarz-type methods cannot be improved for exact Gaussian measurements, under the uniform prior and with an absolute constant. Theorem 1.1 is a reusable statement in its own right: the entropy of a message is divided by a factor proportional to , and the dependence on the prior density bound is only doubly logarithmic, which is what allows conditioning on rare learner states.
Formalizing it. These results appear only in an unrefereed preprint, and none has a machine-checked proof. The companion preprint Memory and precision in noiseless Gaussian regression proves a related statement for memory by a different method; the two missions share the learner model but not the block estimates. Formalizing the goal requires conditional mutual information for general (non-discrete) random variables and the exact equal-label geometry, both of which would be reusable.
Conditioning on one exact observation confines the signal to a lower-dimensional section of the sphere, so posterior densities with respect to do not exist and density-based arguments fail. Bounding the information in the message by alone is far too weak: a message of bits could then carry all relevant information. The block bound must instead account for what the analyst's independent projection already reveals, uniformly over priors with large density bounds , since rare learner states produce such priors.
EuclideanSpace ℝ (Fin d); priors are measures on the ambient space given as (sphereLaw d).withDensity f with .Fin N with NeZero N; information quantities are ℝ≥0∞-valued relative entropies (klDiv), entropies use natural logarithms.2 * (d / 16), d / 8, d / 2 as in the paper.IsLittleO atTop M (d^2), all horizons , all , all seed spaces and all JointKernelExperiments whose output kernel agrees almost surely with the run of the per-seed learner.The goal cannot be met vacuously: block bounds are stated for every finite message kernel, and the streaming hypothesis (success at least ) is satisfiable by learners with large .
A complete development needs Gaussian matrices and their projections, coarea-type identities for equal labels, conditional kernels (condKernel), relative entropy chain rules, and spherical measure estimates. Contributions that isolate one conjunct (for example Theorem 3.3 or Theorem 1.1) are welcome.
A single exact linear equation about an unknown unit vector carries arbitrarily fine information: independent Gaussian equations determine almost surely, provided all of them can be kept. A learner that reads the equations once, in order, and keeps only a bounded number of bits between them faces a different problem. The question asked here is how many noiseless measurements such a learner needs in order to reach a prescribed angular precision , as a function of its memory.
This is a question about memory–sample trade-offs: how much a bound on persistent memory forces a learning procedure to read more data. With unbounded real registers, the randomized Kaczmarz update satisfies on isotropic Gaussian rows, so order samples suffice. That update stores real numbers and gives no finite-bit upper bound; the question is whether a learner with roughly bits can do better than this scale.
Fix integers , , . A signal lies on the unit sphere . At step the learner receives the pair with independent and exactly (no noise).
A finite-state learner with bits keeps a state in a set of at most elements. A data-independent shared seed (drawn from a probability space ) may select its rules. Given the seed, the current state, the step index and the current pair, a transition chooses the next state and whether to stop; it may perform unrestricted computation but retains only the next state. The learner must stop by the deterministic horizon . Its output is a function of the terminal state, the stopping index and the seed only; a discarded observation cannot be read again. Success at precision means angular error .
Write for the uniform probability measure on . Uniform success is the probability of success when is drawn independently of the rows and the seed.
In Lean (OAI.NoiselessRegression), the state space is Fin (2 ^ M), a learner is a structure Learner d M T Ω with fields initialChoice, transition, output, the sample law is the product of stdGaussian on EuclideanSpace ℝ (Fin d), and uniformSuccess and success are the probabilities defined above. Randomness during the run is represented through the arbitrary seed space .
OAI.NoiselessRegression.mainThe goal is the conjunction of two statements.
Fixed quadratic memory (Theorem 1.2): for every there are and such that, for , , , and every admissible learner,
Subquadratic memory (Corollaries 1.3 and 1.4): there is an absolute such that for every memory sequence there is with the same conclusion for , under either uniform success at least or success at least for every fixed signal .
No relation between and is assumed; the constant is absolute in the subquadratic case.
OAI.MemoryPrecision.main)A single bundled statement collecting the paper's projection-density and backward-block estimates (Theorem 3.1, Propositions A.1, A.4, A.5, B.6, B.7, Corollary 8.2), the cube-prior precision bound (Proposition 8.3), and the explicit success bound after a bounded number of samples (Proposition 5.3):
The result. Theorem 1.2 answers, for exact observations and isotropic Gaussian rows, the precision question raised in Section 1.1 of Sharan–Sidford–Valiant: with bits, the scale achieved by real-valued Kaczmarz cannot be improved, uniformly over all . Because an exact-observation learner can simulate added noise, the preprint derives from it an lower bound in the noisy experiment of Sharan–Sidford–Valiant at accuracy , which strengthens their bound in that range.
Formalizing it. The result is proved only in an unrefereed preprint; no machine-checked proof exists. A formal proof would certify a lower bound whose model (randomized measurable rules, early stopping, shared seeds, measurability conventions) is delicate, and the conventions are already fixed in the Lean definitions. Remaining work: the full formal proof, and as a variant the every-signal version of Theorem 1.2 for fixed (Corollary 1.4), which the Lean goal states only in the subquadratic case.
Conditioning the uniform prior on one exact observation confines the signal to a hyperplane section of the sphere, a law singular with respect to the original spherical measure; information-theoretic arguments that track a posterior density therefore break down after a single step. Arguments for noisy observations, such as Sharan–Sidford–Valiant's, rely on the noise to keep posteriors spread out and do not transfer to the more informative exact experiment. The bound must also hold uniformly in with no relation between and , so a learner with bits must be prevented from storing bits per coordinate for very small .
EuclideanSpace ℝ (Fin d); signals and outputs in Metric.sphere 0 1. The uniform sphere law is the normalized toSphere measure; rows are i.i.d. stdGaussian.Fin (2 ^ M); the first component of each action is the stop flag. Runs that never stop are forced to terminate at index .Learner.Admissible requires a.e.-measurability of the initial choice, transitions (against Gaussian × Lebesgue on pairs), outputs, and of the full experiment under each fixed signal and under the uniform prior.ℝ≥0∞-valued; the threshold is ; angular error is Real.arccos ⟪ŝ, s⟫; is natural.u, so randomized learners are covered by placing their randomness in the seed.The goal cannot be satisfied trivially: the hypotheses range over all admissible learners, and the success threshold is achievable (with large ), so the implication has content.
A complete development needs Gaussian measures on Euclidean space, spherical measure and cap estimates, Gram determinants and affine distances, densities of Gaussian projections, and measurable selection of Borel versions of kernels. The projection-density estimates are reusable beyond this mission. Contributions toward the bundled milestone, or toward any of its component estimates, are welcome.
Iterated matrix multiplication asks for the entry of a product of matrices of size with independent variable entries,
It has polynomial-size arithmetic circuits when depth is unrestricted and is complete for algebraic branching programs, so it is the standard test case for the cost of restricting circuit depth. Depth-reduction theorems (Agrawal–Vinay, Koiran, Tavenas) show that any polynomial-size circuit for a degree- polynomial can be flattened to homogeneous depth four with size ; lower bounds of the form at small depth are therefore exactly at the threshold that depth reduction permits, and improving them slightly would separate general circuits from formulas. Nisan and Wigderson asked for an explicit homogeneous polynomial requiring superpolynomial size at constant depth, even at depth five.
These results either restrict the bottom linear forms, use a different width–degree regime, or concern a different polynomial. The source of this mission, an OpenAI preprint dated September 25, 2026, claims the sharp bound in the balanced regime with unrestricted bottom forms.
An arithmetic circuit over a field is a finite DAG whose leaves are variables or field elements; sum gates take -linear combinations of their inputs, product gates multiply their inputs (with multiplicity). A circuit has five layers of types from the output down, with a single output gate; edges join consecutive layers and bottom sums read leaves. Fan-in, fan-out and sharing are unrestricted, and bottom linear forms may involve any number of variables. The circuit is syntactically homogeneous if, with variables of degree , constants of degree and product degrees adding, every sum gate has all inputs of the same formal degree. Size is the number of vertices, leaves included. The target is , of degree in variables.
There is such that for all , every syntactically homogeneous circuit computing over , and more generally over any field of characteristic zero, has
Conversely, over every field and for every there is such a circuit with
The Lean statement OAI.Problem335.main bundles the three clauses and is open on the platform. The constant is the paper's and is not optimized.
The theorem determines the size of homogeneous depth-five circuits for up to the constant in the exponent: . It removes the bottom-support restriction of Bera–Chakrabarti and works at the balanced width–degree point , where the shifted-partials bounds of Amireddy et al. and the low-degree results of Limaye–Srinivasan–Tavenas do not apply directly. It answers the depth-five instance of the Nisan–Wigderson question for an explicit polynomial in VP. It does not give superpolynomial bounds for general circuits.
The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. The upper-bound clause is elementary and a natural first formal target; the lower bound requires a new rank measure and its estimates.
Depth-five circuits with unrestricted bottom linear forms can use linear forms involving all variables, which defeats measures that rely on bottom forms having small support (the Bera–Chakrabarti approach) or on set-multilinearization with degree-dependent losses (which are too costly when ). Partial-derivative and shifted-partial measures applied directly give bounds that degrade with the bottom fan-in. One needs a measure that is small for every product of homogeneous low-degree polynomials of arbitrary support and large for .
Depth5Circuit K n stores the leaves (D5Leaf: a scalar or a variable index in Fin n × Fin n × Fin n), bottom sums (lists of coefficient–leaf pairs), lower products (lists of bottom gates), middle sums, upper products, and one output sum, with explicit formal degrees and homogeneity constraints at every sum gate; empty sums have degree .circuitSize counts leaves plus all gates plus the output gate; circuitValue evaluates to an MvPolynomial.imm K n is the entry of the ordered product of the matrices .ℂ and, with a threshold chosen before the field, over every Field with CharZero; the upper bound over every Field, with the explicit upperGateBound.A complete development needs multivariate polynomial algebra, the derivative-multiplication operator and its rank, an integral (Bargmann–Fock type) moment estimate over , and a transfer to characteristic zero via integer minors. Contributions formalizing Proposition 6.2 (the upper bound) and Proposition 3.1 (the circuit-side rank bound) are welcome.