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 set is square-difference-free if no two of its elements differ by a perfect square with . The Furstenberg–Sárközy theorem says such sets have density tending to zero; the question is how fast. Writing for the largest size of a square-difference-free subset of , the problem is a prototype for polynomial patterns in dense sets: it is the simplest case of finding differences in the image of a polynomial, and it is the model problem on which Fourier-analytic, ergodic and density-increment methods for polynomial configurations are tested. A long-standing gap separates the upper bounds, which until recently saved only a power of (with a slowly growing exponent), from the lower bounds, which are powers and beyond. Whether a fixed power saving holds was posed explicitly by Green and Sawhney.
For a positive integer write . A set is square-difference-free if
that is, for all and all integers . (Differences are taken in ; is allowed since is excluded from the squares.)
In Lean (namespace OAI.SquareDifference), sets are Finset ℤ contained in Finset.Icc 1 N, and IsSquareDifferenceFree A states a - b ≠ (m : ℤ)^2 for all a b ∈ A and m : ℕ with 1 ≤ m.
There are absolute constants and such that for every integer and every square-difference-free ,
Equivalently, every subset of with more than elements contains two elements differing by a nonzero perfect square. The Lean goal is published on the platform with status Open. The statement fixes no numerical value of , so any improvement of the exponent leaves the goal unchanged.
The result itself. Every earlier upper bound saved less than any fixed power of ; the best, due to Green and Sawhney, saved . A fixed power saving changes the nature of the problem: it shows that the extremal exponent lies strictly below , so both upper and lower bounds are now polynomial and the remaining question is the value of the exponent, now known to lie between and . As an immediate consequence (Remark 1.2 of the source), the graph on joining integers differing by a square has chromatic number at least , a polynomial bound for the square-difference coloring problem.
Formalizing it. The statement is elementary and self-contained, involving only finite sets of integers. The proof combines a graph/tuple reformulation, reflection-positivity (chessboard) inequalities for a finite-field probability law, and an induction with fixed finite constructions. A formal proof would certify an argument whose constants are explicitly noted to be extremely small and not computed.
Density-increment arguments, starting from Sárközy's circle-method proof, gain a constant factor of density at each step but lose a power of the length of the progression on which they pass, so after the increments needed the saving is only logarithmic or quasi-logarithmic. The Green–Sawhney level- approach controls the relevant rational Fourier coefficients through hypercontractivity but still gives only . A power saving requires an argument whose loss does not compound with the number of iterations — a single estimate that converts square-difference-freeness into a polynomial density loss.
Finset ℤ inside Finset.Icc 1 N and is a natural number; the bound is uniform in .How efficiently can the edges of a graph be split into cycles? Some single edges must be allowed, since a forest has no cycles at all, and a tree on vertices already needs single-edge parts. The Erdős–Gallai cycle decomposition conjecture asserts that this is essentially the only obstruction: every graph on vertices can have its edge set partitioned into simple cycles and single edges. Equivalently, every graph with all degrees even partitions into cycles. The problem is a basic question about edge decompositions, and the partial bounds , and trace several decades of progress on it.
This mission asks for a formal proof of the linear bound, 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 finite simple graph has vertex set of size and edge set of unordered pairs of distinct vertices. A cycle is a closed walk of length at least with no repeated vertices except the endpoints; its edge set is the set of edges it traverses. A cycle-and-edge decomposition of into parts is a family of pairwise disjoint subsets of with union , where each is either the edge set of a cycle of or a single edge of . Parts may share vertices; isolated vertices need not be covered; for an edgeless graph is allowed.
There is an absolute constant such that for every and every simple graph on vertices,
The value of is left unspecified, which keeps the goal stable under future improvements of the constant (the best possible constant is at least , by complete bipartite examples).
The result itself. The order is optimal (trees). The theorem implies that every Eulerian graph (all degrees even) partitions into cycles (Corollary 1.2, p. 2), and via known equivalences it gives the sharp cycle bound for Eulerian graphs satisfying a large-cut condition. It removes the last iterated-logarithm loss from the Bucić–Montgomery bound.
Formalizing it. The statement uses only Mathlib's SimpleGraph.Walk.IsCycle and edge sets, so it is a clean combinatorial target. A complete development needs Lovász's path-cycle decomposition theorem, the Aharoni–Haxell hypergraph matching theorem, expansion and routing lemmas, and binomial tail bounds; all are reusable in extremal graph theory. No machine-checked proof of any bound is known.
Covering is easy (Pyber's bound), but a cover does not yield a partition: deleting repeated edges can break cycles into many paths. For partitions, the standard strategy decomposes the graph into expanding pieces at a sequence of scales, and paying a cost proportional to the full order at every scale accumulates a factor from the number of scales — this is where the and losses come from. The preprint (Introduction, pp. 2–3) charges the work on a prefix of scales to a single expanding layer and saves a fixed fraction of vertices by identifying pairs, then lifts quotient cycles back with reserved edge-disjoint routes (Lemma 3.1, p. 5); keeping a separate assignment for each original edge throughout is what makes the induction close.
SimpleGraph (Fin n) for arbitrary n (including 0 and edgeless graphs).CycleOrSingleEdge G s: either is p.edgeSet for some p : G.Walk v v with p.IsCycle (Mathlib cycles have length at least ), or for an edge .EdgeDecomposition G k: parts indexed by Fin k, each a cycle or single edge, pairwise disjoint, with union G.edgeSet.MainStatement: EdgeDecomposition G k .A Hadamard matrix of order is an matrix with entries whose rows are mutually orthogonal, . Such matrices are extremal for Hadamard's determinant bound and are used throughout coding theory, experimental design and signal processing. Imposing a circulant structure, where every row is a cyclic shift of the first, links the problem to cyclic difference sets and to binary sequences with ideal periodic autocorrelation. The order-4 example with first row is easy to find; the circulant Hadamard conjecture, traditionally attributed to Ryser (1963), asserts that apart from the trivial order 1 there are no others.
The question is closely tied to Barker sequences, binary sequences with the smallest possible aperiodic autocorrelations, which are used as radar pulse-compression codes. Only lengths are known, and the long-standing Barker-sequence conjecture says there are no others.
Several complete proofs have been claimed (Oh-Hashi 2016, Orozco López 2019, Morris 2023, Gallardo 2024, Manjhi–Kumar 2025). The source of this mission is an OpenAI preprint dated September 23, 2026, which proves the conjecture by an argument with cyclotomic character values over the group ring .
A real matrix is circulant if there is a function with , indices taken modulo . It is a sign Hadamard matrix if every entry is or and
For a circulant sign matrix with first row , the periodic autocorrelations are ; the Hadamard condition says for .
A Barker sequence of length is with aperiodic autocorrelations
The Lean statement OAI.CirculantHadamard.exists_iff_order_one_or_four is open on the platform.
Combined with the classical odd-length classification, this gives the Barker length list .
Theorem 1.1 closes a problem open since the early 1960s and, through the even-length reduction, completes the classification of Barker-sequence lengths. Equivalently, it shows that cyclic difference sets with parameters exist only for . It also explains, in a single statement, the computational evidence of Logan and Mossinghoff and the arithmetic restrictions of Turyn and of Leung–Schmidt.
The result is proved in an OpenAI preprint that has not been peer reviewed; given the number of earlier claimed proofs, an independent machine-checked proof would be especially valuable. No formal proof of either statement exists; the formalization would also produce reusable group-ring and cyclotomic machinery.
The orthogonality condition is a norm equation in the group ring , and every character sends to a cyclotomic integer of absolute value . Classical arguments use such character values one at a time, through factorization of ideals in cyclotomic fields, and stop at the case with odd and divisible by several primes. The obstruction must combine information from all prime divisors of simultaneously and use the fact that the coefficients are signs, not arbitrary integers; norm equations alone do have solutions at these orders.
RealMatrix n := Matrix (Fin n) (Fin n) ℝ; IsCirculant H asks for h : Fin n → ℝ with H i j = h (j - i), where subtraction in Fin n is modular.IsSignHadamard H is entrywise IsSign (equal to or ) together with H * H.transpose = (n : ℝ) • 1.0 < n, matching the paper's "positive integer ".Fin n → ℤ with IsSign entries and aperiodic h k = Σ_{j<n-k} h_j h_{j+k}, bounded by in absolute value for .A complete development needs group rings of finite cyclic groups, characters and cyclotomic integers, localization at primes above , and Kronecker's theorem that an algebraic integer all of whose conjugates have absolute value one is a root of unity. Contributions formalizing Proposition 2.2 (the order restriction , odd), Lemma 3.1 (character comparison) and Proposition 3.4 (alternating character products are roots of unity of odd order) are welcome.
An expander graph is a sparse graph in which every set of vertices has a large edge boundary relative to its size. Expanders with bounded degree are a basic tool across combinatorics, computer science and group theory. High-dimensional expanders are simplicial complexes that extend this behavior to faces of every dimension, and coboundary expansion over is the strongest of the standard notions: the coboundary of any set of -faces must be large unless the set is already close to a coboundary. Gromov connected such filling inequalities with topological overlap of maps to Euclidean space. The basic existence question is whether there are arbitrarily large complexes of fixed dimension with bounded vertex degree and uniform coboundary expansion in every degree.
A finite simplicial complex is a downward-closed family of finite sets (faces) of vertices; denotes the faces with vertices. is pure of dimension if it has -faces and every face lies in one. An -cochain is a function ; its coboundary is . Let , with the constant functions. Faces are weighted by
so is the probability that is nonzero on a random -face of a uniformly random top face, and .
In Lean (namespace OAI.CoboundaryExpanders), a Complex has vertex set Fin vertexCount, a Finset of faces that is downward closed and contains every singleton; Pure, Connected (connected -skeleton), weight, norm, coboundary, coboundaries and distance follow these definitions, and topDegree X d v counts -faces containing .
For every there are , and finite connected pure -dimensional complexes with , every vertex in at most faces of dimension , and
with constants independent of , and . The Lean goal is published on the platform with status Open.
The result itself. Together with the classical graph case and the Chapman–Lubotzky two-dimensional theorem, Theorem 1.1 gives bounded-degree coboundary expanders in every positive dimension, answering the existence question in the form stated by Chapman and Lubotzky. Earlier bounded-vertex-degree constructions gave cosystolic expansion, which permits nonvanishing cohomology, or degree-one expansion only; earlier coboundary expanders in all dimensions had vertex degrees growing with size. Coboundary expansion in all degrees implies vanishing -cohomology below the top dimension, the property Gromov related to topological overlap.
Formalizing it. The definitions are elementary finite combinatorics, so the statement is completely precise; the proof combines group-theoretic coset complexes over , congruence quotients and a quantitative cosystolic input. A formal proof would require formalizing that input (Oppenheim–Valentiner-Branth), which is substantial.
Coboundary expansion requires two things at once: a quantitative isoperimetric inequality against cocycles (cosystolic expansion) and exact vanishing of for every . Random constructions give vanishing cohomology but force growing vertex degree; algebraic bounded-degree constructions (Ramanujan complexes, coset complexes) give the quantitative inequality but typically have nonzero cohomology that cannot be controlled uniformly. A cocycle that is not a coboundary has zero coboundary and positive distance, so any nonzero cohomology class destroys the inequality. The difficulty is a family of bounded-degree complexes whose cohomology vanishes in every degree below , uniformly along the tower.
Fin vertexCount and every vertex is a face; faces are Finsets, and an -face has exactly vertices.ZMod 2-valued; is the constant cochains (reduced cohomology in degree ). Distance is a real sInf over the image of a nonempty finite set, hence a minimum.When does the Erdős–Rényi random graph contain a copy of a prescribed graph ? A necessary condition is visible from first moments: if some subgraph has expected copy count below a constant, then is unlikely to appear. Kahn and Kalai conjectured in 2007 that this elementary obstruction determines the containment threshold up to a logarithmic factor, uniformly over all target graphs, including spanning ones such as perfect matchings, Hamilton cycles or cubes (CPC 2007). Their abstract conjecture for general increasing families (the "first" conjecture) was proved by Park and Pham; the graph-specific "second" conjecture compares the threshold with the smaller, purely subgraph-count-based graph expectation threshold, and is not implied by the abstract theorem.
This mission asks for a formal proof of the second Kahn–Kalai conjecture with explicit constants, 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 finite simple graphs let be the number of subgraphs of isomorphic to (ordinary, non-induced copies). is the random graph on with each of the edges present independently with probability . For a graph with at least one edge and at most vertices,
The first is the containment threshold, the second the graph expectation threshold; always . Write for the number of edges.
For every and every finite simple graph with edges and at most vertices,
The constants are explicit and universal; may vary with .
The result itself. The bound says that, up to a universal constant times , the only obstruction to containing is a subgraph with too few expected copies. The logarithm cannot be removed: for a perfect matching while , because isolated vertices must disappear. This settles the problem left by the abstract Park–Pham theorem, whose bound is in terms of the possibly larger integral expectation threshold of the family of graphs containing .
Formalizing it. Both thresholds are finite, explicit optimization problems over Bernoulli product measures on the edges of , so the statement is fully elementary. Mathlib has SimpleGraph.copyCount but no random-graph or threshold theory; the spread-family resampling lemma and the tree covering theorem would be reusable for other threshold results (Park–Pham, Frankston–Kahn–Narayanan–Park). No machine-checked proof of any Kahn–Kalai-type theorem is known.
The abstract theorem compares with the integral expectation threshold of the family of edge sets containing a copy of , and covers of may be much cheaper than the copies of a single subgraph, so it does not give a bound in terms of . Previous graph-specific approaches lost extra logarithms because each conditional extension step paid the sampling cost again. The preprint (Section 1.2, pp. 3) builds a tree of nested subgraph extensions with geometrically growing, pairwise disjoint labels along each path, and must reuse one random set at every level of the tree while keeping the spread property under conditioning (Theorem 3.1, p. 6).
Finset (Edge n), where Edge n is the type of non-diagonal Sym2 (Fin n); expectations and probabilities are finite sums, defined for every real but used only on .expectedCopies and containmentProbability use Mathlib's copyCount of the graph built from the edge set; both are ordinary (non-induced) copies.criticalThreshold and expectationThreshold are sInf over ; the sets are nonempty (they contain when has at most vertices), so the infima are the true thresholds. The expectation constraint ranges over all H.Subgraphs, including subgraphs with isolated vertices, whose constraints are automatically satisfied.SimpleGraph on an arbitrary finite type V with Fintype.card V ≤ n, 2 ≤ n and at least one edge; logTwo is .A thin spanning tree of a graph is a spanning tree that uses only a small fraction of the edges of every cut. Thin trees were introduced for the asymmetric traveling salesman problem: Asadpour, Goemans, Mądry, Oveis Gharan and Saberi showed that a thin tree of low cost can be augmented into a cheap tour, giving an -approximation (doi:10.1287/opre.2017.1603). Goddyn conjectured that high edge connectivity forces thin trees; the strong thin tree conjecture asks for thinness in every -edge-connected multigraph. For applications one wants not just existence but an efficient algorithm that finds such a tree, also when parallel-edge multiplicities are huge and written in binary.
Background. The maximum-entropy rounding of Asadpour et al. constructs -thin trees. Oveis Gharan and Saberi constructed -thin trees on planar and bounded-genus graphs (2011, doi:10.1137/1.9781611973082.75). Anari and Oveis Gharan proved existence of -thin trees in general (2015, arXiv:1411.4613), without a polynomial-time construction. Klein and Olver (2023, doi:10.1109/FOCS57990.2023.00011) and Klein, Olver and Yeoh (2026, doi:10.4230/LIPIcs.ICALP.2026.129) handled laminar families and near-minimum cuts. A companion OpenAI preprint claims the existence statement of the strong conjecture.
The source of this mission, an OpenAI preprint dated September 23, 2026, claims a deterministic polynomial-time construction.
Graphs are finite undirected loopless multigraphs; parallel copies count separately. For , is the multiset of edges with exactly one endpoint in , and is -edge-connected if for every such . A spanning tree is -thin if for all such . Two input formats are allowed: an explicit list of labelled edge copies, or a list of endpoint pairs with multiplicities written in binary (so the number of edges can be exponential in the input length). Running time is measured in the total binary input length.
There is an absolute constant and a deterministic algorithm that, given and a -edge-connected multigraph on at least one vertex (in either format), returns in time polynomial in the input length a spanning tree with
returning the empty tree for a one-vertex graph. Lean: OAI.AlgorithmicThinTrees.algorithmic_strong_thin_trees, open on the platform.
The theorem would give an algorithmic resolution of the strong thin tree conjecture: not only do -thin trees exist, they can be found deterministically in polynomial time, even for exponentially many parallel edges. It also yields simultaneous cost-and-cut rounding (Corollary 7.1): from a fractional point whose mass on every cut is at least one, a tree in its support with every cut load and total cost within constant factors, with no metric assumption on costs. The order is optimal. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists.
Existence proofs for thin trees go through the Marcus–Spielman–Srivastava interlacing-families theorem and a fixed-point argument, neither of which is constructive: they show that some choice works without locating it. The algorithm must replace these by explicit, rational, polynomially sized computations (checked signings, rational positive semidefinite decompositions, bounded denominators) and must work with binary multiplicities, where even listing the edges is exponential. Certifying thinness on all exponentially many cuts must also be done without enumerating them.
StrongThinTree.MultiGraph n m (vertices Fin n, edges Fin m, loopless). Inputs are ExplicitInput or BinaryInput (ordered, distinct endpoint pairs with multiplicities); a binary input's edge copies are Σ i, Fin (multiplicity i).Valid x: , and EdgeConnected k.CurrentKS.Machine: a deterministic machine with finitely many binary stacks and a finite instruction table, run for a fuel bound. Inputs and outputs are self-delimiting binary encodings (CurrentKS.encodeNat).AlgorithmicStrongThinTrees: ∃ C > 0, ∃ M a degree, 0 < a ∧ ∀ x, Valid x → after a * (len + 1)^degree steps M has halted and its output stack encodes a duplicate-free edge list forming a ThinTree C k; for the output is empty.Needed infrastructure: the existence theory of the companion mission, a model of deterministic computation with polynomial-time bounds, exact rational linear algebra, and constructive spectral sparsification. Contributions formalizing Proposition 2.5, Proposition 3.1, Lemma 6.1, Theorem A.1 (rational rank-one signing) or Corollary 7.1 are welcome.
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.