Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A regular expression describes a set of words using letters, union, concatenation and the Kleene star (any finite repetition of words from ). The star height of an expression is the depth of nesting of its stars, and it measures how many layers of unbounded repetition a regular language genuinely needs. For ordinary expressions this hierarchy is infinite. Allowing complement as an additional operation changes the picture: Boolean conditions can replace some layers of repetition, and the generalized star-height problem asks how far this goes. Whether every regular language has generalized star height at most some fixed number — and in particular whether one star always suffices — has been one of the longest-standing questions in the algebraic theory of automata.
Fix a finite alphabet and let be the set of finite words. A generalized regular expression over is built from the constants (denoting ) and (denoting ), single letters , union , concatenation , complement (taken in ), and star . Its height is defined by
For a regular language , the generalized star height is the least height of an expression over denoting .
In Lean (namespace OAI.GeneralizedStarHeight), expressions are an inductive type Expression Alphabet with exactly these seven constructors, Expression.language interprets them in Mathlib's Language Alphabet (complement is Language complement, i.e. relative to all words), Expression.height is the recursion above, and HasHeightAtMost L n means some expression has language and height at most .
For every finite alphabet and every regular language ,
The goal is published on the platform with status Open.
The result itself. Before 2026 it was not known whether generalized star height is bounded at all; all positive results covered restricted families of monoids or languages. Theorem 1.1 gives a uniform bound independent of the alphabet and of the recognizing automaton, settling the boundedness question. It leaves open the sharper question of whether height one always suffices: no language is known to require height two. A uniform bound also implies that the hierarchy of generalized heights has at most four nonempty levels, which narrows where any separating example must be sought.
Formalizing it. The statement is short and fully elementary, but the proof composes many constructions (finite-monoid recognition, prefix codes of episodes, split identities, marker scales) whose height accounting is error-prone. A formal proof would certify the boundedness theorem itself. Mathlib already has regular languages (Language.IsRegular) and ordinary regular expressions; this mission adds generalized expressions with complement and their height.
The classical lower bounds for ordinary star height do not transfer once complement is allowed, and complement can simulate many but not obviously all counting arguments. The natural approach — write each fiber of a morphism from to a finite monoid by an expression that simulates the monoid computation letter by letter — needs one star per level of the computation's dependence on earlier history, and the depth of this dependence grows with the monoid. Group components are the difficulty: aperiodic monoids give height zero, but counting modulo and nonabelian group computations require stars, and a uniform bound must handle arbitrary finite groups nested inside arbitrary monoids without the number of stars growing with their size.
Type u with [Finite Alphabet]; regularity is Mathlib's Language.IsRegular (acceptance by a finite-state DFA).height charges only for stars; complement, union and concatenation are free, exactly as in the source. Since HasHeightAtMost asks only for existence of an expression, no bound on expression size or computability is claimed, matching the source's remark that the construction bounds nesting only.Weisfeiler–Leman (WL) refinement compares two graphs by repeatedly refining colors of ordered vertex -tuples. For every fixed dimension this is a polynomial-time procedure, with running time . When is part of the input, that computation is no longer polynomial, and the complexity of deciding the outcome becomes a question in its own right. Seppelt (2024) proved coNP-hardness and recorded Berkholz's question whether the problem is EXPTIME-complete.
This preprint answers that question for the joint-update convention: deciding -WL equivalence of two explicit graphs with in binary is EXPTIME-complete, even on connected graphs of maximum degree three.
Graphs are finite, simple, undirected and uncolored, given by adjacency matrices. In the joint-update convention a -tuple's initial color records equalities and adjacencies among its entries; each round adjoins to the old color the multiset, over replacement vertices , of the vector of old colors obtained by replacing each coordinate in turn by . Color names are common to both graphs, and means their -tuple color histograms agree at every round.
The language consists of encodings with in binary and . The language additionally requires and to be connected, of the same positive order, and of maximum degree at most three. Malformed encodings are excluded.
In Lean (OAI.VariableWL), Graph is a SimpleGraph on Fin order, color and histogram implement the joint update by recursion on rounds, pairCode concatenates the two graph codes (order header plus row-major matrix) and the code of , and complexity classes are defined from an explicit deterministic Turing machine model with OutputsWithin, InEXPTIME, PolytimeReduces and EXPTIMEComplete.
Both and are EXPTIME-complete under deterministic polynomial-time many-one reductions:
The result. Theorem 1.1 resolves the question recorded by Seppelt and strengthens the known coNP-hardness to EXPTIME-completeness. The subcubic case is notable because isomorphism of bounded-degree graphs is polynomial-time (Luks), yet equivalence under refinement at a supplied dimension remains EXPTIME-complete for degree three; nonisomorphic graphs can be equivalent. Corollary 8.3 shows hardness persists with in unary.
Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. The uniform computation interface developed here is reused by the companion identification paper, so a formalization would serve both missions.
Membership requires showing that the dimension can be capped before allocating tuple tables (Lemma 2.2), since may exceed the graph order. Hardness requires simulating an arbitrary exponential-time computation by a graph pair whose WL equivalence at a polynomially encoded dimension reflects acceptance. Because the number of address coordinates grows with the input, fixed-dimension constructions with dimension-dependent constants do not give a uniform polynomial-time reduction, and in the subcubic case colors must be realized by uncolored degree-three gadgets that a winning strategy still recognizes.
SimpleGraph (Fin order); Subcubic bounds every vertex degree by three; SubWL also demands positive equal orders and connectivity.Multiset types.The statement is not trivial: both membership and hardness are required for both languages.
Needed infrastructure: the bijective game characterization (Lemma 2.4), product-circuit compilation (Proposition 3.2), the general and subcubic realizations (Propositions 5.1 and 7.1) and the uniform compiler (Proposition 8.2). Contributions toward any of these are welcome.
The Weisfeiler–Leman (WL) method colors -tuples of vertices by repeatedly recording their local extension patterns; two graphs are -WL equivalent when the stable color histograms agree. For each fixed the direct algorithm runs in time : there are tuples and polynomially many refinement rounds. The question is whether the growing exponent is necessary for any algorithm deciding the equivalence relation, not just for implementations of refinement.
This preprint proves that it is, unconditionally: for every sufficiently large fixed , every deterministic sequential decider for -WL equivalence needs time at every sufficiently large graph order, without assuming the Exponential Time Hypothesis.
Graphs are finite, simple, undirected and uncolored, given as adjacency matrices. For a -tuple, the initial color records coordinate equalities and adjacencies. Each refinement step keeps the old color and adds, in the joint convention, the multiset over vertices of the -vectors of colors obtained by replacing each coordinate by ; in the separate convention, one such multiset per coordinate. Two -vertex graphs are -WL equivalent if their color histograms agree at every round.
A decider for a convention and dimension is a deterministic machine that halts on every encoded pair of -vertex graphs and accepts exactly the equivalent pairs. Its worst-case time is the maximum running time over pairs of -vertex graphs (optionally restricted to connected graphs of diameter at most two).
In Lean (OAI.WLTime), Graph n is a symmetric loopless Boolean matrix on Fin n, tupleColor and histogram define both conventions by recursion on rounds, Equivalent compares all rounds, encodePair encodes and both matrices, and machines are either multitape Turing machines (TM) or logarithmic-word RAMs (RAM) whose word operations are themselves implemented by Turing machines in time polynomial in the word length.
There are absolute constants and such that for every fixed , either convention, either input class (all graphs, or connected graphs of diameter at most two) and every correct deterministic decider in either machine model, there is with
The exponent constant is independent of and of the program; the threshold may depend on both. The bound holds at every large order, not only infinitely often.
The result. Theorem 1.1 rules out any running time with , unconditionally. Earlier lower bounds either concerned the number of refinement rounds, assumed ETH, or treated the dimension as part of the input (coNP- and EXPTIME-hardness), which does not give a fixed-dimension exponent. It covers both standard update conventions and the restricted class of diameter-two graphs.
Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. The Lean statement fixes explicit machine models, so a proof would include a verified padded diagonalization (Theorem 5.2), a verified computation-to-graph reduction (Theorem 4.3) and a verified compressed consistency construction (Theorem 3.2).
Unconditional time lower bounds in concrete models are rare; the only general technique is diagonalization, which yields hard languages but not hard natural problems. The proof must therefore transfer a diagonal language to WL equivalence through a reduction that is efficient enough to preserve an exponent linear in . A polynomial-time computation with exponent proportional to has too many addressed locations to list in a small reduction, and local consistency is symmetric whereas a computation must propagate information forward without forcing false predecessors to become true.
Decides A c k p requires halting and correctness on every pair in the input class at every order ; worstTime is a Finset.sup over pairs in the class.ℝ.The statement is not vacuous: correct deciders exist (direct refinement), so the conclusion constrains real algorithms.
Needed infrastructure: bijective pebble games and their equivalence with refinement (Lemma 2.3), Turing machine simulation and clocking, and the graph constructions of Sections 3–4. Contributions toward any of these components are welcome.
The Weisfeiler–Leman (WL) algorithm refines colors of vertex tuples to test graph isomorphism, and its dimension controls how much tuple information is used. A graph's Weisfeiler–Leman dimension is the least for which -WL refinement identifies , i.e. distinguishes it from every non-isomorphic graph. This is a standard measure of the descriptive complexity of an individual graph, tied to counting logics and pebble games. The question here is how hard it is to compute: given and , decide whether .
Identification differs from testing whether a given pair of graphs is equivalent: it quantifies over every possible comparison graph. The preprint shows the problem is EXPTIME-complete when is part of the input.
All graphs are finite, simple, undirected and uncolored. For the joint-update convention is used: a -tuple starts with its equality and adjacency type, and each round adjoins the multiset over vertices of the vector of colors obtained by replacing each coordinate by . For ordinary color refinement is used. Colors are shared between graphs. means the tuple-color histograms agree at every round. -WL identifies if implies for every graph , and is the least positive such .
The decision problem takes a nonempty graph by its adjacency matrix and a positive integer in binary, and asks whether ; malformed inputs are rejected.
In Lean (OAI.WLIdentification), Graph is an order with a symmetric loopless Boolean adjacency on Fin order; Equivalent, Identifies and WLdim follow the definitions above; inputs are bit words consisting of a unary order header, the row-major matrix and the binary dimension; complexity classes are defined from an explicit deterministic single-tape Turing machine model (Machine, run, DecidesWithin, InEXPTIME, PolytimeManyOne, EXPTIMEComplete).
The language
is EXPTIME-complete under deterministic polynomial-time many-one reductions: it is decidable in time , and every EXPTIME language reduces to it in polynomial time.
The result. Theorem 1.1 settles the complexity of the input-dimension identification problem, strengthening the NP-hardness of Lichter, Raßmann and Schweitzer to EXPTIME-completeness. By Corollary 7.3 hardness persists with in unary, so it does not come from exponentially large numerical dimensions.
Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. A formal proof would include a verified reduction from arbitrary exponential-time Turing machine computations to graphs, and a verified upper bound for WL identification. The Turing-machine model and the WL definitions in the Lean statement are reusable for the companion missions on WL equivalence.
Hardness must handle the all-mates quantifier: an encoding of a computation into a graph must ensure that every graph that is -WL equivalent to it is isomorphic to it exactly when the computation accepts. Local recognition of gadgets, as in earlier NP-hardness proofs, shows each incidence piece of has an allowed pattern, but the encoding here admits a whole family of shifted constraints, and one must show every shift arising from an equivalent mate lifts to a single global isomorphism on accepting instances. Membership in EXPTIME is also not immediate, since identification quantifies over infinitely many comparison graphs.
Fin n-indexed Boolean adjacency matrices; the problem language requires a nonempty graph, a binary word with leading bit true, and a positive value.WLdim G is sInf of the positive identifying dimensions; this set is nonempty for finite graphs (dimension equal to the order identifies), so the infimum is not the default value.The goal is not trivial: membership in EXPTIME and hardness under the explicit machine model are both required.
Needed infrastructure: WL refinement monotonicity, pebble games or an equivalent characterization, CFI-type gadget constructions, and Turing-machine simulation. Contributions toward the upper bound (Proposition 7.1) or the reconstruction results of Sections 3–5 are welcome.
The Weisfeiler–Leman (WL) method is the standard combinatorial heuristic for graph isomorphism: it repeatedly refines colors of -tuples of vertices, and two graphs it cannot tell apart are called -WL equivalent. It is equivalent to counting-logic indistinguishability and, by results of Dvořák (2010) and Dell, Grohe and Rattan (2018), to equality of homomorphism counts from graphs of treewidth below (bags of size at most ). For fixed , direct refinement decides -WL equivalence in time; whether the growing exponent is necessary is a natural complexity question.
This preprint gives an exact reduction from a simple constraint problem (choosing compatible elements from finite domains) to -WL equivalence of two explicit uncolored graphs, and uses it to derive conditional time lower bounds.
Fix . The atomic type of a tuple records all equalities and adjacencies among its entries. In joint refinement a round records the old color of and the multiset over of the vectors . In separate refinement it records the old color and the multisets . Two graphs are -WL equivalent () when their tuple-color histograms agree at every round. The bag parameter is (joint) or (separate).
A choice system on domains consists of finite sets and, for each pair , a finite label set with maps , . A successful choice is with for all . Empty domains are allowed.
In Lean (OAI.ParityWL), ChoiceSystem t packages the domains and labels, template t is the -clique with helpers, baseGraph C replaces template types by domains and labels, and zeroLift C, starLift C are the two parity lifts. Colors are defined by recursion on rounds (jointColor, separateColor) with histograms compared as multisets.
For , either convention and the corresponding , for every choice system on domains the two explicit uncolored simple graphs have equal order and
both with common color names on separate graphs and with pure-tuple comparison in the disjoint union. If every domain and label set has size at most , the common order is at most with
When a successful choice exists, the histograms already differ after two joint rounds or one separate round.
The result. The reduction turns compatible-choice problems, which encode sparse satisfiability, into WL equivalence of uncolored graphs whose size grows only linearly in the domain size. Combined with sparsification it gives Theorem 1.3: under the positive-rate ETH there are , such that no deterministic algorithm decides -WL equivalence of -vertex graphs in time for fixed , even when only early-round histograms are compared. This addresses the expectation stated by Lichter, Raßmann and Schweitzer.
Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. A formalization would also give Lean definitions of both WL conventions, reusable by the companion missions in this family on identification and unconditional lower bounds. The ETH consequence (Theorem 1.3) is not part of the Lean goal.
The forward direction (a successful choice yields a distinguishing homomorphism test detected in few rounds) is constructive. The converse is the hard part: one must show that every bounded-treewidth homomorphism test that distinguishes the lifts yields a successful choice, even when bags do not induce cliques, projected images repeat, and some weights vanish. A naive argument that counts only type-preserving homomorphisms fails because non-type-preserving maps also contribute to .
SimpleGraph on finite types; the lifts' vertex types are sigma types of base vertices with parity tags.Multiset-valued types defined by recursion on the round number; equivalence quantifies over all rounds .orderFactor t = t * 2^(t-2+3*(t-1).choose 2) + 12 * t.choose 3 with natural-number subtraction (harmless since ).Successful is an existential over dependent tuples; empty domains are allowed, in which case no successful choice exists and the lifts must be equivalent.The goal is not trivial: the biconditional pins down equivalence exactly, and the detection clause fixes the round.
Needed infrastructure: tree decompositions and homomorphism counts, the Dvořák/Dell–Grohe–Rattan interface for both conventions, and linear algebra for the parity lifts. Contributions toward either direction of the equivalence are welcome.
Sensitivity and block sensitivity are two of the basic complexity measures of a Boolean function . Sensitivity counts how many single-bit flips change the value; block sensitivity allows disjoint groups of bits to be flipped together. Block sensitivity is polynomially related to decision-tree complexity, certificate complexity, degree and quantum query complexity, so the question of how it compares with sensitivity (the Sensitivity Conjecture, from Nisan's 1989 work on CREW PRAMs) decides whether sensitivity belongs to that same family. Huang's 2019 theorem settled the polynomial question: . Nisan and Szegedy had suggested the stronger bound , and the best known separations were quadratic.
This mission asks for a formal proof that no quadratic bound holds, as claimed in an OpenAI preprint dated September 25, 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 and , let be with the coordinates in flipped. For a total Boolean function ,
and is the largest number of pairwise disjoint nonempty sets with for every ; . Always , and a nonconstant has .
For every integer there are and a nonconstant with and
Since the right side tends to infinity, for every some nonconstant has , which is the first sentence of Theorem 1.1. The goal does not include the fixed-exponent statement of Corollary 4.3 (p. 10).
The result itself. It refutes the quadratic strengthening of the Sensitivity Conjecture suggested by Nisan and Szegedy and leaves the true exponent between and : Huang's theorem gives , while Corollary 4.3 of the preprint gives functions with for some and unbounded block sensitivity. Because spectral sensitivity is at most sensitivity, the separation also strengthens Meiburg's spectral result.
Formalizing it. The objects are finite and elementary, so a formal proof is a complete certificate of an explicit combinatorial construction. Huang's theorem has been formalized in Lean; a formal proof here would place the lower side of the gap on the same footing.
Known separations compose small gadgets, and composition multiplies both measures in a way that keeps the exponent at . To break it, a recursion must grow the number of disjoint sensitive blocks by a factor per level while ordinary sensitivity grows by only . The preprint's nested predicates on a labelled tournament (Section 2) achieve this, but a single bit flip can repair a failed gate condition only by changing two child predicates at once. Controlling sensitivity therefore requires tracking these joint sensitivities alongside ordinary ones at every input, not only at the input where the blocks are found (Proposition 3.1, p. 5), and the random edge labelling must exclude dense local configurations (Lemma 2.1, p. 3).
Fin n → Bool; flip x B flips the coordinates in a Finset. sensitivity and blockSensitivity are Finset.sup over all inputs of the local counts; block families are finsets of pairwise disjoint nonempty finsets, each of which changes the value.ℝ. Nonconstancy (∃ x y, f x ≠ f y) forces , so the division is genuine.Welcome contributions: a reusable library of Boolean-function complexity measures (sensitivity, block sensitivity, certificate complexity) and composition lemmas such as Lemma 4.2 (p. 9).
The discrete Fourier transform of length is computed by the fast Fourier transform with arithmetic operations, and this has been the benchmark since Cooley and Tukey (1965). Whether operations are necessary is one of the basic open questions of algebraic complexity theory. Lower bounds of order are known only under restrictions on the algorithm: bounded coefficients, unitary gates on exactly registers, or bounded conditioning of intermediate maps. In the unrestricted model of linear circuits, where coefficients are arbitrary complex numbers and only arithmetic operations are counted, the question remained open. This mission concerns that unrestricted question.
The source of this mission, an OpenAI preprint dated September 25, 2026, claims that the lower bound fails in the unrestricted complex linear-circuit model.
For let and . A linear circuit of length has inputs and the constant , followed by a finite sequence of gates. Each gate computes , or from previously available values , where is a fixed coefficient; each gate costs one. Values may be reused arbitrarily, and the outputs are designated available values. The circuit computes if its outputs equal for every . Coefficients may depend on and have no bound on size or description; depth, storage and conditioning are unrestricted. Let be the minimum number of gates.
equivalently: for every and every there are and an exact circuit for with fewer than gates. The Lean statement OAI.ExactFourier.main_theorem is this second form and is open on the platform.
The statement does not assert an upper bound for every length, a uniform construction, or anything about numerical stability. A companion OpenAI preprint gives a quantitative all-length bound in a model that also charges coefficient preparation; that result is not part of this mission.
The theorem refutes the assertion that for some fixed and all large in the unrestricted linear model. It shows that the known lower bounds necessarily depend on their restrictions (bounded coefficients, conditioning, unitary gates). The mechanism, a single finite tensor saving amplified through tensor powers, is a general tool: one strict improvement over the standard axis-by-axis algorithm for one tensor power of one nonmonomial matrix yields an exponent improvement for all tensor powers.
The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. The existence part of the argument is non-constructive (it proceeds by contradiction through price functions and compactness), so a formal proof is a meaningful check.
Leading-constant improvements of the FFT do not change the scale, and every classical structural algorithm (Cooley–Tukey, Good–Thomas, chirp) has that scale. A gain in the exponent of the logarithm needs a saving that compounds across many tensor factors; but a saving for one tensor power of a small matrix does not obviously transfer to Fourier matrices of growing length, because Fourier factorizations introduce diagonal twiddle factors and change the coordinate set. In addition, the existence of a single finite saving is itself not exhibited explicitly and must be proved.
Gate w is add i j, sub i j or scale c i with c : ℂ, referencing the values available so far.Program n k is a list of gates in topological order; values are the inputs and value is the constant (via Fin.snoc x 0).Circuit n has size, a program of that size, and outputs : Fin n → Fin (n+1+size); output selection is free.fourierMatrix n j k = zeta n ^ (j*k) with zeta n = exp(2πi/n); Computes is equality with mulVec for every input.MainStatement: for every real and there are and a computing circuit with size < c * n * logb 2 n.A complete development needs tensor products of matrices and circuits, the Chinese Remainder (Good–Thomas) identification of with for coprime , a Toeplitz/Vandermonde factorization of on its own coordinates, and the price-function existence argument (separation, compactness, feedback). Contributions formalizing Lemma 2.3 (tensor amplification) and Proposition 3.4 (transfer of a finite win to Fourier circuits) are natural first steps.
Two-way deterministic finite automata (2DFAs) recognize exactly the regular languages (Rabin and Scott; Shepherdson, 1959), but letting the head revisit the input can change how much finite control is needed. In 1978 Sakoda and Sipser asked for the state cost of converting one-way and two-way nondeterministic automata into 2DFAs: is a polynomial number of states always enough? They identified a complete witness family , now called one-way liveness, whose letters are binary relations on an -element set; a word is live when the product of its letters is nonempty. Lower bounds against unrestricted 2DFAs — whose head may reverse anywhere and arbitrarily often — have been the difficult part of this question.
An automaton has a finite set of states and a read-only head on a word over an alphabet , bracketed by two distinct endmarkers. The head starts on the left endmarker in the initial state; each transition depends on the current state and scanned symbol, changes the state, and moves the head left, right or not at all, never across an endmarker. A deterministic rule gives at most one successor (rules may be partial); a nondeterministic rule allows several. Acceptance means some finite computation reaches an accepting state; infinite nonaccepting computations reject. Two conventions are considered: under the first, an accepting initial configuration counts; under the second (positive convention) at least one transition is required. All states are counted.
For let be the monoid of binary relations on with path-order product, iff and for some , and identity . The one-way liveness language is
where the empty product is , so the empty word is live.
For every :
The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. The theorem gives an exponential separation between one-way nondeterministic automata and unrestricted two-way deterministic automata, improving the quadratic bound of Adeogun and Kapoutsis to an exponential one. Corollary 1.2 of the source deduces that no polynomial bounds the deterministic two-way state cost of -state 2NFAs uniformly over all finite alphabets. The alphabet has letters, so the result does not address a fixed alphabet or logarithmic-space complexity classes. A companion OpenAI preprint uses the same language to prove an exponential lower bound for complementing 2NFAs.
Formalizing it. The statement is a finite combinatorial claim about two explicit machine models. A formal proof would certify the passage from deterministic computations to products in the Brauer diagram monoid and the rank-loss induction with explicit constants ( conjugates, additions, step ).
Earlier exponential bounds rely on restricting how often the deterministic head reverses; an unrestricted 2DFA may revisit a cell arbitrarily often as input length grows, and crossing-sequence arguments then lose control. The central obstacle is to represent repeated visits to a cell by an object that depends only on that cell's symbol, not on its neighbors, so that the machine induces a monoid map onto the relation monoid. Once such a representation exists, one still needs a lower bound on its size that grows exponentially in rather than polynomially.
BRel (Fin h), a structure wrapping Fin h → Fin h → Prop, with the monoid structure given by path-order composition and identity Eq; OWL h is the set of words whose List.prod relates some pair.Symbol Alpha adds left and right endmarkers; moves are left | stay | right; head positions are Fin (w.length + 2) and Move.Rel fixes the position change.NMachine Alpha n and DMachine Alpha s have state types Fin n, Fin s, a set of accepting states, set-valued or Option-valued transitions, and boundary axioms forbidding left moves on the left endmarker and right moves on the right endmarker.FiniteRun positive uses TransGen (at least one step) when positive = true and ReflTransGen otherwise; Recognizes positive L means acceptance exactly on L.NoLeft forbids left moves in the source automaton. The recognizer clause quantifies over both conventions with the same machine.(h - 2) / 31, and s ranges over all natural numbers (an s = 0 machine has no states and cannot recognize the language).Given a finite collection of strings, the shortest common superstring (SCS) problem asks for a shortest string that contains every member of as a contiguous substring. It is a basic model of sequence assembly (reconstructing a long DNA sequence from overlapping fragments) and of data compression, and it is a standard test problem for approximation algorithms. Computing the optimum exactly is hard — Blum, Jiang, Li, Tromp and Yannakakis showed the problem is MAX SNP-hard, so it has no polynomial-time approximation scheme unless P = NP (Blum et al., J. ACM 1994) — so the natural question is the best constant factor achievable in polynomial time. For decades the target has been factor : the classical Greedy conjecture asserts that repeatedly merging the pair with maximum overlap achieves it.
A string is a finite list of symbols; a string is a substring of if for some strings (the empty string is a substring of everything). For a finite list of strings, a common superstring is a string having every as a substring, and
where counts symbols. The alphabet is unbounded: each symbol is given by an explicit binary label, and the input is measured by its total encoded bit length . An algorithm runs in polynomial time if its running time on a bit-level machine is bounded by a polynomial in .
In Lean (namespace OAI.Superstring), a symbol is List Bool, a word is a list of symbols, and an instance is a list of words. Substring containment is Mathlib's infix relation <:+:, opt S is the infimum of lengths of common superstrings, and HasPolynomialImplementation f asks for a Mathlib Turing.TM2ComputableInPolyTime certificate for f with respect to an explicit self-delimiting binary encoding of instances and outputs, with every stack alphabet finite.
There is a function from instances to words, computable in polynomial time in the encoded input length, such that for every instance
The goal is published on the platform with status Open.
The result itself. Factor has been the conjectured benchmark for SCS since 1988, and the best proved polynomial-time ratio before this preprint was (reported in 2026). Theorem 1.1 reaches factor with a new algorithm rather than with Greedy, which a 2026 preprint reports does not achieve factor .
Formalizing it. The statement mixes three components that are each easy to get subtly wrong on paper: the correctness of the output (contiguous coverage of every input), the ratio against the unrestricted optimum, and a running-time bound measured in bits, with symbols of arbitrary label length. The formal statement pins down all three with an explicit machine model. A complete formalization requires both the combinatorial ratio proof and a verified polynomial-time implementation on Mathlib's stack-machine model, which is substantial reusable infrastructure for complexity statements in Lean.
The classical approach builds the overlap (distance) graph, takes a minimum-weight cycle cover as a lower bound, and then opens and concatenates the cycles; the cost of joining cycles is what has kept ratios above . Greedy, the natural candidate for factor , is reported to fail. Any factor- algorithm needs a lower bound on that is tight enough that the cost of connecting all the pieces can be charged to the lower bound a second time without double-counting, uniformly over periodic and highly repetitive inputs. The polynomial running time must also be established at the bit level, with symbols of unbounded encoded length.
List (List (List Bool)): duplicates and empty strings are allowed, and symbols are arbitrary bit lists, so the alphabet is unbounded.List.IsInfix), not subsequence containment.opt is a natural-number sInf; the set is nonempty because the concatenation of all inputs is a common superstring, so the junk value is never used. The ratio is measured in symbols.Turing.TM2ComputableInPolyTime for the encodings encodeInstance and encodeWord (prefix markers for list structure), together with finiteness of every stack alphabet, so the time bound is in input bits on a finite-alphabet machine. A function that is merely computable, or polynomial only in the number of symbols, does not satisfy the goal.In metric -median, a finite set (or ) of clients and a finite set of candidate facilities lie in a common finite metric with rational distances. Given an integer , one opens a nonempty set with and pays
Candidate facilities are part of the input and need not coincide with the clients. It is one of the basic clustering and facility-location objectives, and its approximability has been a testing ground for LP rounding, primal-dual methods and local search. A lower bound has long been known: if , no polynomial-time algorithm achieves a factor below in this candidate-facility model, by a reduction from Feige's coverage gap. The best polynomial-time algorithms had reached , leaving a gap between and .
This mission asks for a formal proof that the threshold is exactly , as stated in an OpenAI preprint dated September 24, 2026 (source): a deterministic polynomial-time -approximation for every fixed , and hence, under , an infimal approximation factor of exactly . The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
An instance consists of points with a rational distance table that is a metric (nonnegative, zero exactly on the diagonal, symmetric, triangle inequality), a client set , a facility set (index sets that may overlap), and an integer , encoded in binary. A feasible solution is a nonempty with . An algorithm is an -approximation if it always outputs a feasible with , and it is polynomial-time if it runs on a deterministic multi-stack Turing machine with finite alphabets in time polynomial in the encoding length.
For every fixed there is a deterministic polynomial-time algorithm which, on every instance, returns a feasible with
If , then
The infimum is not asserted to be attained.
The result itself. It closes the approximability of metric -median with specified candidate facilities up to arbitrarily small additive error in the factor, ending a sequence of improvements from LP rounding through local search (), bi-point rounding (, ) to . It shows that the FPT factor of Cohen-Addad et al. is achievable in polynomial time. The case has a different and still separate lower-bound question.
Formalizing it. The goal combines an algorithmic theorem with a hardness reduction. A formal proof needs: the Li–Svensson reduction from constant-additive pseudo-approximations (Theorem 2.2, p. 4); the grid preparation and iterative rounding with a finite directed comparison inequality whose scalar estimates are proved by rational polynomial certificates (Sections 3–5, Appendix A); derandomization by moment-matching distributions of polynomial size (Section 6); and, for the lower bound, NP-hardness of Feige's coverage gap in the Lean computation model. All are reusable for other clustering and covering problems.
Two obstacles meet. The cardinality budget is hard: allowing a constant number of extra facilities makes good connection cost much easier, and earlier rounding analyses in the iterative graph framework only certify factors at least (p. 2). The preprint's new ingredient is a potential that keeps track of surviving assignment copies after an opening and a finite directed comparison inequality (Theorem 4.1, p. 13) that pays for erasures. Then the randomized rounding must be made deterministic and polynomial-time while keeping the analysis valid, which requires preserving exactly the low-order moments the analysis uses (Lemma 6.1, p. 28; Theorem 6.2, p. 33), before Li–Svensson removes the additive surplus. The hardness side is classical but rests on the PCP-based Max--Coverage gap.
Instance carries n, a Fin n → Fin n → ℚ metric (distance_eq_zero is an iff, so a true metric), client and facility Finsets, and 1 ≤ k ≤ facilities.card. cost sums nearest distances over clients; optimum is the minimum over nonempty facility subsets of size .FactorCorrect α I out requires that mask to describe a nonempty with and .Turing.TM2ComputableInPolyTime with finite tape alphabets, on the fixed binary instance encoding.approximationFactors is the set of admitting such an algorithm, and the goal is sInf approximationFactors = 1 + 2/Real.exp 1 under the hypothesis Complexity.PNeNP, where P and NP are defined in the same machine model (NP via polynomial-length witnesses and a finite-alphabet polynomial-time verifier). The set is nonempty by the milestone and bounded below, so sInf is meaningful.In metric -median, a finite set (or ) of clients and a finite set of candidate facilities lie in a common finite metric with rational distances. Given an integer , one opens a nonempty set with and pays
Candidate facilities are part of the input and need not coincide with the clients. It is one of the basic clustering and facility-location objectives, and its approximability has been a testing ground for LP rounding, primal-dual methods and local search. The hard part of the problem is the facility budget: a solution with small connection cost is much easier to find if a few extra facilities may be opened, and every approximation algorithm must eventually enforce on its output.
This mission concerns two tools for enforcing that budget and their combination into a randomized approximation strictly below factor on arbitrary finite rational metrics, 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.
Write and . A comparison solution of size assigns each client to a nearest member of (ties broken by fixed priorities); is the cluster of and , with . An anchor is a supplied feasible with . A certificate partitions into good and bad centres and gives distinct proxies for the good centres. A randomized polynomial-time algorithm is a polynomial-time multi-stack Turing machine that reads the encoded instance together with a string of fair random bits whose length is a fixed polynomial in the input length.
Let be disjoint, with distances between distinct indices positive integers bounded by a fixed polynomial in . Fix , and a rational . There is a randomized algorithm that, given an anchor with and a failure parameter , always returns with , runs in time polynomial in and , and, whenever some comparison solution of size and cost admits a certificate with
satisfies with probability at least . The algorithm is not given , or the certificate.
There is an absolute constant such that for every fixed some randomized polynomial-time algorithm for metric -median always returns a feasible (nonempty, , ) and satisfies
The result itself. Theorem 1.1 makes the running time single-exponential in the number of clusters without accurate proxies, so logarithmically many exceptions are tractable; FPT methods with dependence do not give this by setting . Combined with a new proof of bounded-price strictness for one compatible execution of the logarithmic-surplus construction of Cohen-Addad, Grandoni, Lee, Schwiegelshohn and Svensson (Lemma 8.1, p. 43), it yields Theorem 1.2: a randomized approximation strictly below , both with high probability and in expectation, that opens at most facilities on every output. A companion preprint proves a stronger deterministic bound by an independent route; Theorem 1.2's interest is the way recovery and payment accounting together enforce the budget.
Formalizing it. The statements are fully explicit about the machine model, the random bits, and the input encoding. A formal proof would need local-search anchoring (Theorem 3.3), leader/ball sampling with amortized radius guesses (Section 4), a finite categorical continuous-greedy algorithm with explicit error (Lemma 5.1, p. 21), the surplus construction as an external interface (Theorem 7.1, p. 35), and metric rounding and transfer (Lemma 2.1, p. 6). The submodular-optimization and local-search components are reusable.
Every factor- dual-fitting argument charges to a client set served by a comparison facility, which gives exactly ; improving the constant requires saving on connection cost while still paying for all regular openings with one final price, one set of copy lengths and the budgets of one actual replay of the construction (Section 1.2, p. 3). On the recovery side, guessing a good solution from an anchor naively costs ; keeping the dependence single-exponential in the number of bad clusters requires interleaving leader sampling and removals and amortizing radius guesses over disjoint client sets (Section 4). Theorem 1.1 holds only for normalized integral metrics; the global application must construct its anchors after normalization and transfer the final cost bound back (Lemma 2.1, p. 6).
RationalMetricInput: points Fin pointCount, a rational pseudometric table (zero on the diagonal, symmetric, triangle inequality), client and facility Finsets covering all points (they may overlap, so clients and facilities may share locations), a nonempty facility set and a positive budget . Feasible S is , , and nonempty when there are clients; optimum minimizes over nonempty subsets of size .BinaryRandomizedAlgorithm is a TM2ComputableInPolyTime function of (input bits, random bits) with finite alphabets, using randomBits.eval (input length) fair bits; probabilities and expectations are uniform averages over all seeds.Real.rpow); the same algorithm must also satisfy the expectation bound.Input adds disjointness of and , integral distances, positivity between distinct indices, and an anchor with anchor.card = budget; Bounded bound caps distances by a fixed polynomial in ; ζ is passed in unary precision , and PolynomialWork bounds work by . A Certificate encodes with , , the good set, injective proxies into the anchor, the proxy-cost promise with lexicographic tie-breaking, and at most bad centres.A set of unit-length jobs with precedence constraints is to be run on a fixed number of identical machines so that all jobs finish as early as possible. For two machines this was solved in 1969–1972; for a number of machines given as part of the input the problem is NP-complete (Ullman, 1975). Whether the problem is polynomial-time solvable for three machines, written , is problem OPEN8 in the appendix of Garey and Johnson's 1979 book and is one of the best-known open questions on the complexity of scheduling.
The source of this mission, an OpenAI preprint dated September 24, 2026, claims a deterministic polynomial-time algorithm.
The input is a directed acyclic graph on , , given as an explicit list of arcs, and optionally an integer deadline with . A feasible schedule with makespan at most is a map
such that each value is taken at most three times (three machines) and for every arc (precedence). Slot means execution during . There are no release dates, communication delays or other resources. The input length is the length of the binary encoding of the graph and deadline.
There is a single deterministic multitape Turing machine and a constant such that, on every such input of length , halts within
steps and
The exponent is the one stated in the paper and is not optimized; the content of the theorem is that a fixed polynomial bound exists. The Lean statement OAI.ThreeMachine.main_theorem is open on the platform.
The theorem resolves the polynomial-time side of Garey and Johnson's OPEN8: unit-job makespan scheduling with arbitrary precedence constraints on three identical machines lies in P. Previous exact algorithms were either restricted to special precedence structures (forests, bounded height) or subexponential, and approximation schemes did not decide the optimum. The structural statement behind the algorithm, that feasible schedules admit recursive decompositions whose interval job sets have descriptions of bounded size, may be of independent use for other fixed-machine scheduling problems. No practical running time is claimed.
The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. A formal proof would also certify the running-time analysis in an explicit machine model, which is rarely done for algorithmic results of this size.
Removing selected slots from a feasible schedule leaves gaps that can be rescheduled independently, which suggests a recursive search over the job sets of gaps. The obstacle is their number: naming a gap by its two boundary triples does not determine its job set, and intersecting descriptions inherited from ancestors can make the descriptions grow without bound along a recursion of linear depth. The subexponential decomposition of Nederlof–Swennenhuis–Węgrzycki controls the number of subproblems only up to ; a polynomial bound needs every subproblem to have a global description of constant size.
Instance n is a list of arcs on Fin n; acyclic forbids a Relation.TransGen cycle. Jobs are Fin n (shifted to in the encoding).Feasible G T τ: slots in , at most three jobs per slot, strict precedence.CorrectOutput distinguishes the optimization mode (none) and the decision mode (some T).Machine k q g over Fin (g+3) with tapes; input on tape 0 encoded by encodeInput (self-delimiting binary numbers), output read from tape 0 after halting. The time bound is with the encoded length.A complete development needs the combinatorics of the decomposition (separators and bounded global descriptions), a dynamic program over polynomially many descriptions, and its implementation and time analysis on the given Turing machine model. Contributions formalizing the purely combinatorial structure theorem, independently of the machine model, are welcome.
In the trace reconstruction problem an unknown binary word is passed repeatedly through a deletion channel: each bit is deleted independently with known probability and the surviving bits are concatenated in order. Each output, called a trace, reveals its length and its bits but not which positions survived. The question is how many independent traces are needed to recover every word exactly with a fixed success probability. The problem arises in DNA storage and sequencing, in multiple sequence alignment, and as a basic test of how much information a channel with synchronization errors destroys. Its central open question has been whether a polynomial number of traces suffices at a fixed deletion probability.
Fix and . A deletion mask keeps bit when ; it has probability . The trace of under is the list of the bits with , in order. Write for the law of the trace of under a random mask.
An estimator with budget receives independent traces of and returns a random word; it may be randomized and its computation is unrestricted. For , the sample complexity is the least such that some estimator recovers every with probability at least ; it is if no finite works. The one-trace distance is
the sum running over all finite binary words.
In Lean (namespace OAI.TraceReconstruction), words are Fin n → Bool, traceMass q x w is the probability of output w, an estimator is a function A : (Fin m → Trace) → Word n → ℝ giving a probability vector for each sample, sampleComplexity n q s : ℝ≥0∞ is the infimum of sufficient budgets, and minTraceTV n q is the minimum of traceTV q x y over .
Fix and . For every sequence of instances with , and ,
At fixed this gives , so no polynomial number of traces suffices. The goal is published on the platform with status Open.
For every fixed and every ,
The result itself. Theorem 1.1 is the first superpolynomial lower bound for exact worst-case trace reconstruction at a fixed deletion probability; previous lower bounds were of order up to logarithms. It holds against unrestricted computation and any fixed positive success probability, and it settles in the negative the question of whether polynomially many traces suffice. Combined with the 2026 quasipolynomial upper bound of Burudgunte, Valiant and Wang, the sample complexity at fixed is now known to lie between and . Theorem 1.2 isolates the underlying phenomenon: some pairs of distinct words have single-trace laws closer than every inverse polynomial.
Formalizing it. The definitions fix exactly what an estimator may see (only the complete traces, no positions or boundaries) and what "sample complexity" means, including the value . A formal proof would certify a lower bound whose argument is a long multi-scale construction with many quantitative error budgets, the kind of argument where an overlooked loss would invalidate the conclusion.
Earlier lower bounds compare two words that differ by a single local defect and compute their trace distance directly; such pairs are distinguishable from polynomially many traces, so no single-defect construction can give a superpolynomial bound. A superpolynomial bound needs pairs of words whose trace laws agree to every polynomial order, while the argument must remain uniform in the deletion probability (which may tend to slowly), keep all constants below scale margins that shrink as the number of construction stages grows with , and transfer a bound for one trace to a bound for independent traces and for arbitrary randomized estimators.
List Bool; traceTV sums over the finite set of all lists of length at most , which contains the support of every trace law, so it agrees with the source's total variation over all finite words.sampleComplexity is an sInf in ℝ≥0∞; the infimum of the empty set is , matching . The lower bound is compared after ENNReal.ofReal, and the right-hand side uses the real power.n q : ℕ → …, Tendsto n atTop atTop, and Tendsto (q k ^ 3 * log (n k)) atTop atTop; the conclusion is ∀ᶠ k in atTop. Logarithms are natural.minTraceTV n q is a real sInf, attained for ; at the set is empty and the junk value does not affect the limit.Sparsest cut asks for a partition of a weighted graph whose crossing capacity is small compared with the demand it separates. It is a basic graph-partitioning primitive (used for divide-and-conquer algorithms, clustering and expansion testing), and its relaxations are the main bridge between approximation algorithms and the geometry of finite metric spaces. In the uniform version every pair of vertices has demand one. The best known polynomial-time approximation, due to Arora, Rao and Vazirani, uses the Goemans–Linial semidefinite relaxation and achieves ratio . How good this relaxation can be, i.e. its integrality gap on uniform instances, has been a long-standing question.
For uniform demands the gap between the lower bound and the upper bound remained. The source of this mission, an OpenAI preprint dated September 24, 2026, claims a lower bound matching the upper bound up to a power of .
Let be symmetric nonnegative capacities on pairs of distinct vertices of . The uniform sparsest-cut value is
A negative-type semimetric is for vectors in a real Hilbert space, satisfying all triangle inequalities ; distinct points may have distance zero. The Goemans–Linial value is
Normalized cut metrics are feasible, so . The integrality gap of is .
There are an absolute and instances on vertices with such that, for all large ,
The Lean statement OAI.UniformSparsestCut.mainGap is open on the platform.
The bound reaches the exponent in , so the Arora–Rao–Vazirani analysis of the Goemans–Linial SDP is tight for uniform demands up to the factor . It strengthens the Devanur–Khot–Saket–Vishnoi and Kane–Meka refutations of the uniform constant-gap conjecture. Geometrically, it gives a finite negative-type metric for which every -Lipschitz map into preserves only a fraction of the average distance. The theorem concerns the basic Goemans–Linial SDP only, not strengthened hierarchies.
The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists.
The sharp general-demand lower bounds (Heisenberg group, Naor–Young) control worst-pair distortion, and Cheeger–Kleiner–Naor note that those examples have constant average distortion into a line, so they cannot give a diverging uniform gap. A uniform-demand example must force every contraction to lose most of the average distance over all pairs, not merely on a few pairs. At the same time the constructed distance must remain of negative type and satisfy all triangle inequalities exactly, and the passage from a probability measure on points to an exactly uniform demand with positive SDP value must be carried out without losing the bound.
Capacity n stores cap : Fin n → Fin n → ℝ, nonnegative, symmetric, zero on the diagonal.cutRatio C B is the crossing capacity of divided by ; OPT C is the sInf over nonempty proper Finsets .NegativeType d requires points x : Fin n → EuclideanSpace ℝ (Fin n) with and all triangle inequalities; Feasible d adds ; glValue C is the sInf of over feasible .A complete development needs cut-cone duality, a Hilbert-space kernel construction with rounded charts, Gaussian direction families, and contraction estimates for maps into . Cut-cone duality and the reduction to exactly uniform demands are reusable. Contributions formalizing Lemma 6.1 (cut-cone duality) or the weak duality are welcome first steps.
A cell-bounded contingency table is a nonnegative integer matrix with prescribed row sums, column sums and an upper bound on each entry. Bounds of zero forbid entries (structural zeros), and bounds of one give bipartite graphs with prescribed degrees, so the model contains degree-constrained subgraph counting and perfect matchings (the permanent). Counting such tables is central to exact conditional inference in statistics and is equivalent to counting integer flows in bipartite networks. Exact counting is #P-complete even for two-row ordinary tables (Dyer, Kannan and Mount, 1997), so the target is a fully polynomial randomized approximation scheme (FPRAS): a randomized algorithm that, for any , returns a -approximation with probability at least in time polynomial in the input length, and .
The source of this mission, an OpenAI preprint dated September 24, 2026, claims an FPRAS with no restriction on dimensions, margins or caps.
For positive integers , margins , with equal totals, and bounds ,
All numbers are written in binary, so a capacity can be exponentially larger than its description. denotes the total binary input length including the rational accuracy parameters . The algorithm uses independent unbiased random bits and is charged for every bit operation.
One randomized algorithm, given and rational , outputs a nonnegative rational with
outputs exactly on every execution when , and performs at most bit operations on every execution. Lean: OAI.ContingencyTables.counting, open on the platform.
The theorem would answer the question left open by Cryan, Dyer and Randall in 2010: approximate counting of cell-bounded tables (equivalently, integral flows in bipartite networks with arbitrary capacities) without any fixed-dimension, large-capacity, density or balance assumption, with polynomial cost on every execution and no oracle. It contains the 0/1 case handled by Jerrum–Sinclair–Vigoda and the fixed-row results as special cases, and via self-reduction it gives approximate samplers for integer flows. A companion preprint of the same family treats exact uniform sampling of uncapped tables. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists.
Two regimes clash. Large capacities cannot be expanded into that many binary choices without exponential blow-up, so geometric (polytope volume) methods are needed for them; but those methods require every cell to be large. Small capacities need combinatorial Markov chains, which in turn must preserve exactly one unit of mass per table despite the multiplicities created by encoding a bounded integer by binary choices. Arbitrary mixtures of tiny and huge caps, zero caps and variable dimensions defeat each approach used alone.
MatchingFPRAS.RandomMachines: a single finite transition table on an 8-symbol alphabet, one random bit per tick; time is counted in ticks (polynomially equivalent to bit operations).encodeCountingInput); outputs are encoded rationals.count r c b is Fintype.card of bounded tables.CountingStatement: one machine and constants , ; with , every tape of length halts with a rational ; if count = 0 every tape outputs ; and the fraction of tapes with is at least .Needed infrastructure: randomized Turing machines, Markov chain mixing and Poincaré inequalities, log-concavity (Prékopa–Leindler), and network-flow feasibility. The machine model and encodings are shared with the exact-sampling mission of this family. Contributions formalizing Proposition 2.2 (contamination bound), Lemma 3.3 (log-concave tree marginals), Proposition 6.1 (weight evaluation) or Proposition 7.2 are welcome.
A contingency table with margins and is a nonnegative integer matrix whose row sums are and column sums are . Such tables are the basic objects of categorical data analysis: conditional tests of independence (Fisher's exact test and its generalizations) compare an observed table with the uniform distribution on all tables with the same margins, and in practice this requires sampling uniformly from that set. The set is finite but can be exponentially large in the input size when margins are written in binary. Whether one can sample it (approximately or exactly) in time polynomial in both dimensions and in the bit length of the margins has been open since the 1990s.
The source of this mission, an OpenAI preprint dated September 24, 2026, claims both an almost-uniform and an exactly uniform sampler for arbitrary margins.
For nonnegative integer vectors , with common total , let
The input is with margins in binary, so its length is polynomial in , and . An algorithm uses unbiased random bits. For laws on a finite set, .
For each , an algorithm halts on every execution in time and outputs with
An algorithm outputs with
terminates almost surely, and has expected running time , with polynomials uniform over all margins. Lean: OAI.ContingencyTables.exactSampling, open on the platform.
The theorem would give the first unconditional polynomial-time exact uniform sampler for contingency tables with arbitrary dimensions and binary margins, with no positivity, sparsity, balance or fixed-dimension restriction, and with all random bits and integer arithmetic counted. It removes the fixed-row restriction of the Dyer–Greenhill and Cryan–Dyer line and the sparsity condition of Arman–Gao–Wormald. The exponents are deliberately large; the contribution is the existence of a polynomial algorithm. Exact time is polynomial in expectation, not on every run. A companion preprint of the same family gives an FPRAS for counting tables with cell bounds. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists.
Markov-chain approaches mix rapidly for a fixed number of rows, but the bounds degrade with the row count. Geometric (polytope) methods need all margins to be large, and fail when some margins are tiny while others are huge, which is exactly the mixed regime that arbitrary binary margins allow. Making the sampler exact rather than approximate adds a separate difficulty: the residual-mixture correction requires that the actual output law of the approximate sampler can be computed, with cost polynomial in the accuracy bits.
MatchingFPRAS.RandomMachines: a single finite transition table over an 8-symbol tape alphabet; each tick reads one random bit and either moves, writes or halts. Time is counted in ticks, polynomially equivalent to bit operations.encodeNat, encodeMargins); outputs are row-major matrix encodings left on the tape (OutputsTable).tableMass A input t X and haltMass A input t are the fractions of the random tapes of length that halt with output , respectively halt at all, within ticks.ExactSamplingStatement: one machine and constants , such that for all with equal totals: every halted output is in ; tableMass → 1/|Ω| for each table; haltMass → 1; and , the expected running time, is at most .BoundedSamplingStatement: every tape of length halts with a feasible table, and the TV distance to uniform is at most .Needed infrastructure: randomized Turing machines and their output laws, Markov chain mixing (conductance, Poincaré inequalities), and log-concave sampling. Contributions formalizing Theorem 4.3 (graph Poincaré inequality), Theorem 5.1 (dense completion draw), Proposition 6.3 (law tabulation) or the Göbel–Liu–Manurangsi–Pappik correction are welcome.
A matroid abstracts linear independence: a finite ground set with a family of "independent" subsets that is closed under subsets and satisfies the augmentation axiom. Its maximal independent sets, the bases, all have the same size, the rank. Matroid intersection, finding a common basis of two matroids, is one of the central polynomially solvable problems of combinatorial optimization (Edmonds, 1979). Counting common bases is much harder. It contains counting bases of a single matroid (take both matroids equal) and counting perfect matchings of a bipartite graph (take two partition matroids), and exact counting is #P-hard. The natural goal is therefore a fully polynomial randomized approximation scheme (FPRAS): an algorithm whose output is within relative error with probability at least , in time polynomial in the input size, and . The matroids should be accessible only through independence oracles.
Let be matroids of the same rank on the ground set , supplied by exact independence oracles: a query is an -bit indicator of a subset, and the answer says whether it is independent. The quantity to estimate is
the number of common bases. The input also contains rationals ; denotes the binary encoding length of . Oracle calls are counted separately from the bit operations used to build queries and process answers.
There is a single randomized oracle algorithm and a fixed polynomial such that, for all rank- matroids on and rational , it outputs a nonnegative rational with
the output is always when , and on every execution the numbers of oracle calls and bit operations are at most . The algorithm uses only independent fair random bits. The goal statement is published on the platform with status Open.
The result itself. Theorem 1.1 answers the question recorded by Liu (2023) and extends both the single-matroid FPRAS of Anari–Liu–Oveis Gharan–Vinzant and, in the bipartite-matching case, the permanent FPRAS of Jerrum–Sinclair–Vigoda. It needs no representation of either matroid and holds for unrestricted rank, whereas the previous oracle-model scheme was fully polynomial only for . The source derives FPRASs and almost-uniform samplers for common independent sets of prescribed, unrestricted or maximum size, even for matroids of different ranks (Corollary 9.1).
Formalizing it. The Lean goal fixes a concrete machine model, so it states a complete complexity-theoretic claim with no informal "polynomial-time" left. A proof would combine Lorentzian-polynomial inequalities (Brändén–Huh), a transport inequality, a Markov-chain Poincaré bound, and simulated annealing with explicit bit accounting. Each layer is reusable: Mathlib has matroids, but no Lorentzian polynomials, no mixing-time theory of this kind and no randomized-algorithm framework.
For one matroid, the bases-exchange walk mixes rapidly because the basis generating polynomial is log-concave. The intersection of two matroids has no such structure: its common bases need not be connected by short exchanges, and the natural chain on transversals of the paired construction passes through states of exponentially small weight, so positivity and connectivity alone give no polynomial bound. Earlier approaches either lost exponential factors or needed real-stable polynomials that an independence oracle does not provide. The proof must balance defect classes, as in Jerrum–Sinclair–Vigoda, and establish a Poincaré inequality for observables from matroid-theoretic inequalities alone.
Matroid (Fin n) with ground set univ and eRank = r for both. Oracles are functions Bool → (Fin n → Bool) → Bool, required to answer independence queries exactly.Program k s for a register machine with binary stacks: push/pop, fair coin, oracle query on an -bit register, and halt with output (register 6)/(register 7) as a rational. Inputs are loaded in binary.Prescribing the probability that each edge belongs to a random perfect matching does not determine the distribution of the whole matching. The largest entropy compatible with those edge probabilities, , measures how many matching choices can coexist with them, and it links three topics: lower bounds on the number of perfect matchings, convex-optimization approaches to approximate counting, and the facial geometry of the perfect-matching polytope. For bipartite graphs, Schrijver's permanent inequality (Schrijver 1998) and Gurvits' weighted Bethe inequality (Gurvits 2011) give the clean comparison between and sums of one-coordinate entropies. For general graphs, odd cuts make such comparisons harder, and Anari, Oveis Gharan and Vinzant (2018) asked (FOCS version, Conjecture 6) whether the maximum binary-coordinate entropy over the polytope exceeds by only a linear function of the number of vertices.
Let be a finite loopless multigraph with vertex set , , and edge set (parallel edges are distinct coordinates). A perfect matching is a set of edges covering each vertex exactly once; is the set of them and . The perfect-matching polytope is
For put, with natural logarithms and ,
The milestones are listed in attack order: the face of a triangle expansion (Lemma 5.1), the coefficient-eight nonlinear bound (Theorem B.1), deterministic approximate counting (Theorem 1.2) and its singleton-loop variant (Proposition C.1).
If has at least one perfect matching, then for every
The bound holds on the whole polytope, boundary included. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. The upper bound is Shearer's inequality; the content is the lower comparison with coefficient , valid in nonbipartite graphs where the bipartite coefficient fails (the source gives an eight-vertex counterexample, and Corollary 5.3 shows any universal coefficient is at least ). Optimizing over gives , answering the Anari–Oveis Gharan–Vinzant question. Plugging in uniform marginals gives for graphs with edge-disjoint perfect matchings, and for -regular graphs whose odd cuts all have at least edges. The same entropy framework yields a deterministic polynomial-time algorithm approximating within a factor for graphs with binary edge multiplicities (Theorem 1.2).
Formalizing it. The goal is a finite-dimensional inequality about polytopes and entropies, accessible to Mathlib's convexity and analysis libraries. The milestones extend the mission to a certified polynomial-time counting algorithm in Mathlib's Turing-machine model, a rare example of a formally specified approximation algorithm for a #P-hard quantity.
Shearer's inequality gives the upper bound in one line, and in bipartite graphs the lower bound follows from permanent inequalities that have no analogue for general graphs. A direct convexity argument fails because is not differentiable across faces of : at a boundary mean the maximum-entropy law lives on a lower-dimensional face, and its covariance is singular in the ambient edge space. The lower bound must therefore be proved face by face, and it needs the sharp geometric estimate for the minimal face containing ; the earlier rank bound would not give the coefficient .
LooplessGraph V E: endpoint maps left right : E → V with left e ≠ right e, on finite types with decidable equality, so parallel edges are distinct elements of E. A perfect matching is a Finset E with exactly one edge at each vertex.polytope G is the convex hull of matching indicator vectors in E → ℝ; maxMatchingEntropy G x is sSup of the entropies of probability vectors on matchings with mean x. On the polytope this set is nonempty, compact and bounded, so the sSup is the attained maximum; off the polytope it would be junk, which is why the hypothesis x ∈ G.polytope is required.entropy uses Real.negMulLog, so ; complementEntropy x is .0 < m, Fintype.card V = 2 * m, and a perfect matching exists. The coefficient is the real number 2 - 2 / m.Turing.TM2ComputableInPolyTime with finite alphabets, binary encodings of the vertex count and of positive multiplicity records, and require polynomially bounded output length.TM2. The polytope and entropy definitions are reusable for other counting missions.A perfect matching of a graph is a set of edges covering every vertex exactly once. Finding one is easy — Edmonds (1965) gave a polynomial-time algorithm for general graphs — but counting them is hard: Valiant (1979) proved exact counting #P-complete already for bipartite graphs, where the count is the permanent of a 0–1 matrix. Exact counting is tractable only in special classes, such as planar graphs via Pfaffians (Kasteleyn 1963). The natural relaxation is a fully polynomial randomized approximation scheme (FPRAS): an algorithm that, with probability at least , returns the count within relative error , in time polynomial in the input size, and . Whether perfect matchings in general (nonbipartite) graphs admit an FPRAS was explicitly raised by Jerrum and Sinclair in 1989 and has been a benchmark question in approximate counting since. Perfect-matching counts are partition functions of the monomer–dimer model, so the question also connects to statistical physics.
A finite simple undirected graph on vertices is given by a set of edges, each written once as a pair with . A set is a perfect matching if every vertex lies in exactly one edge of , and
(The graph with no vertices has ; any graph with an odd number of vertices has .)
A randomized algorithm is modelled as a single fixed machine with a finite transition table over a finite tape alphabet, which at each step reads the current tape symbol and one fresh fair random bit, then writes, moves, or halts. The input is the graph in binary (number of vertices, number of edges, the sorted edge list) followed by the rationals and in reduced form; the output is a rational number written on the tape when the machine halts.
There are a machine and constants , such that for every graph and rationals , , with :
The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. The theorem answers the Jerrum–Sinclair question affirmatively: perfect matchings in arbitrary graphs can be approximately counted as efficiently, up to polynomial factors, as in the bipartite case. The worst-case time bound holds for every execution, not just in expectation. Via standard reductions, the source also derives counting schemes for edge subsets with prescribed vertex degrees and for matchings of a fixed size (Corollary 10.1). The accompanying samplers for those families always return a feasible object and approximate the uniform law in total variation.
Formalizing it. The statement fixes a concrete machine model, input encoding and time bound, so a formal proof would certify both correctness of the estimator and the polynomial running time of an explicit algorithm — a level of rigor rarely reached for Markov-chain Monte Carlo results, whose analyses involve many interacting constants.
The natural approach extends the Jerrum–Sinclair–Vigoda Markov chain on perfect and near-perfect matchings, with weights learned while edge activities are gradually lowered. In general graphs this approach provably fails: Štefankovič, Vigoda and Wilmes constructed graphs on which every chain of that type, for any hole-dependent weights, has either exponentially small stationary mass on perfect matchings or exponentially slow mixing. Odd cycles (blossoms) are the reason the bipartite canonical-path arguments do not carry over. A solution needs a different state space and a different mixing analysis.
GraphInput is a vertex count n and a Finset (Fin n × Fin n) of edges with strictly increasing endpoints, so loops and duplicate edges are excluded. Perfect G M requires M ⊆ edges and that each vertex is incident to exactly one edge of M; Z G is the number of such M.RandomMachine: a finite transition table on Fin 8 symbols, whose step consumes one random bit and performs a Turing.TM0 write or move, or halts. run folds tick over a list of t bits; halted configurations are absorbing.encodeInput writes the vertex count, edge count and lexicographically sorted edges in binary, then encodeRat ε and encodeRat δ (reduced numerator with sign, denominator). Outputs requires that the machine has halted and the tape to the right of the head is exactly the encoding of the output rational.RandomMachine transitions, Markov-chain spectral-gap bounds, and sampling-to-counting reductions. The machine model and encodings are reusable for other approximate-counting missions.Proving that explicit Boolean functions need large circuits is the central problem of circuit complexity. Even for very shallow circuits the known bounds are far from what counting arguments suggest. A depth-three OR–AND–OR circuit is an OR of CNFs, with unbounded fan-in and arbitrary sharing; most functions need gates in this model, yet for every explicit function in P the best known lower bounds had the form for a constant . Håstad's switching lemma gave for parity (1989), and Paturi, Pudlák and Zane showed this is tight for parity up to a constant factor (1999), so parity cannot go further. Moving the exponent beyond any constant multiple of for an explicit language was identified as an open problem in the depth-three literature (Gurumukhani, Paturi, Pudlák, Saks and Talebanfard, CCC 2024; Gurumukhani, Kleber, Paturi, Rosin and Talebanfard, CCC 2026). Depth-three lower bounds are also tied to satisfiability algorithms and to Valiant's approach to lower bounds for logarithmic-depth circuits.
This mission asks for a formal proof that one polynomial-time language requires depth-three gates, as stated in an OpenAI preprint dated September 23, 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 literal is a variable or its negation; negations are free. A depth-three OR–AND–OR circuit on inputs has bottom OR gates (clauses) reading literals and optional constants, middle AND gates reading bottom gates, and one top OR gate reading middle gates. Fan-in and fan-out are unbounded and gates may be shared. Its size counts every bottom gate, every middle gate and the output gate. For , is the least size of such a circuit computing exactly. For a language , is its membership function on .
There are a language , a deterministic multi-tape Turing machine deciding , and positive integers such that the machine halts within steps on every input of length , and for every real there is with
The language and machine are fixed before ; no uniformity or bottom fan-in restriction is imposed on the circuits.
The result itself. It is the first explicit depth-three lower bound whose exponent is not , crossing the barrier at which parity, majority and the earlier code-membership functions stop. It is weaker than the bound asked by Håstad, Jukna and Pudlák and gives no fixed improvement of the exponent's power. Because every function has a single-CNF representation when bottom fan-in is unbounded, the result depends on counting all gates, as stated.
Formalizing it. Circuit lower bounds are combinatorial statements well suited to formal proof, but the libraries are thin: a complete development needs a Turing-machine time bound for a concrete polynomial-evaluation language, restriction arguments for CNFs, the Erdős–Rado sunflower lemma, and limited-independence estimates from hashing and polynomial interpolation. All of these are reusable in complexity theory. No machine-checked depth-three lower bound beyond small cases is known.
The classical switching lemma changes the normal form and loses a constant in the exponent, which keeps bounds at the scale, and parity is provably no harder than , so a different hard function and a different argument are needed. The preprint needs a function whose sign has small correlation with every moderately wide CNF, independently of the number of clauses. Its key step (Lemma 3.1, p. 4) expresses each randomly restricted width- CNF as a signed combination of width- CNFs with expected coefficient mass at most two, with no dependence on the clause count. A uniform polynomial-time language cannot search for a hard function at each length, so hardness must come from inputs that carry the parameters selecting a hard slice (Section 5).
Circuit3 (Fin n) has bottomCount raw clauses (lists of literals or Boolean constants), middleCount AND gates given as Finsets of bottom indices, and a top Finset of middle indices; gateCount = bottomCount + middleCount + 1. Computes requires exact agreement with L (List.ofFn x) on every input.FiniteMultiTapeMachine has finitely many tapes, a finite alphabet, finite states, an input tape initialized with the input, and an accept predicate on the halting state. MultiTapeHaltsIn M w (L w) (C*(|w|+1)^a) requires halting within the bound with output L w.ℝ.In the -server problem, labelled servers occupy points of a metric space, requests arrive online, and each request is served by moving one server onto it; the cost is the total distance moved, compared with the offline optimum through the competitive ratio. A companion OpenAI preprint claims that on every metric there exists a randomized policy with ratio against oblivious requests, matching the known worst-case lower bound. That result is an existence statement: it gives no procedure for computing the policy's probabilities.
This mission asks whether the bound can be realized by one uniform algorithm with explicit bit complexity on all finite rational metrics, 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.
Fix and . A rational metric on is a table that is nonnegative, zero exactly on the diagonal, symmetric, and satisfies the triangle inequality. An initial labelled tuple may have repetitions. For a request word , is the algorithm's total movement and the minimum over all choices of serving labels with knowledge of . denotes the total binary length of the encoding of .
The computational model is a bit machine: a finite control with an input tape, finitely many work tapes over , an output channel, and one fresh unbiased random bit per step. At each request the input tape is replaced by the encoded request, the internal state is retained, and the output after the step budget names the server to move.
There are an absolute constant and a polynomial such that a single uniform randomized online algorithm, on every instance as above,
with independent of and of its length.
The result itself. It converts the existence theorem into an algorithm whose ratio is independent of , using only unbiased random bits and polynomial work per request in the input length and the bit length of the request counter. The price is an additive constant with no size bound: the algorithm may serve a very long initial stretch with a fixed label while its constructor runs. Coester and Cosson obtain stronger time and randomness guarantees but with ratio on general metrics; the two results are incomparable.
Formalizing it. The goal is stated in an explicit machine model, so a formal proof certifies both the competitive bound and the bit-complexity bound. It needs the companion existence theorem (Theorem 2.1 here, p. 4) as an input; a full development therefore also requires formalizing that theorem or taking it as a separate milestone. Exact rational linear algebra (Fourier–Motzkin elimination), dyadic rounding of probabilities, and step-counted machine simulation are reusable.
Knowing that a good policy exists does not give its probabilities, and a finite horizon alone does not control a long input on which the optimum barely moves. The preprint (pp. 3–4) solves a rational linear system for each horizon, then filters requests so that only those missed by some strongly lazy service with bounded moves are retained, which bounds the retained word length; a marking fallback pays for trajectories exceeding the move cap. The constructor's running time is uncontrolled, so the algorithm simulates it for only steps at request (Proposition 4.2, p. 14), and the delayed activation is absorbed into .
RationalMetric n is a Fin n → Fin n → ℚ table with the metric axioms; configurations are Fin k → Fin n; offlineCost is the sInf over label histories matching the request word (a finite, nonempty set of costs).BitMachine has finitely many controls and tapes and a transition consuming one coin per step. Preprocessing (boot) runs steps with all coins , so it is deterministic; this is satisfied by the source's deterministic constructor, and Theorem 1.1 does not require randomness there.requestBudget c e L t steps (Nat.clog 2 (t+1)) and must have yielded with output value for every reachable state and every coin string; requests are encoded by a fixed self-delimiting binary code.machineExpectedCost averages over all coin strings of the step budget, i.e. uniformly random bits; the bound is required for every request list w, with chosen after and before w.In the -server problem, servers sit at points of a metric space; requests arrive one at a time, and each request must be served by moving some server onto it, at a cost equal to the distance travelled. An online policy sees only the requests revealed so far, and its quality is measured by its competitive ratio: how much more it moves, in expectation, than the offline optimum that knows the whole sequence. The problem was introduced as a common framework for paging, caching and other online service problems, and the question of the best ratio achievable by randomized policies has driven the development of metric embeddings, online primal-dual methods and entropic regularization.
This mission asks for a formal proof that randomized -server has competitive ratio on every metric space, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
Let be a metric space and the initial positions of labelled servers; repeated positions are allowed. To serve a request , a policy chooses one label and moves server to , leaving the others fixed (a server already at may be chosen at zero cost). For a finite request sequence , is the total distance moved and is the minimum of this cost over all label sequences, chosen with knowledge of . A randomized online policy chooses, at each step, a probability distribution over labels as a function of the past requests, its own past choices and the current request. Requests are fixed in advance, independently of the policy's randomness (the oblivious adversary).
There is an absolute constant such that for every , every metric space with at least points, and every , there are a randomized online policy and a finite with
for every finite request sequence . The same policy serves all sequences and horizons; may depend on , and but not on ; and when the entries of are distinct.
The result itself. Combined with the Bubeck–Coester–Rabani lower bound, it identifies as the worst-case order of the randomized competitive ratio over all metrics. The bound has no dependence on the number of points, the aspect ratio, finiteness or boundedness of , removing the factor left by static tree embeddings. No computational efficiency is claimed; a companion preprint turns the existence statement into a uniform algorithm on finite rational metrics.
Formalizing it. The statement is elementary to state, but its proof combines a rank-based allocation on separated trees, slowly varying simplex trackers, a compact potential for partition edits, online partitions with an embedded comparator, balanced rounding, and a compactness argument (Tychonoff) producing one policy for all finite inputs. None of these online-algorithm tools exist in a formal library, and a machine-checked competitive analysis of a randomized -server algorithm on general metrics is not known.
Embedding the metric into a random hierarchically separated tree and running an tree algorithm loses the embedding distortion, which is in the worst case and is not bounded in terms of . Removing it requires changing the tree as requests arrive, and the cost of re-partitioning must be paid for. A previous dynamic approach (Lee's fusible HSTs) had its general claim withdrawn after a gap in that accounting (p. 3). In the preprint, the partition schedule is driven by the posterior measure of a hidden comparator, and the edit costs and the travel of parked mass are bounded separately (Sections 7–8). Passing from finite metrics and finite horizons to one policy on an arbitrary, possibly infinite and unbounded, space with a fixed constant requires a further compactness step (Section 10).
X : Type u carries an arbitrary MetricSpace instance; "at least points" is an injection Fin (k+1) → X. No finiteness, separability or boundedness is assumed.Policy k X maps the history (list of past requests with the labels used) and the current request to a LabelDistribution k, i.e. a probability vector on Fin k. Every step moves exactly one server (Function.update), as in the source.expectedCost is the finite sum over all label sequences of the path probability times the service cost; optimalCost is the sInf over all label sequences of the service cost (nonempty finite set, so the infimum is a minimum). Restricting the offline optimum to one-server-per-request service does not change it (triangle inequality).Function.Injective s → B = 0 encodes the distinct-start clause.Real.log).The permanent of an matrix ,
has the same monomials as the determinant but no signs. The determinant can be computed in polynomial time; the permanent is #P-hard (Valiant, 1979). Valiant's algebraic theory makes this contrast precise: the determinant is complete for small formulas and branching programs, the permanent is complete for the class VNP, and VP ≠ VNP, the algebraic analogue of P ≠ NP, would follow if the permanent cannot be written as a determinant of polynomially larger size with affine-linear entries. Mulmuley and Sohoni's geometric complexity theory reformulates this through orbit closures, which leads to the border version of the question studied here.
Until this work the best lower bounds for both exact and border determinantal complexity of the permanent were quadratic. The source of this mission, an OpenAI preprint dated September 24, 2026, claims a cubic lower bound in the border model.
For a complex polynomial , the determinantal complexity is the least positive integer with
The border determinantal complexity is the least positive such that is a coefficientwise limit of such determinants of size (the size stays fixed along the sequence; the matrices are arbitrary). Clearly .
If , , , and the lowest nonzero homogeneous term of has degree and defines a smooth projective hypersurface, then
For every ,
The constants are those stated in the paper and are not optimized. The Lean statement OAI.PermanentBorder.permanent_cubic_lower_bounds is open on the platform.
The theorem raises the exponent of the best lower bound for the permanent versus determinant problem from (Mignon–Ressayre, Landsberg–Manivel–Ressayre) to , in the border model and hence also in the exact model. Through determinant reductions it also gives lower bounds on the size of affine-linear algebraic branching programs for the permanent. It remains a polynomial bound: superpolynomial determinantal complexity of the permanent, which would separate VP from VNP-type classes, is still open. The smooth-form bound of Corollary 9.3 applies to any polynomial with a smooth initial form, not only the permanent.
The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. Formalizing it would certify the polar-degree counting argument and the coefficient-projection construction that extracts a smooth form of linear degree and quadratic dimension from the permanent.
The Hessian method stops at the quadratic scale: the Hessian of an order- determinant has rank at most at a singular matrix, while the permanent's Hessian has rank at most , so it cannot give more than . Singular-locus methods give only linear bounds for the permanent because its singular locus has small codimension. A cubic bound needs an invariant that grows multiplicatively in degree and dimension, and in the border model it must survive limits, so any intersection count used must be shown to persist for a single sufficiently close determinant.
MvPolynomial σ ℂ; the permanent is permanentPolynomial m on variables Fin m × Fin m.affineMatrixPolynomial n A₀ A is with complex matrices.HasExactDeterminant n p: and equals such a determinant. HasBorderDeterminant n p: and sequences whose determinant polynomials converge to coefficient by coefficient. Instead of defining as a minimum, the goal states that every admissible size obeys the bound, which is equivalent.affineSubstitution a I g is , homogeneousComponent extracts , and smoothness is stated on the affine cone: the only common zero of and all its partial derivatives is .Real.exp 1 for .A complete development needs projective smoothness and polar intersections (Bézout-type counts with simple points), adjugate and kernel-line computations for determinant pencils, and dimension estimates for matrix fibers. Contributions formalizing Lemma 2.1 (affine substitution preserves the closure), Proposition 2.2 (equivalence of border models) or Theorem 2.3 are welcome.
Multiplying two matrices by the schoolbook method costs about operations. The matrix-multiplication exponent of a field is the infimum of exponents such that matrices over can be multiplied with additions, subtractions and multiplications. It governs the asymptotic cost of a central bilinear operation and of the many algorithms built from it (determinants, inversion, linear systems). Bounding has driven algebraic complexity theory since 1969. In recent years the bounds have moved in the third and fourth decimal place, with each improvement coming from a finer analysis of the same tensor-power framework.
Fix a field . An arithmetic program is a straight-line sequence of gates, each a constant from , an input entry, or the sum, difference or product of two earlier gates. Its cost counts the addition, subtraction and multiplication gates. A program multiplies matrices if designated registers equal the entries of for every pair of input matrices over . A real number is admissible if for every there is such that for every some correct program has cost at most , and
In Lean this is MatrixAllFields.MatrixMultiplication.Arithmetic.omega F, defined for every F : Type u with [Field F].
The Lean statement also contains the numerical comparison , which carries no mathematical content (the source writes the comparison as ). This is Theorem 1.1 of the source. The goal is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. If the source's argument and certificate are correct, the theorem lowers the best stated bound on from (Dupont et al.) to , and it does so uniformly over all fields, with exact algorithms in every positive characteristic. Any improvement in lowers the exponent of every algorithm reducible to matrix multiplication. The method — pooling directional capacities across extraction depths and staggering lots so that one lot sits at each splitting stage — shows that combination losses in the asymmetric framework can be traded across depths.
Formalizing it. Bounds of this type rest on long chains of tensor-power constructions, recovery arguments and large rational parameter tables, checked in the source by an accompanying verifier with interval certificates for logarithms. A machine-checked proof would certify the whole chain from the arithmetic model to the final rational inequality. It would also give Mathlib the asymptotic sum inequality and Coppersmith–Winograd machinery, which every future bound on needs.
Every recent improvement fights extraction losses. Restricting a tensor power to a direct sum of independent matrix products wastes variables whenever whole blocks must be disjoint, while the final products only need disjoint subsets. Prescribed marginals may also allow several joint distributions. Earlier analyses take the minimum of three directional capacities separately at each depth, so a shortage on one side at one depth is lost. Using capacity across depths requires that variables deleted in earlier extractions (to resolve conflicts or impose type conditions) can still be recovered exactly, over the original field and with only subexponentially many extra copies. Positive characteristic rules out arguments that divide by small integers or rely on characteristic-zero identities.
F : Type u, with free constants from and unit cost for add, sub and mul. This matches the source's "scalar additions and multiplications".AdmissibleExponent F τ asks, for each , for one constant that works for every . omega F is the sInf of the admissible set, which is nonempty (schoolbook algorithm) and bounded below by the output size, so a junk value cannot make the strict inequality true.A graph is three-colorable if its vertices can be colored with three colors so that adjacent vertices get different colors. Deciding three-colorability is NP-complete. The approximate coloring problem asks how much a promise helps: given a graph promised to be three-colorable, can one efficiently find a coloring with a few more colors, or at least a large independent set? Every three-colorable graph on vertices has an independent set of size (its largest color class). The best polynomial-time algorithms use colors, while hardness results long reached only small palettes and needed extra conjectures for stronger gaps. Problems of this kind are central test cases for the PCP theorem, Label Cover and the theory of promise constraint satisfaction.
A 3-CNF formula is a conjunction of clauses, each a disjunction of at most three literals (variables or their negations); it is satisfiable if some truth assignment makes every clause true. For a finite simple undirected graph with vertices, is the size of a largest independent set, a set of pairwise nonadjacent vertices. A polynomial-time reduction is a deterministic algorithm that, on an explicit binary encoding of its input, runs in time polynomial in the encoding length and outputs an explicit encoding (here the full adjacency matrix) of the output graph.
For every fixed real there is a deterministic polynomial-time algorithm mapping each explicitly encoded 3-CNF formula to a nonempty finite simple graph with
The running time and output size are polynomial in the binary length of , with constants depending only on . The goal statement is published on the platform with status Open.
The result itself. Theorem 1.1 shows that, even with the full promise of three-colorability, it is NP-hard to find an independent set of any fixed positive density. It implies hardness of distinguishing -colorable graphs from non--colorable graphs for all fixed (Corollary 1.2), the long-standing conjecture recorded by Barto–Bulín–Krokhin–Opršal. Unlike the routes through -to- games and arc graphs, it keeps the independent-set soundness together with three-colorable completeness, and unlike Dinur–Khot–Perkins–Safra it does not delete vertices. Earlier results with this combination were conditional (Dinur–Mossel–Regev; Braverman–Khot–Lifshitz–Minzer).
Formalizing it. The statement is fully explicit: Mathlib's TM2ComputableInPolyTime fixes the machine model, and the formula and graph encodings are spelled out bit by bit. A formal proof would require a machine-checked PCP theorem with perfect completeness (Label Cover), a dimension-independent junta approximation theorem, and the paper's alignment and list-decoding lemmas. Any of these is a substantial and reusable formalization project; complexity-theoretic reductions are barely represented in Mathlib today.
Gap reductions from Label Cover to coloring traditionally use long-code or dictatorship tests whose soundness analysis loses control either of three-colorability of every vertex (completeness) or of independent sets of arbitrarily small density (soundness). Known unconditional routes reach constant-palette coloring hardness only by composing reductions that lose the independent-set guarantee, and routes keeping it required unproven games conjectures with structural assumptions. The proof must decode a labeling from any independent set of density in a graph that is genuinely three-colorable on every vertex when is satisfiable, without bounds on projection-fiber sizes.
Graph records: vertices Fin n, a symmetric loopless Boolean adjacency. Independence number is the maximum card of an independent Finset; three-colorability is a proper map to Fin 3.RealGraphReduction δ packages a function reduce : List Bool → Graph with a Turing.TM2ComputableInPolyTime witness (identity input encoding, graphBits output encoding, finite stack alphabets), an explicit polynomial output-size bound, completeness and strict soundness on encoded formulas. The reduction must be total and polynomial-time on all bit strings, which is harmless since malformed inputs can be sent to a fixed graph.