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.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
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?
For a field and a group , the group algebra consists of finite formal sums with , multiplied by extending the group law bilinearly. If has finite order , then , so has zero divisors. Kaplansky's zero-divisor conjecture asserts that this is the only source: if is torsion-free, has no nonzero zero divisors. Together with the unit and idempotent conjectures it is one of the central problems connecting ring theory, group theory and topology, and positive answers are known for large classes of groups (elementary amenable groups, groups with the unique-product property, torsion-free 3-manifold groups).
A group is torsion-free if with implies . It is finitely presented if it has a presentation with finitely many generators and relations. A classifying space (or ) for is a path-connected space with whose universal cover is contractible; it is finite two-dimensional if it is a finite CW complex with cells only in dimensions . A group with a finite-dimensional classifying space is automatically torsion-free, but the formal goal asks for both properties explicitly.
The coefficient field is , and is Mathlib's MonoidAlgebra (ZMod 2) G.
There exist a group and such that
This is the full Theorem 1.1 of the source, including its "Moreover" clause. The source proves existence probabilistically; it does not exhibit a concrete presentation. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. If correct, the theorem disproves Kaplansky's zero-divisor conjecture over , a problem open since the 1940s, and shows that torsion-freeness — even together with finite presentability and a 2-dimensional classifying space — does not force to be a domain. It implies that fails the unique-product property, and it bears on the implications among the Kaplansky conjectures (zero divisors, units, idempotents) and on approaches through the Atiyah conjecture and division-ring embeddings.
Formalizing it. The claim refutes a long-standing conjecture by an intricate probabilistic and topological construction, which is a strong case for machine verification. A full formal proof needs the probabilistic existence argument, planar separation, and asphericity of a 2-complex — none of which is a routine Mathlib application. Partial contributions (e.g. the characteristic-2 cancellation argument once asphericity and root separation are assumed, or the torsion-freeness of groups with finite-dimensional ) are welcome. A related machine-checked result exists only for the weaker non-unique-product property of Gardam's lattice (Mian–Siddique 2026).
Writing down whose product cancels in characteristic two is the easy part; the source does this by a parity argument on a graph of simultaneous steps. The hard part is two safeguards in the quotient group: both factors must remain nonzero (no vertex label other than the root can collapse to the identity), and the group must be torsion-free, which the source obtains by proving the 2-complex is aspherical. Standard tools — small-cancellation or CAT(0) criteria — are not applied; instead the source must exclude spherical arrangements of arbitrarily many paths of arbitrary length, which a union bound over sizes cannot handle.
TorsionFree G is the plain group-theoretic notion (, implies ); finite presentability is Group.IsFinitelyPresented.HasFiniteTwoDimensionalClassifyingSpace G asks for a Hausdorff, path-connected space with a finite CW structure on all of , no cells above dimension , at least one -cell, a group isomorphism , and a surjective covering map from a contractible space onto (so is aspherical). Requiring a -cell excludes only the case of free groups, whose group algebras are domains.Type and is existentially quantified together with its group structure; the zero divisors are elements of MonoidAlgebra (ZMod 2) G.A removal lemma says that an object far from having a forbidden substructure must contain many copies of it. Such statements are the combinatorial backbone of property testing: if every matrix that is -far from avoiding a pattern contains at least copies of , then sampling a number of rows and columns polynomial in detects the pattern with constant probability. Whether removal bounds are polynomial determines whether testers are efficient. For binary matrices whose rows and columns carry a fixed order, qualitative removal is known, and the polynomial version was conjectured.
A binary matrix of order is a map (in Lean BinaryMatrix n := Fin n → Fin n → Bool). For a binary pattern , an ordered copy of in is a pair of strictly increasing maps with for all : zeros must match as well as ones, and rows and columns are chosen independently. is the number of ordered copies, and is -free if . The normalized distance to -freeness is
where every cell may be changed in either direction.
The polynomial ordered binary matrix-removal conjecture asserts that for each fixed there are such that whenever , for all and .
The pattern is explicit: with and , the anchor has for , , and otherwise, and
For every there exist , and a binary matrix with
This is the "consequently" clause of Theorem 1.1 of the source, i.e. the negation of the conjecture for this fixed (here ). The source proves more: for every , with and , an explicit has and . The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. A single explicit pattern shows that ordered binary matrix removal can be super-polynomial, answering the finite-family question of Alon and Ben-Eliezer negatively and disproving the singleton conjecture recorded by Gishboliner and Shapira. It also gives a testing lower bound (Corollary 5.1): a canonical row–column sampler needs sampled positions per axis on these examples. Earlier non-polynomial examples needed a third symbol in the host; here the host is binary. The example separates hitting all existing copies (a set of cells meets them) from repairing the matrix (at least edits are needed).
Formalizing it. The statement is fully finite and explicit, so a formal proof would certify both the construction and the two counting estimates. The construction is intricate (tree-indexed blocks with interleaved orders, a 66-cell pattern), which is exactly where a machine check adds confidence.
Two estimates pull in opposite directions. The distance bound must hold against every binary repair, including repairs that create new copies elsewhere; the obvious argument — delete one cell per copy — fails because changing cells can create copies, and the source must show any repair needs at least edits. The copy bound requires locating every ordered copy of the 66-cell pattern in the unedited host, not only the designated anchors, which forces a rigidity analysis of how the anchor can embed.
Fin n → Fin n → Bool; ordered copies are pairs of StrictMono maps Fin k → Fin n, counted by copyCount. fixedH : BinaryMatrix 66 encodes with 0-based indices (the anchor rule becomes etaBit (u-32) (v-58) for , ).fixedMinEdits A is the minimum Hamming distance from to an -free matrix (the all-zero matrix is -free, so the minimum is attained by a genuine matrix, and the sentinel is never selected); fixedDistance divides by .Real.rpow; are arbitrary positive reals, and are existentially chosen, so the statement is exactly the failure of the conjectured inequality for this . It is weaker than the explicit quantitative family of Theorem 1.1; a stronger milestone recording and the bound would be welcome.In a Maker–Breaker achievement game, two players alternately claim cells of a board; Maker wins by owning every cell of some copy of a fixed shape, and Breaker only tries to prevent this. Polyomino achievement games on the infinite square grid, introduced by Frank Harary, ask which small polyominoes are winners (Maker can force a copy) and which are losers (Breaker can prevent it forever). The six-cell shape Snaky is the long-standing hard case: Maker was known to win with a one-stone handicap or in higher dimensions, but the ordinary planar game without handicap remained undecided.
The source of this mission, an OpenAI preprint dated September 25, 2026, settles the ordinary planar game: Snaky is a winner, within 21 Maker moves.
The board is , initially empty. Snaky is
An allowed copy is with and one of the eight signed permutation matrices (rotations by quarter turns and reflections; no scaling). Maker moves first; then Breaker and Maker alternate, each claiming one previously unclaimed cell. Maker wins when it owns all cells of an allowed copy.
A Maker policy is a rule that, given the current position, returns an unclaimed cell. In the fixed-endpoint formulation, the policy keeps claiming fresh cells even after a win, and one asks that after Maker's -th claim its set of cells contain an allowed copy whenever Breaker's first replies were legal.
A pure computation on a printed certificate of 616 cards: card counts, 1,837 placement terms, required-set/envelope/height data of four interface cards, and uniform bounds for all cards.
The Lean statement OAI.SnakyPrototype.snaky_winning_strategy_21_with_legal_states is open on the platform.
Theorem 1 decides the ordinary planar Snaky game, recorded as undecided by Sieben (2008), and gives an explicit bound of 21 Maker moves (a win by the 41st individual turn). It also gives a win on the finite board (Corollary 6), and removes the handicap from the earlier handicap-one strategies. The paper does not claim the bound 21 is optimal or address the strong game in which both players seek a copy.
The result is proved in an OpenAI preprint that has not been peer reviewed. Its correctness rests on a soundness lemma for a composition rule together with large finite certificates checked by standalone programs. A machine-checked proof would replace this combination of informal soundness argument and external computation by a single certified statement.
The board is infinite and Breaker may play anywhere, so no finite game-tree search applies directly: a proof must cover all Breaker replies, including those far from the action. Pairing strategies, the usual tool for proving shapes are losers, are known to fail for Snaky, but that does not give Maker a strategy. The certificate approach needs a composition rule whose soundness accounts for arbitrary previous ownership on both sides; the move count must be the number of actual Maker claims, including any replacement moves.
ℤ × ℤ; snaky is the six-cell set above and HasSnaky M asks for r : Fin 8, t : Cell with snaky.image (placement r t) ⊆ M, where orient lists all eight signed permutations.Policy is a function of a move counter, the Maker set and the Breaker set; it must never return an owned cell. playState σ N β ∅ ∅ k is the position after Maker claims and Breaker replies.LegalRepliesBeforeFinal σ N β ∅ ∅ constrains only the first Breaker replies; the theorems conclude a copy of , exactly Maker cells, and disjointness of the two players' sets throughout.Array Entry and computes rowAt i (required set, envelope, height) by the composition recursion; it is a decidable statement about explicit finite data.A trivializing reading is ruled out: the policy is required to be legal on all inputs, and Breaker's replies are arbitrary legal cells of the infinite board. A complete development needs a soundness proof for the composition rule (Lemma 3) and verified evaluation of the certificates; the policy, game and certificate infrastructure is shared between the 21- and 35-move statements. Contributions formalizing Lemma 3, Proposition 5 (the 21-move certificate identities) and Corollary 6 are welcome.
Given points in the plane with no three on a line, a halving line is a line through two of the points that leaves exactly half of the remaining points on each side. How many halving lines can an -point set have? The question is the middle case of the -set problem: count the -element subsets that a line can cut off. It controls the complexity of levels in line arrangements, and through them the running time of many algorithms in computational geometry (levels, ham-sandwich cuts, -th order Voronoi diagrams).
The gap between the bounds is one of the best known in discrete geometry: the upper bound has been since 1998, while the best constructions give only .
The source of this mission is an OpenAI preprint dated September 25, 2026, which claims the first power saving below .
Let be distinct points of with no three collinear. For , the orientation is the usual determinant; its sign says on which side of the line the point lies. For even , an unordered pair is a halving pair if exactly points lie strictly on each side of the line ; is the number of halving pairs.
A configuration is generic if moreover its -coordinates are distinct, the slopes of the segments are distinct, and no point where two of these segments properly cross lies on a third segment. Fix a rank . For a slope , mark the points with smallest value of . As increases from to , the marked set changes by exchanging one point for another; each change is a switch, and is the total number of switches. A switch at rank happens at the slope of exactly when points lie strictly below the line . At the middle rank, switches are halving pairs.
The Lean statement OAI.PlanarHalving.power_bounds is the conjunction of these two clauses and is open on the platform. Neither nor is specified, so the goal asserts only the shape of the improvement and survives any later numerical sharpening.
A power saving is the first improvement of the exponent in Dey's bound since 1998. The uniform version over all ranks gives, through shallow cuttings, a -sensitive bound for planar -sets and for the complexity of the -level in an arrangement of lines (Corollary 1.3). The saving is non-quantitative: the paper's compactness argument gives no numerical .
The result is proved in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. Formalizing it would certify a long compactness argument (limiting measures, rank coordinates, differentiation of monotone functions) whose ineffective nature makes informal checking hard.
Dey's argument decomposes the halving graph into convex chains and applies the crossing lemma; both ingredients are tight on their own, so a power saving must show that configurations nearly attaining the crossing-lemma bound cannot exist. The bound must also hold uniformly over all ranks , because restricting a block of switches to the points that take part in it changes the rank. Since the lower-bound constructions are far below , there is no extremal example to guide the argument.
ℝ × ℝ, configurations are P : Fin n → Point; GeneralPosition P is injectivity plus nonvanishing orient for every triple of distinct indices.halvingCount P counts pairs i < j with sideCount P i j = (n-2)/2 and sideCount P j i = (n-2)/2, where sideCount counts points with strictly positive orientation. Natural-number division is harmless because is even.Generic P adds distinct first coordinates, distinct slopes of index pairs, and the condition that no proper crossing of two determined open segments lies on a third closed segment.switchCount P k counts pairs i < j with 0 < k < n and exactly k - 1 points strictly below the line through P i, P j in the order . Ranks and therefore contribute zero, as in the paper.slope divides by the -difference; the generic hypothesis makes it nonzero.A complete development needs the crossing lemma, convex-chain decompositions of the rotating-line process, weak compactness of finite Borel measures, the Radon–Nikodym and Lebesgue differentiation theorems, Rademacher-type differentiability of monotone functions, and planar Jordan-curve separation. Contributions formalizing Dey's bound, Theorem 2.1 (uniform activity packing) and Proposition 8.1 (the fixed-scale recurrence) are welcome.
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 .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 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 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. 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.
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 measure-preserving transformation of a probability space acts on square-integrable functions by the Koopman operator , a unitary operator. Its spectral type (discrete, singular continuous, absolutely continuous) and its multiplicity are basic invariants of ergodic theory. The Lebesgue spectrum is the spectral type of the shift on , the type of Bernoulli shifts and other strongly chaotic systems, where it occurs with infinite multiplicity. Banach's problem asks whether Lebesgue spectrum can occur with multiplicity one: is there a transformation whose Koopman operator on the orthogonal complement of the constants is unitarily equivalent to multiplication by on ? Equivalently, is there a single function whose bilateral orbit under is an orthonormal basis of the mean-zero space? The problem combines spectral theory with the construction of explicit dynamics, and a smooth example would show this spectral behavior is compatible with the regularity of differentiable dynamics.
Let and let be normalized Lebesgue (Haar) measure on . A bijection is a diffeomorphism if and lift locally to maps of . It is volume preserving if for every measurable . Let be the closed subspace of complex square-integrable functions with integral zero, and . Let be Haar measure on the circle and the first Fourier character.
In Lean (namespace OAI.ThreeTorus), the torus is Fin 3 → UnitAddCircle with the product Haar measure, smoothness is local smooth lifting on Fin 3 → ℝ, is the subspace meanZero of Lp ℂ 2 μ, and MainConclusion packages the theorem below.
There exist a volume-preserving diffeomorphism of and a real-valued such that
moreover is ergodic, and there is a unitary with
The goal is published on the platform with status Open.
The result itself. The theorem answers the probability-preserving form of Banach's problem, with the strongest kind of example: the invariant measure is the standard smooth volume on a compact manifold, the map is , and the conclusion covers the whole mean-zero space, both spectral type and multiplicity. Earlier work produced Lebesgue components, Lebesgue spectrum of higher multiplicity, simple spectrum of other types, flows, or infinite-measure examples; time- maps of simple-Lebesgue flows have infinite multiplicity, so they do not answer the question. The source also derives from it mixing (of all orders, using a separate companion multiple-mixing theorem), zero Kolmogorov–Sinai entropy (via Rokhlin's finite-multiplicity entropy theorem) and vanishing Lyapunov exponents (Corollary 6.1, p. 28).
Formalizing it. The statement exercises Mathlib's spaces, Haar measure on the additive circle, ergodicity and Fourier characters together. A formal proof would certify a long quantitative construction (successive smooth passages, stationary-phase estimates, Fourier signals) whose convergence must be checked simultaneously in the topology and in spectral norms.
Smooth constructions by successive conjugation (Anosov–Katok type) naturally produce maps with singular or discrete spectral behavior, because each approximating map is close to a rotation or an integrable twist with pure point or very structured spectrum. Lebesgue spectral type requires the spectral measure of every function to be absolutely continuous with the right density, and simplicity requires a single orbit to span the whole space. Making both hold in the limit, while keeping the limit map , requires controlling spectral densities at every scale and approximating every target function by translates of one fixed vector — the step where generic perturbation arguments give no control.
Fin 3 → UnitAddCircle with Measure.pi of AddCircle.haarAddCircle; is an Equiv.Perm with Smooth T and Smooth T.symm (local lifts), and MeasurePreserving T μ μ.Lp ℂ 2 μ with zero integral; is real-valued almost everywhere. The orbit is required to be orthonormal with dense span, i.e. a Hilbert basis indexed by .W : H₀ ≃ₗᵢ[ℂ] CircleH intertwining composition with and multiplication by fourier 1. Ergodicity is Mathlib's Ergodic T μ.A limit cycle of a planar vector field is a periodic orbit that is isolated among periodic orbits. The second part of Hilbert's sixteenth problem asks how many limit cycles a polynomial vector field of a given degree can have, and it is open even for quadratic fields. The classical Liénard systems
equivalent to the oscillator equation , are the most studied restricted family. In 1977 Lins, de Melo and Pugh conjectured that for the maximum number of limit cycles is . The conjecture is now known to fail for , holds for , and degree five was the remaining undecided case, where it predicts exactly two.
This mission asks for a formal proof of the degree-five bound and its sharpness, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
For a real polynomial (the primitive of the damping), consider the vector field on . A solution is a differentiable with for all . A periodic orbit is the image of a nonconstant solution that is periodic with some period . A limit cycle is a periodic orbit having an open neighbourhood such that every periodic orbit contained in equals . Limit cycles are counted as sets: once each, regardless of multiplicity, stability or hyperbolicity. The periodic orbits of a centre are not limit cycles.
For every real polynomial with ,
and some with has exactly two limit cycles. No parity, coefficient-sign, hyperbolicity or amplitude restriction is imposed.
The result itself. It decides the last open degree of the Lins–de Melo–Pugh conjecture in the affirmative, so the conjecture is true exactly for . Unlike the slow–fast result of Li and Lu, it bounds all cycles of every quintic system, including degenerate (multiple) ones and cycles of large amplitude. The preprint also corrects a proposed four-cycle quintic example from the literature by identifying it with a family known to have exactly two periodic solutions (p. 2).
Formalizing it. The statement uses only polynomials, ODE solutions and planar topology, so it is well suited to formal verification, and it would be one of the first machine-checked global limit-cycle bounds for a nonlinear family. The proof's general comparison results for smooth profiles (Propositions 5.2 and 5.3, pp. 32–34) and the global quadratic fit (Theorem 3.6, p. 18) are independent of the polynomial application and reusable.
Small-amplitude (Hopf/Melnikov) calculations only control cycles near the origin or near a perturbation of a centre; they say nothing about distant cycles. The even coefficients of prevent the reduction to the odd quintic family settled by Rychkov. Generic-perturbation arguments that remove multiple cycles cannot be used, since the count must include degenerate cycles. The preprint keeps the two half-orbits separate, writes each as an arch in coordinates valid at every amplitude, fits each arch by a quadratic comparison profile (Theorem 3.6), and controls how the fitted parameters move with width through a Schwarzian-type model inequality (Theorem 4.1, p. 20). Periodic orbits then become zeros of a single matching function (Proposition 2.5, p. 10), whose isolated zeros are bounded using an integrating factor (Section 6).
ℝ × ℝ; vectorField F z = (z.2 - F.eval z.1, -z.1) with F : Polynomial ℝ and F.degree ≤ 5 (this includes constants and the zero polynomial, which have no limit cycles).IsSolution requires HasDerivAt at every real time; IsPeriodicOrbit asks for a solution, a period T > 0, non-constancy, and C = range z.IsLimitCycle F C is a periodic orbit with an open U ⊇ C such that every periodic orbit C' ⊆ U equals C.Set.encard on the set of limit cycles, so infinitely many would give ⊤; the goal asks for ≤ 2 for every admissible F and = 2 for some.Welcome contributions: existence and smooth dependence of return maps for planar polynomial flows, and the energy-identity first-order return calculation used for sharpness (Section 7, p. 39).
An exact linear equation can carry arbitrarily fine real information: independent Gaussian equations determine a vector almost surely. A streaming learner that keeps only finitely many persistent states cannot retain those equations at arbitrary precision. The question is how many fresh equations such a learner needs to estimate a direction to angular accuracy when the information passed between observations is bounded in bits.
This preprint proves an explicit answer for memory : at least samples, uniformly in . With real-valued registers, randomized Kaczmarz needs only order samples, so the bound shows that bounded memory cannot beat that scale.
Fix , , , and . For a signal the observations are independent and exactly. A finite-state Gaussian stream learner reads the pairs in order; at every index its persistent state has at most values. Transition and stopping rules may depend on the index, , the current state, the whole current pair and fresh randomness, with unrestricted computation. It stops at some and outputs from the terminal state, and fresh randomness. A shared seed may choose the rules; seed and initial state are independent of the signal and rows. The experiment is jointly measurable.
For a linear space and , with , the affine subsphere is a test set of dimension . A block of exact Gaussian rows leaves the target, conditionally, uniform on a random residual subsphere of dimension .
In Lean (OAI.SubsphereCurrent), learners are SeededLearner d M T Ω built from KernelLearners (Markov-kernel transitions on completed observations, states Fin (2^M)), with Admissible measurability, uniformSuccess and per-signal success.
full_current_main_scopeThe conjunction of the paper's main statements:
The result. Theorem 1.2 gives explicit constants for the memory–sample bound with exact Gaussian observations and memory, e.g. at accuracy . The block estimates are statements about uniform measures on random affine subspheres that are independent of the learning application.
Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. Companion missions on the same family of preprints (memory and precision, posterior replicas, projection moments) share the learner model; this one is distinguished by explicit constants.
Conditioning on an exact Gaussian block makes the posterior of the signal singular: it is uniform on a lower-dimensional residual subsphere determined by the data. Density-based information arguments therefore fail after one block. The bound must control the success probability of the remaining computation, started from any state, averaged over every affine subsphere of large dimension, uniformly over learners that may process each real-valued pair without limit.
Vector d = EuclideanSpace ℝ (Fin d), signals in the unit sphere with normalized surface measure, rows i.i.d. stdGaussian.ℝ≥0∞; the constant is written (2:ℝ)⁻¹ ^ 16 and the logarithm is Real.logb 2.d/16, d/32, d/8; the fixed-length estimate uses Fin (2^(d^2)) states.The goal cannot be satisfied vacuously: hypotheses range over all admissible learners and the success thresholds are attainable with large .
Needed infrastructure: Haar measure on Grassmannians or orthogonal groups, beta laws of projected directions, spherical caps, measurable selection of Borel rule versions. Contributions proving individual conjuncts are welcome.
A finite message chosen from data changes the conditional distribution of those data. In memory-constrained inference this matters directly: a learner observing a signal through exact Gaussian equations keeps a finite state , and after conditioning on the rows that were used to select it are biased. An independent Gaussian matrix has the same unconditional law as those rows, but once its labels are revealed it need not leave the same information about .
This preprint quantifies the cost of that replacement. For a uniform signal on the sphere and a message of entropy at most , replacing the actual rows by fresh independent rows increases the remaining conditional information by at most . As an application, learners with persistent bits need exact Gaussian observations to reach angular accuracy .
Let be uniform probability on , the law of a matrix with i.i.d. entries, discrete entropy and conditional mutual information, all in nats. Put
Let and be independent, and let be a countable message with an arbitrary joint law with .
In Lean (OAI.CurrentProjection), the joint law of is a probability measure P on (Sphere d × W) × Rows (d/10) d whose marginal is uniformSphere d ⊗ gaussianRows (d/10) d; alignedExperiment and P.fst.prod (gaussianRows ...) are the two experiments; exposedInformation is computed as a relative entropy via condKernel; shannonEntropy is .
There are an absolute and such that for and every such countable with ,
with an exact-density version when .
The result. Theorem 4.1 converts a statement about the actual, selection-biased rows into one about fresh rows at an additive cost of , which is the step that lets block-by-block information bounds be iterated along a stream. With the residual-sphere endpoint it gives the lower bound for learners with bits (Theorem 8.4, Corollary 8.7). The mixed projection moment (Theorem 3.1) is a reusable estimate on exact Gaussian projections of measures with local mass control.
Formalizing it. All results are in an unrefereed preprint, with no machine-checked proofs. The streaming theorems themselves (Theorem 8.4, Theorem 8.6, Corollary 8.7) are not among the published Lean targets and remain future work.
Conditioning on biases in a way that depends on the unknown signal, so the two experiments have different joint laws even though their and marginals agree. A direct comparison of densities fails because the exact label density under the actual law can be large on a selection-dependent set; controlling it requires a high moment of the projected density with the row-information charge entering only with coefficient .
Metric.sphere (0 : EuclideanSpace ℝ (Fin d)) 1 with normalized surface measure; rows are Fin k → EuclideanSpace ℝ (Fin d) with stdGaussian entries.ℝ≥0∞-valued.d/10, d/2 - d/10, d/32, d/8, d/4, d/3 as in each source statement.The goal is not vacuous: it quantifies over all joint laws with the stated marginal and entropy bound, and the right side is finite for many of them.
Needed infrastructure: conditional mutual information for standard Borel variables, chain rules, exact density versions of Gaussian projections, local mass bounds on the sphere. Contributions toward any milestone are welcome.
An exact linear observation of a real signal can carry arbitrarily many bits. A finite message computed from a block of such observations cannot, but its information content is not controlled by the number of observations alone: if earlier messages have already concentrated the signal in a small region, the next block can exploit that concentration. Bounds of this kind are the engine of memory–sample lower bounds for noiseless Gaussian regression, where a learner with bits of memory must recover a unit vector to angular accuracy from a stream of exact Gaussian measurements.
This preprint asks how to restore a geometric spread condition on the posterior while paying for the information revealed in doing so, and proves that, for a cube-shaped prior on a spherical patch, blocks of exact measurements with messages of at most values reveal only nats.
Let be large, , , . The cube prior is normalized Lebesgue measure on the half-open cube , and the chart maps it into . Dyadic cells of level subdivide into half-open subcubes of side .
Draw . In block an independent standard Gaussian matrix is drawn, and is observed exactly. A message is drawn from a Borel probability kernel of the block data, whose choice may depend on the preceding messages . Information is measured in nats by mutual information , defined as a relative entropy.
In Lean (OAI.RepeatedLocalization), Coordinate n = Fin n → ℝ, cubePrior n is Lebesgue measure conditioned on initialCube n, chart is , a Cell n is a level with a multi-index in Fin (2^J), a BlockRule n N is a measurable probability vector on Fin N indexed by block data, Rules n N t chooses a rule for each block from the past history, and experimentLaw rules is the joint law of .
repeated_localizationThere is an absolute such that for every there is with the following property, for large. If
then one can reveal nested dyadic cells containing , with a finite-valued measurable function of and , such that the augmented transcript satisfies
where is the level of . An alphabet of size satisfies the hypothesis with depending only on .
The result. Theorem 3.2 is the first information estimate in the paper and the model for its later routes: it shows that revealing a nested dyadic cell after each block, which restores the spread condition needed by the projection estimate, costs only nats per block. Since the original message history is a function of , the bound also controls the information in the messages alone. Combined with the paper's endpoint arguments this yields the lower bound for learners with bits.
Formalizing it. These results are proved only in an unrefereed preprint; no machine-checked proofs exist. The milestones are independent analytic statements (an entropy regularization, a convex potential and its drift, an inverse-volume moment) that are reusable in the companion missions on exact Gaussian observations.
The information a block reveals depends on how concentrated the current posterior is, and earlier messages can make it arbitrarily concentrated. Simply conditioning on messages gives no control. Revealing a localizing cell restores spread, but naming a cell itself costs information, and the count of candidate cells at depth grows like ; the argument must show that confinement to a depth- cell (worth bits relative to the prior) pays for this, uniformly over all message rules.
Fin n → ℝ, and appears as n + 1.n / 16, n / 8. Gaussian entries are gaussianReal 0 1.Q : Disclosure n N t is valid when each cell map is measurable with finite range, contains , lies in , and the cells are nested. The goal asserts existence of a valid disclosure with mutualInformation (augmentedLaw rules Q) ≤ C (n+1) t and expected final level at most .klDiv of the joint law against the product of marginals, valued in ℝ≥0∞.The goal is not trivial: the trivial disclosure (always ) does not bound the information in arbitrary messages, and the quantifier order (absolute , then , then ) matches the source.
Needed infrastructure: Gaussian projections of measures on cells, density bounds, dyadic cell combinatorics, and relative-entropy chain rules. Contributions toward any milestone are welcome.
Suppose an unknown unit vector is observed through exact linear measurements with independent Gaussian rows . If every pair is kept, rows determine . A learner that can keep only a bounded number of bits between measurements must compress each exact real label into a state update, and the question is how many measurements this costs for a prescribed angular accuracy . Exact labels make the question delicate: a real label has no built-in bit precision, so noise-based arguments do not apply.
This preprint attacks the question through a conditional information bound for a single block of observations: how much information about can a finite message formed from exact Gaussian measurements carry, beyond what an independent Gaussian projection of (revealed only to the analyst) already reveals? Iterating such a block bound over a stream gives a memory–sample lower bound.
Let be uniform probability on . In a block experiment the signal has law with a Borel density . Independently draw a standard Gaussian matrix and observe . A message with values in a finite set is drawn from a measurable Markov kernel of . Finally an standard Gaussian matrix is drawn independently of everything. The quantity of interest is the conditional mutual information
in nats, and denotes the Shannon entropy of the message.
A finite-state learner with bits reads pairs once, in order, keeps a state in a set of size , may stop at any index up to a deterministic horizon , and outputs a unit vector from its terminal state, stopping index and fresh randomness only. Transitions and stopping may be arbitrary measurable randomized rules of the current state and current pair; shared randomness is independent of the signal and samples.
In Lean (OAI.PosteriorReplicas), sphereLaw d is normalized surface measure, gaussianRows d k is the product of stdGaussian, signalMessageLaw p κ is the law of , sideLaw ℓ appends , conditionalInformation is the relative entropy of the joint law from the conditionally independent coupling, and messageEntropy is . Learners are CompletedKernelLearner d M with Markov-kernel transitions on the completed observation space, wrapped in a JointKernelExperiment over a seed space .
OAI.PosteriorReplicas.source_mainThe goal is the conjunction of the paper's principal statements:
uniformly over the prior, , and the message kernel.
The result. Theorem 1.2 shows that with persistent bits, the sample scale of real-valued Kaczmarz-type methods cannot be improved for exact Gaussian measurements, under the uniform prior and with an absolute constant. Theorem 1.1 is a reusable statement in its own right: the entropy of a message is divided by a factor proportional to , and the dependence on the prior density bound is only doubly logarithmic, which is what allows conditioning on rare learner states.
Formalizing it. These results appear only in an unrefereed preprint, and none has a machine-checked proof. The companion preprint Memory and precision in noiseless Gaussian regression proves a related statement for memory by a different method; the two missions share the learner model but not the block estimates. Formalizing the goal requires conditional mutual information for general (non-discrete) random variables and the exact equal-label geometry, both of which would be reusable.
Conditioning on one exact observation confines the signal to a lower-dimensional section of the sphere, so posterior densities with respect to do not exist and density-based arguments fail. Bounding the information in the message by alone is far too weak: a message of bits could then carry all relevant information. The block bound must instead account for what the analyst's independent projection already reveals, uniformly over priors with large density bounds , since rare learner states produce such priors.
EuclideanSpace ℝ (Fin d); priors are measures on the ambient space given as (sphereLaw d).withDensity f with .Fin N with NeZero N; information quantities are ℝ≥0∞-valued relative entropies (klDiv), entropies use natural logarithms.2 * (d / 16), d / 8, d / 2 as in the paper.IsLittleO atTop M (d^2), all horizons , all , all seed spaces and all JointKernelExperiments whose output kernel agrees almost surely with the run of the per-seed learner.The goal cannot be met vacuously: block bounds are stated for every finite message kernel, and the streaming hypothesis (success at least ) is satisfiable by learners with large .
A complete development needs Gaussian matrices and their projections, coarea-type identities for equal labels, conditional kernels (condKernel), relative entropy chain rules, and spherical measure estimates. Contributions that isolate one conjunct (for example Theorem 3.3 or Theorem 1.1) are welcome.
A single exact linear equation about an unknown unit vector carries arbitrarily fine information: independent Gaussian equations determine almost surely, provided all of them can be kept. A learner that reads the equations once, in order, and keeps only a bounded number of bits between them faces a different problem. The question asked here is how many noiseless measurements such a learner needs in order to reach a prescribed angular precision , as a function of its memory.
This is a question about memory–sample trade-offs: how much a bound on persistent memory forces a learning procedure to read more data. With unbounded real registers, the randomized Kaczmarz update satisfies on isotropic Gaussian rows, so order samples suffice. That update stores real numbers and gives no finite-bit upper bound; the question is whether a learner with roughly bits can do better than this scale.
Fix integers , , . A signal lies on the unit sphere . At step the learner receives the pair with independent and exactly (no noise).
A finite-state learner with bits keeps a state in a set of at most elements. A data-independent shared seed (drawn from a probability space ) may select its rules. Given the seed, the current state, the step index and the current pair, a transition chooses the next state and whether to stop; it may perform unrestricted computation but retains only the next state. The learner must stop by the deterministic horizon . Its output is a function of the terminal state, the stopping index and the seed only; a discarded observation cannot be read again. Success at precision means angular error .
Write for the uniform probability measure on . Uniform success is the probability of success when is drawn independently of the rows and the seed.
In Lean (OAI.NoiselessRegression), the state space is Fin (2 ^ M), a learner is a structure Learner d M T Ω with fields initialChoice, transition, output, the sample law is the product of stdGaussian on EuclideanSpace ℝ (Fin d), and uniformSuccess and success are the probabilities defined above. Randomness during the run is represented through the arbitrary seed space .
OAI.NoiselessRegression.mainThe goal is the conjunction of two statements.
Fixed quadratic memory (Theorem 1.2): for every there are and such that, for , , , and every admissible learner,
Subquadratic memory (Corollaries 1.3 and 1.4): there is an absolute such that for every memory sequence there is with the same conclusion for , under either uniform success at least or success at least for every fixed signal .
No relation between and is assumed; the constant is absolute in the subquadratic case.
OAI.MemoryPrecision.main)A single bundled statement collecting the paper's projection-density and backward-block estimates (Theorem 3.1, Propositions A.1, A.4, A.5, B.6, B.7, Corollary 8.2), the cube-prior precision bound (Proposition 8.3), and the explicit success bound after a bounded number of samples (Proposition 5.3):
The result. Theorem 1.2 answers, for exact observations and isotropic Gaussian rows, the precision question raised in Section 1.1 of Sharan–Sidford–Valiant: with bits, the scale achieved by real-valued Kaczmarz cannot be improved, uniformly over all . Because an exact-observation learner can simulate added noise, the preprint derives from it an lower bound in the noisy experiment of Sharan–Sidford–Valiant at accuracy , which strengthens their bound in that range.
Formalizing it. The result is proved only in an unrefereed preprint; no machine-checked proof exists. A formal proof would certify a lower bound whose model (randomized measurable rules, early stopping, shared seeds, measurability conventions) is delicate, and the conventions are already fixed in the Lean definitions. Remaining work: the full formal proof, and as a variant the every-signal version of Theorem 1.2 for fixed (Corollary 1.4), which the Lean goal states only in the subquadratic case.
Conditioning the uniform prior on one exact observation confines the signal to a hyperplane section of the sphere, a law singular with respect to the original spherical measure; information-theoretic arguments that track a posterior density therefore break down after a single step. Arguments for noisy observations, such as Sharan–Sidford–Valiant's, rely on the noise to keep posteriors spread out and do not transfer to the more informative exact experiment. The bound must also hold uniformly in with no relation between and , so a learner with bits must be prevented from storing bits per coordinate for very small .
EuclideanSpace ℝ (Fin d); signals and outputs in Metric.sphere 0 1. The uniform sphere law is the normalized toSphere measure; rows are i.i.d. stdGaussian.Fin (2 ^ M); the first component of each action is the stop flag. Runs that never stop are forced to terminate at index .Learner.Admissible requires a.e.-measurability of the initial choice, transitions (against Gaussian × Lebesgue on pairs), outputs, and of the full experiment under each fixed signal and under the uniform prior.ℝ≥0∞-valued; the threshold is ; angular error is Real.arccos ⟪ŝ, s⟫; is natural.u, so randomized learners are covered by placing their randomness in the seed.The goal cannot be satisfied trivially: the hypotheses range over all admissible learners, and the success threshold is achievable (with large ), so the implication has content.
A complete development needs Gaussian measures on Euclidean space, spherical measure and cap estimates, Gram determinants and affine distances, densities of Gaussian projections, and measurable selection of Borel versions of kernels. The projection-density estimates are reusable beyond this mission. Contributions toward the bundled milestone, or toward any of its component estimates, are welcome.