Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Iterated matrix multiplication asks for the entry of a product of matrices of size with independent variable entries,
It has polynomial-size arithmetic circuits when depth is unrestricted and is complete for algebraic branching programs, so it is the standard test case for the cost of restricting circuit depth. Depth-reduction theorems (Agrawal–Vinay, Koiran, Tavenas) show that any polynomial-size circuit for a degree- polynomial can be flattened to homogeneous depth four with size ; lower bounds of the form at small depth are therefore exactly at the threshold that depth reduction permits, and improving them slightly would separate general circuits from formulas. Nisan and Wigderson asked for an explicit homogeneous polynomial requiring superpolynomial size at constant depth, even at depth five.
These results either restrict the bottom linear forms, use a different width–degree regime, or concern a different polynomial. The source of this mission, an OpenAI preprint dated September 25, 2026, claims the sharp bound in the balanced regime with unrestricted bottom forms.
An arithmetic circuit over a field is a finite DAG whose leaves are variables or field elements; sum gates take -linear combinations of their inputs, product gates multiply their inputs (with multiplicity). A circuit has five layers of types from the output down, with a single output gate; edges join consecutive layers and bottom sums read leaves. Fan-in, fan-out and sharing are unrestricted, and bottom linear forms may involve any number of variables. The circuit is syntactically homogeneous if, with variables of degree , constants of degree and product degrees adding, every sum gate has all inputs of the same formal degree. Size is the number of vertices, leaves included. The target is , of degree in variables.
There is such that for all , every syntactically homogeneous circuit computing over , and more generally over any field of characteristic zero, has
Conversely, over every field and for every there is such a circuit with
The Lean statement OAI.Problem335.main bundles the three clauses and is open on the platform. The constant is the paper's and is not optimized.
The theorem determines the size of homogeneous depth-five circuits for up to the constant in the exponent: . It removes the bottom-support restriction of Bera–Chakrabarti and works at the balanced width–degree point , where the shifted-partials bounds of Amireddy et al. and the low-degree results of Limaye–Srinivasan–Tavenas do not apply directly. It answers the depth-five instance of the Nisan–Wigderson question for an explicit polynomial in VP. It does not give superpolynomial bounds for general circuits.
The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. The upper-bound clause is elementary and a natural first formal target; the lower bound requires a new rank measure and its estimates.
Depth-five circuits with unrestricted bottom linear forms can use linear forms involving all variables, which defeats measures that rely on bottom forms having small support (the Bera–Chakrabarti approach) or on set-multilinearization with degree-dependent losses (which are too costly when ). Partial-derivative and shifted-partial measures applied directly give bounds that degrade with the bottom fan-in. One needs a measure that is small for every product of homogeneous low-degree polynomials of arbitrary support and large for .
Depth5Circuit K n stores the leaves (D5Leaf: a scalar or a variable index in Fin n × Fin n × Fin n), bottom sums (lists of coefficient–leaf pairs), lower products (lists of bottom gates), middle sums, upper products, and one output sum, with explicit formal degrees and homogeneity constraints at every sum gate; empty sums have degree .circuitSize counts leaves plus all gates plus the output gate; circuitValue evaluates to an MvPolynomial.imm K n is the entry of the ordered product of the matrices .ℂ and, with a threshold chosen before the field, over every Field with CharZero; the upper bound over every Field, with the explicit upperGateBound.A complete development needs multivariate polynomial algebra, the derivative-multiplication operator and its rank, an integral (Bargmann–Fock type) moment estimate over , and a transfer to characteristic zero via integer minors. Contributions formalizing Proposition 6.2 (the upper bound) and Proposition 3.1 (the circuit-side rank bound) are welcome.
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 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.
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, 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.
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.A directed feedback vertex set of a finite digraph is a set of vertices meeting every directed cycle, equivalently one whose removal leaves acyclic; is the minimum size of such a set. The problem arises wherever cyclic dependencies must be broken — deadlock resolution, circuit testing, scheduling — and a topological order of certifies a solution in polynomial time.
The best general approximation guarantee is , originating in Seymour's work on fractional packing of directed circuits (Combinatorica 1995) and made constructive by Even, Naor, Schieber and Sudan (Algorithmica 1998). On the hardness side, NP-hardness was known only for particular constants (via Vertex Cover), while ruling out every constant factor required the Unique Games Conjecture. Whether a constant-factor approximation exists under P ≠ NP alone was open.
This mission asks for a machine-checked proof that approximating DFVS within any fixed factor is NP-hard on unweighted digraphs, as claimed in an OpenAI preprint dated September 23, 2026 (source, Theorem 1.1, p. 2). The preprint has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal is open.
A digraph is finite and loopless, given by a vertex count and a duplicate-free list of arcs with ; opposite arcs are allowed. A directed cycle is a cyclic sequence of distinct vertices with every successive arc present, including the closing one. is a feedback set if it meets every directed cycle, and is the least size of one.
A language is in NP if there are a polynomial and a deterministic polynomial-time verifier (a multi-stack Turing machine with finite alphabets) with iff some certificate with makes accept.
For every real and every language there is a deterministic polynomial-time map with such that
In Lean this is OAI.DirectedFeedback.main : DirectedFeedback.MainStatement. The preprint states Theorem 1.1 as a reduction from an NP-hard promise problem (the 2-to-1 game gap of Theorem 2.1, p. 5) to ; composing with that promise problem's NP-hardness gives the Lean form, which quantifies over all NP languages directly. A deterministic polynomial-time -approximation would then decide every NP language (proof of Theorem 1.1, p. 28).
The preprint also proves Corollary 8.3 (p. 28) for directed feedback arc set; it is not formalized on the platform.
The result itself. Theorem 1.1 shows that a constant-factor approximation for DFVS exists if and only if P = NP, removing the Unique Games hypothesis from the Guruswami–Manokaran–Raghavendra and Svensson results. It does not determine the true growth of the optimal factor between constants and .
Formalizing it. No machine-checked inapproximability result of this kind is known to exist. A complete development needs the 2-to-1 Games Theorem with imperfect completeness (Theorem 2.1, p. 5, external input), Friedgut's junta theorem in a dyadic fixed-bias form (Theorem 2.2 and Corollary 2.3, p. 6), finite Ramsey theory and von Neumann's minimax theorem, and the preprint's rank-graph construction (Definition 3.1, p. 8; Proposition 3.7, p. 12), pivotality budget (Definition 6.1, p. 20) and weighted soundness (Proposition 7.4, p. 25). An NP and Karp-reduction library on TM2 machines (including Cook–Levin) would be reusable across the whole family of hardness missions.
The central difficulty (Introduction, pp. 3–4) is extracting a game labeling from an arbitrary acyclic remainder: a topological order exists, but it can interleave the many vertices representing one local test arbitrarily. Comparisons in that order must first be made consistent and then read as Boolean functions; Friedgut-type junta bounds must hold at many biases simultaneously for the same random function, so a separate influence bound at each scale does not suffice. The coordinate lists must also be fixed before the tested game edge is drawn, or they do not define a game labeling. Gadget reductions from Vertex Cover cannot go beyond the Vertex Cover constants.
DirectedFeedback.Digraph: n : ℕ, a Nodup list of arcs in Fin n × Fin n, loopless; cycles are injective maps Fin (r+1) → Fin n with all successive arcs (including the wrap-around) present, so 2-cycles count and 1-cycles cannot occur. dfvs is the least cardinality of a feedback Finset.NPVerifier: a polynomial certificate bound and a polynomial-time TM2 verifier with finite alphabets on the unary-framed pair encoding pairBits; no SAT-specific definition is used.GapReduction A L is a polynomial-time TM2 machine (finite alphabets, raw-bit input) producing a GapInstance (digraph plus k > 0), encoded explicitly in unary-framed form by GapInstance.bits; completeness and soundness are as displayed, with soundness compared in ℝ.TM2 verifiers plus the 2-to-1 Games reduction.k > 0 and the strict inequality rule out a trivial reading (e.g. empty graphs with k = 0).Welcome contributions: Friedgut's junta theorem, finite Ramsey and minimax in usable forms, the 2-to-1 Games Theorem, and Cook–Levin for Turing.TM2ComputableInPolyTime.
Min-UnCut asks, for a finite simple graph , for the minimum number of edges whose deletion makes bipartite. Equivalently, for a bipartition let count the edges with both endpoints on the same side, and set . The quantity measures distance from bipartiteness. Although it equals minus the maximum cut, a good multiplicative approximation for Max-Cut gives nothing multiplicative for Min-UnCut on nearly bipartite graphs, which is exactly the regime of interest.
The best known algorithm (Agarwal, Charikar, Makarychev, Makarychev, STOC 2005) achieves an factor. Before the source preprint, NP-hardness was known only for specific constant factors below about , and hardness for every constant factor was known only under the Unique Games Conjecture.
This mission asks for a machine-checked proof that Min-UnCut has no polynomial-time approximation within any constant factor unless P = NP, as claimed in an OpenAI preprint dated September 23, 2026 (source, Theorem 1.1, p. 2). The preprint has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal is open.
A graph is finite, simple, undirected and unweighted, given by a vertex count and a symmetric loopless Boolean adjacency table. A cut is a map ; the parts may be empty or unbalanced. counts unordered edges with , and is its minimum over all cuts.
3SAT formulas are conjunctions of three-slot clauses over natural-number variable names (repeated variables allowed), given to the reduction by a canonical prefix-free binary encoding.
For every fixed integer there is a deterministic polynomial-time reduction to an explicit simple graph and a binary integer with
with graph size and running time polynomial in the bit length of for each fixed . Choosing shows that a deterministic polynomial-time -approximation for any real would imply P = NP. The positive threshold is what separates this from bipartiteness testing. In Lean this is OAI.MinUncut.main : Nonempty MinUncut.Reduction.
The preprint also derives Corollary 1.2 (p. 3): minimum 2CNF clause deletion is NP-hard to approximate within every fixed factor . It is not formalized on the platform.
The result itself. Theorem 1.1 settles the constant-factor approximability of Min-UnCut in the hardness direction without the Unique Games Conjecture, and by an exact cost-preserving transformation the same holds for Min 2CNF Deletion. Together with the algorithm, it places these problems strictly between constant-factor approximable and inapproximable within logarithmic factors (the remaining gap concerns super-constant factors).
Formalizing it. No machine-checked proof of super-constant-type inapproximability for any natural graph problem is known to exist. A complete development needs Håstad's parity gap (Theorem 2.2, p. 6) and uniform parallel repetition (Theorem 2.3, p. 7), used as external inputs, plus the preprint's inner decoding theorem (Theorem 3.2, p. 9), the composition gap for bit comparisons (Proposition 6.1, p. 27) and the finite constructions (Lemmas 7.1 and 7.2, pp. 31 and 34). PCP and parallel-repetition infrastructure would be reusable across many hardness missions.
A natural route is to compose a long-code test with a projection game, as in Håstad's work. The obstacle is extracting a label from an arbitrary folded bit proof with a probability and coefficient size independent of the label alphabet: the alphabet grows as the outer soundness is driven down, and every inner constant must be fixed before it (Introduction, pp. 3–4). In addition, the decoder's choices depend on shared background affine functions, so the outer game's soundness must survive such shared hints. Gadget-based approaches yield only isolated constants (up to about ); unbounded constants previously required the Unique Games hypothesis.
MinUncut.Output packages the graph (vertex count, symmetric loopless Bool adjacency) with a threshold threshold ≥ 1; uncut counts pairs u < v that are adjacent and on the same side, and opt is the minimum over all Fin N → Bool cuts (nonempty, so always defined).MinUncut.Reduction is a single TM2 machine taking the pair (encoded by inputBits) with finite tape alphabets, a polynomial time K bounding the running time in the formula's bit length, and a polynomial size K bounding vertices plus output length; yes/no hold for every K ≥ 2.formulaBits φ, the canonical encoding including variable names.Welcome contributions: Fourier and Gaussian analysis on -affine spaces, the long code with folding, parallel repetition for projection games, and Turing-machine complexity infrastructure.
Max-Cut asks for a partition of the vertices of a graph that maximizes the number of edges crossing it. Its decision version is one of Karp's original NP-complete problems, so the natural question is how well it can be approximated in polynomial time. Goemans and Williamson's semidefinite-programming algorithm with random-hyperplane rounding achieves ratio approaching
(GW 1995). Whether any polynomial-time algorithm can beat this constant is a central question of approximation algorithms: unconditional NP-hardness was known only above , and optimality of was known only under Khot's Unique Games Conjecture.
This mission asks for a machine-checked proof that approximating Max-Cut within any fixed ratio is NP-hard, even on simple unweighted graphs, as claimed in an OpenAI preprint dated September 23, 2026 (source, Theorem 1.1, p. 1). The preprint gives a direct reduction from the 2-to-1 Games Theorem, not via the Unique Games Conjecture. It has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal is open.
A simple unweighted graph on vertices is given by a symmetric, loopless Boolean adjacency table. A cut is a map from the vertices to ; its size is the number of unordered edges with , and is the largest cut size. An algorithm is an -approximation if it always returns a cut of size at least .
3SAT inputs are bit strings decoding canonically to a conjunction of three-slot clauses (repeated variables and literals allowed); malformed strings are NO instances. A gap reduction for consists of rationals and with , and a deterministic polynomial-time map outputting a graph together with a positive integer scale such that
Given such a reduction, an -approximation algorithm would decide 3SAT by comparing its output with .
For every real with , a gap reduction for from 3SAT to simple unweighted Max-Cut exists:
In Lean this is OAI.OptimalMaxCut.main : OptimalMaxCut.MainStatement. The preprint proves it from a sharper weighted gap (Theorem 1.2, p. 2): for rational , and , it is NP-hard to distinguish from on graphs with a rational edge distribution; Appendix B (p. 35) converts weighted graphs to simple unweighted ones.
The result itself. Theorem 1.1 shows that the Goemans–Williamson algorithm is optimal among polynomial-time algorithms unless P = NP, removing the Unique Games hypothesis from the result of Khot, Kindler, Mossel and O'Donnell. It is the most prominent instance of an SDP-tight threshold, and the gap form (Theorem 1.2) gives a whole curve of completeness/soundness pairs.
Formalizing it. No machine-checked proof of any optimal inapproximability result for Max-Cut exists. A full development requires the 2-to-1 Games Theorem in the affine form stated as Proposition 2.2 (p. 6) and derived in Appendix A, the Majority Is Stablest theorem (Lemma 2.1, p. 5), and the paper's new ingredients: tree-code Fourier analysis (Section 5), a vector-valued affine hashing lemma (Lemma 6.1, p. 14), dimension-independent extraction (Proposition 7.1, p. 18) and decoding (Proposition 8.4, p. 24). Several of these — Majority Is Stablest, Boolean Fourier analysis, polynomial-time gap reductions on Turing machines — are reusable libraries in their own right.
The classical long-code test for Max-Cut, analysed via Majority Is Stablest, identifies an influential coordinate of an arbitrary cut. Under the Unique Games Conjecture that coordinate is directly a label of the source game. Starting instead from 2-to-1 games, the influential coordinate is indexed by a gate input of the test, not by a source-game label, and the two endpoints of a source edge cannot in general reconstruct a common context without knowing their projection. The decoding loss must also be independent of the source alphabet, because the alphabet dimension is chosen after the target soundness; a dimension-dependent loss would make the parameter choice circular (Introduction, pp. 3–4).
OptimalMaxCut.Graph: a vertex count with a symmetric loopless Bool adjacency function; maxCut maximizes cutSize over all Fin n → Bool, counting each unordered crossing edge once.ScaledGraph with an explicit positive integer scale; the YES/NO bounds compare maxCut / scale in ℝ, and 0 < scale rules out division by zero.alphaGW is defined as the sInf of over ; this set is nonempty and bounded below, so the infimum is the true constant.Turing.TM2ComputableInPolyTime machine with finite tape alphabets, from raw input bits (identity encoding) to ScaledGraph.bits (delimited vertex count and scale, then the full adjacency table); the rational bounds and the machine are fixed before the input.noBound < α * yesBound with 0 < yesBound, so there is no trivial reading. No assumption P ≠ NP is built in.Welcome contributions: Boolean and Gaussian Fourier analysis (noise stability, influences, Borell's theorem), Majority Is Stablest, the 2-to-1 Games Theorem, and a reusable library for polynomial-time gap reductions on TM2 machines.
A Unique Game is a system of constraints between pairs of variables, each constraint saying that the label of one endpoint is a fixed permutation of the label of the other. Deciding whether all constraints can be satisfied is easy (propagate labels along a spanning tree), so the interesting question is approximate: given an instance in which almost all constraints can be satisfied, can a polynomial-time algorithm find a labeling that satisfies even a small fraction?
Khot's Unique Games Conjecture (UGC, 2002) asserts that it cannot, unless P = NP. The conjecture matters because many optimal approximation thresholds have been proved conditionally on it: the Goemans–Williamson ratio for Max-Cut (KKMO 2007), the factor for Vertex Cover (Khot–Regev 2008), the basic-SDP threshold for every constraint satisfaction problem (Raghavendra 2008), and hardness for ordering, multicut/sparsest-cut and correlation-clustering problems. An unconditional proof would turn all of these into NP-hardness results.
This mission asks for a machine-checked proof of the Unique Games Theorem as stated in an OpenAI preprint dated September 23, 2026 (source), which claims a positive resolution of the conjecture. The preprint has not been peer reviewed, and its claim has not been independently verified; on the platform the Lean goal below is open.
Fix a finite alphabet . An instance has a finite vertex set and a nonempty list of oriented constraints with a permutation of ; repeated list entries count with multiplicity, and no weights are allowed. A labeling assigns a label to every vertex and satisfies when . The value of is the fraction of satisfied constraints and is the maximum over labelings.
An instance is simple bipartite if its vertices split into two sides, every constraint goes from the first side to the second, and no two list entries join the same ordered pair. It is a translation instance over if every constraint has the form .
3SAT inputs are bit strings decoding to a conjunction of clauses with exactly three literal slots (repeated variables and literals allowed); the input is a YES instance when it decodes to a satisfiable formula.
For every there exist and a deterministic polynomial-time map to simple bipartite translation instances over such that
The alphabet, the program and the running-time polynomial depend only on ; the two errors are chosen independently, before the alphabet. In Lean this is OAI.UniqueGamesTheorem.theorem11, which asserts that the structure BinaryGapReduction ε δ is inhabited.
The result itself. The conjecture is the hypothesis behind a large body of tight approximation thresholds; the preprint's Section 8 (pp. 39–43) records how Theorem 1.1 feeds the earlier reductions for Max-Cut, Vertex Cover, Raghavendra's CSP theorem, ordering CSPs, multicut/sparsest cut and correlation clustering. Those reductions and thresholds are due to their original authors. The statement also fixes the conjecture's quantifier order (errors first, then alphabet), which is exactly what the known algorithms above do not contradict.
Formalizing it. No machine-checked proof of the UGC, or of the 2-to-2 theorem it builds on, is known to exist. A complete development would have to formalize Håstad's parity gap, classical parallel repetition for projection games, the Khot–Minzer–Safra Grassmann/shortcode inverse theorem (used as an external input via Theorem 5.1, p. 22 of the preprint), and the preprint's new latent-alphabet gadget and matrix test. Each of these is reusable well beyond this mission.
The central obstacle, identified in the preprint's introduction (pp. 2–4), is completeness: in a unique constraint every label permits exactly one reply, so the natural codeword tests lose a constant fraction of constraints even on honest proofs. For example, on the rank-one matrix shortcode the evaluation is preserved by a random rank-one update only with probability about . The 2-to-2 theorem gives soundness but only near- completeness, and pushing completeness to while keeping soundness independent of the alphabet is a separate problem that the earlier programme left open.
Foundations.Target.Instance q over alphabet Fin q, with constraints given by explicit forward/inverse permutation tables and a nonemptiness proof; the value is countSatisfied / constraints.length in ℝ, so division by zero cannot occur.Turing.TM2ComputableInPolyTime program from raw input bits (identity encoding, so runtime is measured in the raw input length including sparse variable names) to the bit encoding gameBits; its tape alphabets must be finite.coordinates : Fin alphabet ≃ (Fin s → ZMod 2) fixes the structure, and translations requires every constraint to be a translation in these coordinates; simpleBipartite gives the orientation and the no-parallel-edge condition on list positions.BinaryLanguage.language: inputs that decode (canonically) to a satisfiable three-slot formula. Malformed inputs are NO instances and must be mapped to low-value games.Welcome contributions: a reusable Lean library for PCP-style gap reductions on TM2 machines, Fourier analysis over , parallel repetition for projection games, and the Grassmann expansion theorem.
Edit distance , the least number of single-symbol insertions, deletions and substitutions turning into , is the standard distance on strings. Embedding strings into with small distortion would make edit distance amenable to the fast nearest-neighbour and sketching tools available for , so the least achievable distortion is a central quantity in metric embedding theory. A single insertion shifts every later symbol, yet cyclically shifting a word costs only two edits; this tension between position and alignment is what makes edit distance hard to embed.
This preprint gives two independent constructions of binary word sets whose least distortion is , two binary coding arguments that transfer large-alphabet constructions to binary, and a complete histogram embedding attaining the matching upper scale. Together they determine the exponential scale of the distortion.
For a finite alphabet with and an integer , let be the words of length at most , including the empty word. For an injective ,
The longest common subsequence and the deficit for words of length are used in the coding results. A binary substitution replaces each letter by a codeword.
In Lean (OAI.FiniteCircle), editDistance is the least script length, lcs and deficit are as above, optimalDistortion is the infimum of distortion over injective maps into lp (fun _ : ℕ => ℝ) 1, E α d is the least distortion of words of length at most , and maskWord, excludedWord are the two finite-circle constructions with prime-period parameters.
finiteCircle_fullMainThe conjunction of the paper's main statements, with common absolute constants:
and the same bounds for .
The result. The lower bounds reach the Ostrovsky–Rabani scale, so the order of is ; this improves the previous lower bound to . The histogram embedding gives an explicit, alphabet-uniform upper bound including all shorter words.
Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. Unlike the companion paper, the upper bound here is proved in full (Section 8) rather than imported, so the goal is self-contained relative to the preprint. The edit-distance and distortion definitions are reusable across the edit-distance missions.
Lower bounds for edit distance must control every increasing matching of the two words, including matchings crossing the row boundaries used to construct them. A cheap translation of phases moves row lists at low edit cost, while a simultaneous half-turn at every leaf must be expensive; proving the latter for arbitrary alignments, and then showing that every image must distort one of these comparisons, requires combining a combinatorial separation estimate with a Fourier argument on the finite phase space that forces large total frequency.
List α with Fintype α; the domain is a subtype by length; the empty word is included.distortion uses sSup over finite sets of ratios; optimalDistortion is sInf over injective maps into ; exponentScale d = sqrt(log d · log log d) with natural logarithms.MaskPrimes, ExcludedPrimes, depth parameters) and require a common positive length .UniformUpper asks for a map into Fin M → ℝ with the norm written as a finite sum.The goal is not vacuous: a set with one element would have least distortion , so witnesses must be nontrivial, and both bounds are required uniformly.
Needed infrastructure: LCS and alignment combinatorics, cut decompositions of finite metrics, Fourier analysis on finite cyclic groups, prime counting estimates, and random partition arguments for the upper bound. Contributions toward any component are welcome.
Edit distance is the least number of single-symbol insertions, deletions and substitutions transforming a string into . It is the basic similarity measure for strings, but it is expensive to compute and awkward to index. A standard way around this is to embed strings into so that distances approximate edit distances; the quality of such a map is its distortion. Low-distortion embeddings give fast approximate nearest-neighbour search and sketching for edit distance, so the best possible distortion has been studied for two decades.
This preprint determines the exponential scale of the optimal distortion: for strings of length at most , it is , uniformly over finite alphabets.
For a finite alphabet and , let be the set of strings of length at most , including the empty string. Edit scripts may pass through strings of any length. Let be the space of absolutely summable real sequences. Define
the infimum over injective maps with no restriction on dimension or computability.
In Lean (OAI.EditDistortion), edit x y is the least length of a Script true n x y of unit insertions, deletions and substitutions on List Alpha; L1 = lp (fun _ : ℕ => ℝ) 1; distortion ρ f is the product of the two maximal ratios for an embedding f : X ↪ L1; leastDistortion is the infimum over embeddings; E Alpha d applies this to {x : List Alpha // x.length ≤ d}; exponentScale c d = exp(c·sqrt(log d · log log d)).
There are absolute and such that for every and every finite alphabet with ,
The lower bound is witnessed by a finite set of binary strings of one common length at most , and the same two bounds hold for .
The result. Theorem 1.1 shows that the Ostrovsky–Rabani embedding is optimal up to the constant in the exponent, closing the gap between (Krauthgamer–Rabani) and . It rules out any embedding of edit distance with distortion , which limits -based approaches to approximate edit-distance search.
Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. The upper bound relies on Ostrovsky and Rabani's fixed-length theorem (Theorem 5.1 in the preprint, taken from the literature) plus reductions proved in the preprint, so a full formalization also requires formalizing the Ostrovsky–Rabani embedding. The lower bound (Sections 2–4) is the new contribution.
Any lower bound must control every alignment of two strings, including matchings that cross the boundaries of the blocks used to build them, because an insertion or deletion shifts an entire suffix. Earlier Fourier-analytic arguments (Khot–Naor) and recursive constructions (Krauthgamer–Rabani) lose too much to reach the exponent; reaching it requires a construction whose combinatorial separation and an displacement inequality match at that scale.
List Alpha with Fintype Alpha, 2 ≤ card Alpha; the domain includes the empty string and all lengths up to .edit is an sInf over script lengths, which is attained since scripts always exist.distortion uses sSup over finitely many ratios (the domain is finite), so no default values arise; leastDistortion is sInf over all injective maps into .BinaryWitness c d asks for a finite nonempty set of Boolean lists of common length whose least distortion is at least exponentScale c d; a singleton has least distortion , so the witness must be nontrivial.The statement cannot be met trivially: both bounds are required with constants uniform in the alphabet.
Needed infrastructure: cut decompositions of finite metrics, Fourier analysis on finite abelian groups, prime-number estimates (Rosser–Schoenfeld), and the Ostrovsky–Rabani construction. Contributions toward the displacement inequality (Proposition 2.2) or the recursive construction (Proposition 3.1) are welcome.
A metric space is doubling if every ball can be covered by a bounded number of balls of half the radius. Every subset of a finite-dimensional Euclidean space is doubling, so doubling is a necessary condition for a metric space to embed bi-Lipschitzly into some . Whether it is also sufficient, for subsets of Hilbert space, is the Lang–Plaut problem. It sits at the meeting point of metric geometry and algorithm design: doubling is a standard notion of "intrinsic dimension" for data, and a positive answer would mean that intrinsically low-dimensional Euclidean data can always be represented in a bounded number of coordinates with bounded distortion.
The Hilbert case () remained open. The source of this mission, an OpenAI preprint dated September 25, 2026, claims a negative answer.
A metric space is doubling with constant at most if for every and , the ball of radius about is covered by at most balls of radius with centers in . A map is a bi-Lipschitz embedding with distortion at most if some scale satisfies
Real is the Hilbert space of square-summable real sequences indexed by ; subsets carry the induced distance.
There is a universal such that every infinite-dimensional real Banach space contains a compact set with doubling constant at most that admits no bi-Lipschitz embedding into any finite-dimensional real normed space at any finite distortion.
The set is fixed once, independently of and of the distortion. The Lean statement OAI.DoublingHilbert.main is open on the platform. The constant comes from the paper's covering count; any finite universal constant would answer the Lang–Plaut problem, but the Lean goal records the paper's value.
The theorem answers the Lang–Plaut problem negatively: there is no function of the doubling constant alone that bounds both the dimension and the distortion for doubling subsets of Hilbert space. It extends the Lafforgue–Naor and Bartal–Gottlieb–Neiman obstructions from to the Hilbert case, which is the case of most interest for applications. By Gaussian isometric embedding the same metric space sits in every , (Corollary 5), and by Dvoretzky's theorem a compact version sits in every infinite-dimensional Banach space (Corollary 6). Assouad's theorem shows that any snowflake of the set does embed, so the obstruction is specific to the original distance.
The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. A previous announced proof of this statement (Schioppa, 2017) was withdrawn, which makes an independent formal verification particularly informative.
Doubling gives covering control at every scale, and Assouad's theorem shows that any loss in the exponent of the metric removes the obstruction, so a counterexample must be sharp at the level of exact Lipschitz bounds. The constructions rely on uniform convexity estimates of that degenerate at , and Hilbert space has the most symmetric geometry available, so the standard Laakso and diamond-type obstructions do not transfer. The set must also be chosen before the target dimension and distortion, so a single set has to defeat every and every simultaneously.
RealL2 := lp (fun _ : ℕ => ℝ) 2; is a Set RealL2 with the subspace metric.DoublingAtMost S bound: for each and there is a Finset of at most bound centers in such that every with satisfies for some center (open balls; centers in ).AdmitsBiLipschitzEmbedding S k: there are EuclideanSpace ℝ (Fin k), and with the two-sided bound above.CompactBanach.main quantifies over all complete real normed spaces that are not finite-dimensional and all finite-dimensional real normed targets, with the doubling constant chosen before .A complete development needs Hilbert direct sums, the explicit strip-colored set, covering estimates, a.e. differentiability of Lipschitz maps on open subsets of (Rademacher), and a Euclidean packing bound. Rademacher's theorem and packing estimates are reusable well beyond this mission. Contributions formalizing Proposition 2 (the doubling bound) are a natural first step.