Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A finite message chosen from data changes the conditional distribution of those data. In memory-constrained inference this matters directly: a learner observing a signal through exact Gaussian equations keeps a finite state , and after conditioning on the rows that were used to select it are biased. An independent Gaussian matrix has the same unconditional law as those rows, but once its labels are revealed it need not leave the same information about .
This preprint quantifies the cost of that replacement. For a uniform signal on the sphere and a message of entropy at most , replacing the actual rows by fresh independent rows increases the remaining conditional information by at most . As an application, learners with persistent bits need exact Gaussian observations to reach angular accuracy .
Let be uniform probability on , the law of a matrix with i.i.d. entries, discrete entropy and conditional mutual information, all in nats. Put
Let and be independent, and let be a countable message with an arbitrary joint law with .
In Lean (OAI.CurrentProjection), the joint law of is a probability measure P on (Sphere d × W) × Rows (d/10) d whose marginal is uniformSphere d ⊗ gaussianRows (d/10) d; alignedExperiment and P.fst.prod (gaussianRows ...) are the two experiments; exposedInformation is computed as a relative entropy via condKernel; shannonEntropy is .
There are an absolute and such that for and every such countable with ,
with an exact-density version when .
The result. Theorem 4.1 converts a statement about the actual, selection-biased rows into one about fresh rows at an additive cost of , which is the step that lets block-by-block information bounds be iterated along a stream. With the residual-sphere endpoint it gives the lower bound for learners with bits (Theorem 8.4, Corollary 8.7). The mixed projection moment (Theorem 3.1) is a reusable estimate on exact Gaussian projections of measures with local mass control.
Formalizing it. All results are in an unrefereed preprint, with no machine-checked proofs. The streaming theorems themselves (Theorem 8.4, Theorem 8.6, Corollary 8.7) are not among the published Lean targets and remain future work.
Conditioning on biases in a way that depends on the unknown signal, so the two experiments have different joint laws even though their and marginals agree. A direct comparison of densities fails because the exact label density under the actual law can be large on a selection-dependent set; controlling it requires a high moment of the projected density with the row-information charge entering only with coefficient .
Metric.sphere (0 : EuclideanSpace ℝ (Fin d)) 1 with normalized surface measure; rows are Fin k → EuclideanSpace ℝ (Fin d) with stdGaussian entries.ℝ≥0∞-valued.d/10, d/2 - d/10, d/32, d/8, d/4, d/3 as in each source statement.The goal is not vacuous: it quantifies over all joint laws with the stated marginal and entropy bound, and the right side is finite for many of them.
Needed infrastructure: conditional mutual information for standard Borel variables, chain rules, exact density versions of Gaussian projections, local mass bounds on the sphere. Contributions toward any milestone are welcome.
A linear projection can concentrate a measure even when the measure has no atoms; how much depends on how much mass sits near the affine subspaces that the projection collapses. Quantitative versions of this principle go back to the potential-theoretic projection method of Kaufman and Mattila, which relates ball-growth bounds to the behaviour of projections. This preprint proves explicit, dimension-dependent versions for random exact projections and applies them to a learning question: how many noiseless Gaussian measurements does a learner with bits of memory need to recover a unit vector to angular accuracy ?
The answer proved here is that bits force measurements, matching the real-valued randomized Kaczmarz scale, and more generally for every .
Let be uniform probability on . A finite measure on satisfies an all-ball mass bound with constants if for every ball. For an orthonormal -frame , is the image measure on and its density. The Riesz functional of is .
In the finite-state regression experiment, the signal ; at each step a row arrives with its exact label . A learner keeps one of states, may use arbitrary measurable randomized transitions of the current state and pair, stops by a deterministic horizon , and outputs a unit vector from its terminal state, stopping index and fresh randomness. Success means .
In Lean (OAI.ProjectionMoments, OAI.NoiselessRegression), learners are FiniteKernelLearner d M T (Markov-kernel transitions on completed observations, states Fin (2^M)), mixed over a seed space Ξ with probability ρ; seededSuccess is uniform-prior success; AllBallMass ν K β, coordinateDensity, frameLaw, capMeasure, rieszPotential encode the geometric objects.
OAI.ProjectionMoments.mainA conjunction of the paper's results, including:
also under an every-signal guarantee.
The result. The projection moment estimates are general statements about finite measures with ball-growth control and apply beyond learning. In the learning application they give three proofs, with different stopping and accuracy costs, that bits cannot beat the sample scale for exact Gaussian measurements, plus an explicit trade-off for all .
Formalizing it. The results are in an unrefereed preprint; there is no machine-checked proof. The conjunct FixedQuadraticMemory coincides with part of the goal of the companion mission on Memory and precision in noiseless Gaussian regression, so progress here is shared.
Integrated density norms do not determine density values on a matrix-dependent graph, so pointwise statements need an explicitly chosen density version. The high moments of projected densities require controlling collisions of independent points under projection, which leads to inverse affine heights whose integrability must be extracted from the ball-growth hypothesis at all scales. In the learning application, conditioning on an exact label produces a singular posterior, so arguments that track a posterior density fail.
EuclideanSpace ℝ (Fin d); frames are orthonormal families Fin k → E drawn by frameLaw; densities are ℝ≥0∞-valued with explicit measurable versions.d/4, d/8, d/16); block counts appear as (T+k-1)/k.FiniteKernelLearner with CompletedRules almost surely in the seed; success probabilities are ℝ≥0∞.The goal has no trivial reading: each conjunct quantifies over all measures or learners satisfying the stated hypotheses, and the hypotheses are satisfiable.
Needed infrastructure: Stiefel and Haar measures, Gaussian polar decomposition of matrices, Gram–Schmidt Jacobians, spherical caps, Riesz potentials. Contributions proving individual conjuncts (for example Theorem 3.3) are welcome.
An exact linear observation of a real signal can carry arbitrarily many bits. A finite message computed from a block of such observations cannot, but its information content is not controlled by the number of observations alone: if earlier messages have already concentrated the signal in a small region, the next block can exploit that concentration. Bounds of this kind are the engine of memory–sample lower bounds for noiseless Gaussian regression, where a learner with bits of memory must recover a unit vector to angular accuracy from a stream of exact Gaussian measurements.
This preprint asks how to restore a geometric spread condition on the posterior while paying for the information revealed in doing so, and proves that, for a cube-shaped prior on a spherical patch, blocks of exact measurements with messages of at most values reveal only nats.
Let be large, , , . The cube prior is normalized Lebesgue measure on the half-open cube , and the chart maps it into . Dyadic cells of level subdivide into half-open subcubes of side .
Draw . In block an independent standard Gaussian matrix is drawn, and is observed exactly. A message is drawn from a Borel probability kernel of the block data, whose choice may depend on the preceding messages . Information is measured in nats by mutual information , defined as a relative entropy.
In Lean (OAI.RepeatedLocalization), Coordinate n = Fin n → ℝ, cubePrior n is Lebesgue measure conditioned on initialCube n, chart is , a Cell n is a level with a multi-index in Fin (2^J), a BlockRule n N is a measurable probability vector on Fin N indexed by block data, Rules n N t chooses a rule for each block from the past history, and experimentLaw rules is the joint law of .
repeated_localizationThere is an absolute such that for every there is with the following property, for large. If
then one can reveal nested dyadic cells containing , with a finite-valued measurable function of and , such that the augmented transcript satisfies
where is the level of . An alphabet of size satisfies the hypothesis with depending only on .
The result. Theorem 3.2 is the first information estimate in the paper and the model for its later routes: it shows that revealing a nested dyadic cell after each block, which restores the spread condition needed by the projection estimate, costs only nats per block. Since the original message history is a function of , the bound also controls the information in the messages alone. Combined with the paper's endpoint arguments this yields the lower bound for learners with bits.
Formalizing it. These results are proved only in an unrefereed preprint; no machine-checked proofs exist. The milestones are independent analytic statements (an entropy regularization, a convex potential and its drift, an inverse-volume moment) that are reusable in the companion missions on exact Gaussian observations.
The information a block reveals depends on how concentrated the current posterior is, and earlier messages can make it arbitrarily concentrated. Simply conditioning on messages gives no control. Revealing a localizing cell restores spread, but naming a cell itself costs information, and the count of candidate cells at depth grows like ; the argument must show that confinement to a depth- cell (worth bits relative to the prior) pays for this, uniformly over all message rules.
Fin n → ℝ, and appears as n + 1.n / 16, n / 8. Gaussian entries are gaussianReal 0 1.Q : Disclosure n N t is valid when each cell map is measurable with finite range, contains , lies in , and the cells are nested. The goal asserts existence of a valid disclosure with mutualInformation (augmentedLaw rules Q) ≤ C (n+1) t and expected final level at most .klDiv of the joint law against the product of marginals, valued in ℝ≥0∞.The goal is not trivial: the trivial disclosure (always ) does not bound the information in arbitrary messages, and the quantifier order (absolute , then , then ) matches the source.
Needed infrastructure: Gaussian projections of measures on cells, density bounds, dyadic cell combinatorics, and relative-entropy chain rules. Contributions toward any milestone are welcome.
Suppose an unknown unit vector is observed through exact linear measurements with independent Gaussian rows . If every pair is kept, rows determine . A learner that can keep only a bounded number of bits between measurements must compress each exact real label into a state update, and the question is how many measurements this costs for a prescribed angular accuracy . Exact labels make the question delicate: a real label has no built-in bit precision, so noise-based arguments do not apply.
This preprint attacks the question through a conditional information bound for a single block of observations: how much information about can a finite message formed from exact Gaussian measurements carry, beyond what an independent Gaussian projection of (revealed only to the analyst) already reveals? Iterating such a block bound over a stream gives a memory–sample lower bound.
Let be uniform probability on . In a block experiment the signal has law with a Borel density . Independently draw a standard Gaussian matrix and observe . A message with values in a finite set is drawn from a measurable Markov kernel of . Finally an standard Gaussian matrix is drawn independently of everything. The quantity of interest is the conditional mutual information
in nats, and denotes the Shannon entropy of the message.
A finite-state learner with bits reads pairs once, in order, keeps a state in a set of size , may stop at any index up to a deterministic horizon , and outputs a unit vector from its terminal state, stopping index and fresh randomness only. Transitions and stopping may be arbitrary measurable randomized rules of the current state and current pair; shared randomness is independent of the signal and samples.
In Lean (OAI.PosteriorReplicas), sphereLaw d is normalized surface measure, gaussianRows d k is the product of stdGaussian, signalMessageLaw p κ is the law of , sideLaw ℓ appends , conditionalInformation is the relative entropy of the joint law from the conditionally independent coupling, and messageEntropy is . Learners are CompletedKernelLearner d M with Markov-kernel transitions on the completed observation space, wrapped in a JointKernelExperiment over a seed space .
OAI.PosteriorReplicas.source_mainThe goal is the conjunction of the paper's principal statements:
uniformly over the prior, , and the message kernel.
The result. Theorem 1.2 shows that with persistent bits, the sample scale of real-valued Kaczmarz-type methods cannot be improved for exact Gaussian measurements, under the uniform prior and with an absolute constant. Theorem 1.1 is a reusable statement in its own right: the entropy of a message is divided by a factor proportional to , and the dependence on the prior density bound is only doubly logarithmic, which is what allows conditioning on rare learner states.
Formalizing it. These results appear only in an unrefereed preprint, and none has a machine-checked proof. The companion preprint Memory and precision in noiseless Gaussian regression proves a related statement for memory by a different method; the two missions share the learner model but not the block estimates. Formalizing the goal requires conditional mutual information for general (non-discrete) random variables and the exact equal-label geometry, both of which would be reusable.
Conditioning on one exact observation confines the signal to a lower-dimensional section of the sphere, so posterior densities with respect to do not exist and density-based arguments fail. Bounding the information in the message by alone is far too weak: a message of bits could then carry all relevant information. The block bound must instead account for what the analyst's independent projection already reveals, uniformly over priors with large density bounds , since rare learner states produce such priors.
EuclideanSpace ℝ (Fin d); priors are measures on the ambient space given as (sphereLaw d).withDensity f with .Fin N with NeZero N; information quantities are ℝ≥0∞-valued relative entropies (klDiv), entropies use natural logarithms.2 * (d / 16), d / 8, d / 2 as in the paper.IsLittleO atTop M (d^2), all horizons , all , all seed spaces and all JointKernelExperiments whose output kernel agrees almost surely with the run of the per-seed learner.The goal cannot be met vacuously: block bounds are stated for every finite message kernel, and the streaming hypothesis (success at least ) is satisfiable by learners with large .
A complete development needs Gaussian matrices and their projections, coarea-type identities for equal labels, conditional kernels (condKernel), relative entropy chain rules, and spherical measure estimates. Contributions that isolate one conjunct (for example Theorem 3.3 or Theorem 1.1) are welcome.
A single exact linear equation about an unknown unit vector carries arbitrarily fine information: independent Gaussian equations determine almost surely, provided all of them can be kept. A learner that reads the equations once, in order, and keeps only a bounded number of bits between them faces a different problem. The question asked here is how many noiseless measurements such a learner needs in order to reach a prescribed angular precision , as a function of its memory.
This is a question about memory–sample trade-offs: how much a bound on persistent memory forces a learning procedure to read more data. With unbounded real registers, the randomized Kaczmarz update satisfies on isotropic Gaussian rows, so order samples suffice. That update stores real numbers and gives no finite-bit upper bound; the question is whether a learner with roughly bits can do better than this scale.
Fix integers , , . A signal lies on the unit sphere . At step the learner receives the pair with independent and exactly (no noise).
A finite-state learner with bits keeps a state in a set of at most elements. A data-independent shared seed (drawn from a probability space ) may select its rules. Given the seed, the current state, the step index and the current pair, a transition chooses the next state and whether to stop; it may perform unrestricted computation but retains only the next state. The learner must stop by the deterministic horizon . Its output is a function of the terminal state, the stopping index and the seed only; a discarded observation cannot be read again. Success at precision means angular error .
Write for the uniform probability measure on . Uniform success is the probability of success when is drawn independently of the rows and the seed.
In Lean (OAI.NoiselessRegression), the state space is Fin (2 ^ M), a learner is a structure Learner d M T Ω with fields initialChoice, transition, output, the sample law is the product of stdGaussian on EuclideanSpace ℝ (Fin d), and uniformSuccess and success are the probabilities defined above. Randomness during the run is represented through the arbitrary seed space .
OAI.NoiselessRegression.mainThe goal is the conjunction of two statements.
Fixed quadratic memory (Theorem 1.2): for every there are and such that, for , , , and every admissible learner,
Subquadratic memory (Corollaries 1.3 and 1.4): there is an absolute such that for every memory sequence there is with the same conclusion for , under either uniform success at least or success at least for every fixed signal .
No relation between and is assumed; the constant is absolute in the subquadratic case.
OAI.MemoryPrecision.main)A single bundled statement collecting the paper's projection-density and backward-block estimates (Theorem 3.1, Propositions A.1, A.4, A.5, B.6, B.7, Corollary 8.2), the cube-prior precision bound (Proposition 8.3), and the explicit success bound after a bounded number of samples (Proposition 5.3):
The result. Theorem 1.2 answers, for exact observations and isotropic Gaussian rows, the precision question raised in Section 1.1 of Sharan–Sidford–Valiant: with bits, the scale achieved by real-valued Kaczmarz cannot be improved, uniformly over all . Because an exact-observation learner can simulate added noise, the preprint derives from it an lower bound in the noisy experiment of Sharan–Sidford–Valiant at accuracy , which strengthens their bound in that range.
Formalizing it. The result is proved only in an unrefereed preprint; no machine-checked proof exists. A formal proof would certify a lower bound whose model (randomized measurable rules, early stopping, shared seeds, measurability conventions) is delicate, and the conventions are already fixed in the Lean definitions. Remaining work: the full formal proof, and as a variant the every-signal version of Theorem 1.2 for fixed (Corollary 1.4), which the Lean goal states only in the subquadratic case.
Conditioning the uniform prior on one exact observation confines the signal to a hyperplane section of the sphere, a law singular with respect to the original spherical measure; information-theoretic arguments that track a posterior density therefore break down after a single step. Arguments for noisy observations, such as Sharan–Sidford–Valiant's, rely on the noise to keep posteriors spread out and do not transfer to the more informative exact experiment. The bound must also hold uniformly in with no relation between and , so a learner with bits must be prevented from storing bits per coordinate for very small .
EuclideanSpace ℝ (Fin d); signals and outputs in Metric.sphere 0 1. The uniform sphere law is the normalized toSphere measure; rows are i.i.d. stdGaussian.Fin (2 ^ M); the first component of each action is the stop flag. Runs that never stop are forced to terminate at index .Learner.Admissible requires a.e.-measurability of the initial choice, transitions (against Gaussian × Lebesgue on pairs), outputs, and of the full experiment under each fixed signal and under the uniform prior.ℝ≥0∞-valued; the threshold is ; angular error is Real.arccos ⟪ŝ, s⟫; is natural.u, so randomized learners are covered by placing their randomness in the seed.The goal cannot be satisfied trivially: the hypotheses range over all admissible learners, and the success threshold is achievable (with large ), so the implication has content.
A complete development needs Gaussian measures on Euclidean space, spherical measure and cap estimates, Gram determinants and affine distances, densities of Gaussian projections, and measurable selection of Borel versions of kernels. The projection-density estimates are reusable beyond this mission. Contributions toward the bundled milestone, or toward any of its component estimates, are welcome.
Iterated matrix multiplication asks for the entry of a product of matrices of size with independent variable entries,
It has polynomial-size arithmetic circuits when depth is unrestricted and is complete for algebraic branching programs, so it is the standard test case for the cost of restricting circuit depth. Depth-reduction theorems (Agrawal–Vinay, Koiran, Tavenas) show that any polynomial-size circuit for a degree- polynomial can be flattened to homogeneous depth four with size ; lower bounds of the form at small depth are therefore exactly at the threshold that depth reduction permits, and improving them slightly would separate general circuits from formulas. Nisan and Wigderson asked for an explicit homogeneous polynomial requiring superpolynomial size at constant depth, even at depth five.
These results either restrict the bottom linear forms, use a different width–degree regime, or concern a different polynomial. The source of this mission, an OpenAI preprint dated September 25, 2026, claims the sharp bound in the balanced regime with unrestricted bottom forms.
An arithmetic circuit over a field is a finite DAG whose leaves are variables or field elements; sum gates take -linear combinations of their inputs, product gates multiply their inputs (with multiplicity). A circuit has five layers of types from the output down, with a single output gate; edges join consecutive layers and bottom sums read leaves. Fan-in, fan-out and sharing are unrestricted, and bottom linear forms may involve any number of variables. The circuit is syntactically homogeneous if, with variables of degree , constants of degree and product degrees adding, every sum gate has all inputs of the same formal degree. Size is the number of vertices, leaves included. The target is , of degree in variables.
There is such that for all , every syntactically homogeneous circuit computing over , and more generally over any field of characteristic zero, has
Conversely, over every field and for every there is such a circuit with
The Lean statement OAI.Problem335.main bundles the three clauses and is open on the platform. The constant is the paper's and is not optimized.
The theorem determines the size of homogeneous depth-five circuits for up to the constant in the exponent: . It removes the bottom-support restriction of Bera–Chakrabarti and works at the balanced width–degree point , where the shifted-partials bounds of Amireddy et al. and the low-degree results of Limaye–Srinivasan–Tavenas do not apply directly. It answers the depth-five instance of the Nisan–Wigderson question for an explicit polynomial in VP. It does not give superpolynomial bounds for general circuits.
The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. The upper-bound clause is elementary and a natural first formal target; the lower bound requires a new rank measure and its estimates.
Depth-five circuits with unrestricted bottom linear forms can use linear forms involving all variables, which defeats measures that rely on bottom forms having small support (the Bera–Chakrabarti approach) or on set-multilinearization with degree-dependent losses (which are too costly when ). Partial-derivative and shifted-partial measures applied directly give bounds that degrade with the bottom fan-in. One needs a measure that is small for every product of homogeneous low-degree polynomials of arbitrary support and large for .
Depth5Circuit K n stores the leaves (D5Leaf: a scalar or a variable index in Fin n × Fin n × Fin n), bottom sums (lists of coefficient–leaf pairs), lower products (lists of bottom gates), middle sums, upper products, and one output sum, with explicit formal degrees and homogeneity constraints at every sum gate; empty sums have degree .circuitSize counts leaves plus all gates plus the output gate; circuitValue evaluates to an MvPolynomial.imm K n is the entry of the ordered product of the matrices .ℂ and, with a threshold chosen before the field, over every Field with CharZero; the upper bound over every Field, with the explicit upperGateBound.A complete development needs multivariate polynomial algebra, the derivative-multiplication operator and its rank, an integral (Bargmann–Fock type) moment estimate over , and a transfer to characteristic zero via integer minors. Contributions formalizing Proposition 6.2 (the upper bound) and Proposition 3.1 (the circuit-side rank bound) are welcome.
A regular expression describes a set of words using letters, union, concatenation and the Kleene star (any finite repetition of words from ). The star height of an expression is the depth of nesting of its stars, and it measures how many layers of unbounded repetition a regular language genuinely needs. For ordinary expressions this hierarchy is infinite. Allowing complement as an additional operation changes the picture: Boolean conditions can replace some layers of repetition, and the generalized star-height problem asks how far this goes. Whether every regular language has generalized star height at most some fixed number — and in particular whether one star always suffices — has been one of the longest-standing questions in the algebraic theory of automata.
Fix a finite alphabet and let be the set of finite words. A generalized regular expression over is built from the constants (denoting ) and (denoting ), single letters , union , concatenation , complement (taken in ), and star . Its height is defined by
For a regular language , the generalized star height is the least height of an expression over denoting .
In Lean (namespace OAI.GeneralizedStarHeight), expressions are an inductive type Expression Alphabet with exactly these seven constructors, Expression.language interprets them in Mathlib's Language Alphabet (complement is Language complement, i.e. relative to all words), Expression.height is the recursion above, and HasHeightAtMost L n means some expression has language and height at most .
For every finite alphabet and every regular language ,
The goal is published on the platform with status Open.
The result itself. Before 2026 it was not known whether generalized star height is bounded at all; all positive results covered restricted families of monoids or languages. Theorem 1.1 gives a uniform bound independent of the alphabet and of the recognizing automaton, settling the boundedness question. It leaves open the sharper question of whether height one always suffices: no language is known to require height two. A uniform bound also implies that the hierarchy of generalized heights has at most four nonempty levels, which narrows where any separating example must be sought.
Formalizing it. The statement is short and fully elementary, but the proof composes many constructions (finite-monoid recognition, prefix codes of episodes, split identities, marker scales) whose height accounting is error-prone. A formal proof would certify the boundedness theorem itself. Mathlib already has regular languages (Language.IsRegular) and ordinary regular expressions; this mission adds generalized expressions with complement and their height.
The classical lower bounds for ordinary star height do not transfer once complement is allowed, and complement can simulate many but not obviously all counting arguments. The natural approach — write each fiber of a morphism from to a finite monoid by an expression that simulates the monoid computation letter by letter — needs one star per level of the computation's dependence on earlier history, and the depth of this dependence grows with the monoid. Group components are the difficulty: aperiodic monoids give height zero, but counting modulo and nonabelian group computations require stars, and a uniform bound must handle arbitrary finite groups nested inside arbitrary monoids without the number of stars growing with their size.
Type u with [Finite Alphabet]; regularity is Mathlib's Language.IsRegular (acceptance by a finite-state DFA).height charges only for stars; complement, union and concatenation are free, exactly as in the source. Since HasHeightAtMost asks only for existence of an expression, no bound on expression size or computability is claimed, matching the source's remark that the construction bounds nesting only.Weisfeiler–Leman (WL) refinement compares two graphs by repeatedly refining colors of ordered vertex -tuples. For every fixed dimension this is a polynomial-time procedure, with running time . When is part of the input, that computation is no longer polynomial, and the complexity of deciding the outcome becomes a question in its own right. Seppelt (2024) proved coNP-hardness and recorded Berkholz's question whether the problem is EXPTIME-complete.
This preprint answers that question for the joint-update convention: deciding -WL equivalence of two explicit graphs with in binary is EXPTIME-complete, even on connected graphs of maximum degree three.
Graphs are finite, simple, undirected and uncolored, given by adjacency matrices. In the joint-update convention a -tuple's initial color records equalities and adjacencies among its entries; each round adjoins to the old color the multiset, over replacement vertices , of the vector of old colors obtained by replacing each coordinate in turn by . Color names are common to both graphs, and means their -tuple color histograms agree at every round.
The language consists of encodings with in binary and . The language additionally requires and to be connected, of the same positive order, and of maximum degree at most three. Malformed encodings are excluded.
In Lean (OAI.VariableWL), Graph is a SimpleGraph on Fin order, color and histogram implement the joint update by recursion on rounds, pairCode concatenates the two graph codes (order header plus row-major matrix) and the code of , and complexity classes are defined from an explicit deterministic Turing machine model with OutputsWithin, InEXPTIME, PolytimeReduces and EXPTIMEComplete.
Both and are EXPTIME-complete under deterministic polynomial-time many-one reductions:
The result. Theorem 1.1 resolves the question recorded by Seppelt and strengthens the known coNP-hardness to EXPTIME-completeness. The subcubic case is notable because isomorphism of bounded-degree graphs is polynomial-time (Luks), yet equivalence under refinement at a supplied dimension remains EXPTIME-complete for degree three; nonisomorphic graphs can be equivalent. Corollary 8.3 shows hardness persists with in unary.
Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. The uniform computation interface developed here is reused by the companion identification paper, so a formalization would serve both missions.
Membership requires showing that the dimension can be capped before allocating tuple tables (Lemma 2.2), since may exceed the graph order. Hardness requires simulating an arbitrary exponential-time computation by a graph pair whose WL equivalence at a polynomially encoded dimension reflects acceptance. Because the number of address coordinates grows with the input, fixed-dimension constructions with dimension-dependent constants do not give a uniform polynomial-time reduction, and in the subcubic case colors must be realized by uncolored degree-three gadgets that a winning strategy still recognizes.
SimpleGraph (Fin order); Subcubic bounds every vertex degree by three; SubWL also demands positive equal orders and connectivity.Multiset types.The statement is not trivial: both membership and hardness are required for both languages.
Needed infrastructure: the bijective game characterization (Lemma 2.4), product-circuit compilation (Proposition 3.2), the general and subcubic realizations (Propositions 5.1 and 7.1) and the uniform compiler (Proposition 8.2). Contributions toward any of these are welcome.
The Weisfeiler–Leman (WL) method colors -tuples of vertices by repeatedly recording their local extension patterns; two graphs are -WL equivalent when the stable color histograms agree. For each fixed the direct algorithm runs in time : there are tuples and polynomially many refinement rounds. The question is whether the growing exponent is necessary for any algorithm deciding the equivalence relation, not just for implementations of refinement.
This preprint proves that it is, unconditionally: for every sufficiently large fixed , every deterministic sequential decider for -WL equivalence needs time at every sufficiently large graph order, without assuming the Exponential Time Hypothesis.
Graphs are finite, simple, undirected and uncolored, given as adjacency matrices. For a -tuple, the initial color records coordinate equalities and adjacencies. Each refinement step keeps the old color and adds, in the joint convention, the multiset over vertices of the -vectors of colors obtained by replacing each coordinate by ; in the separate convention, one such multiset per coordinate. Two -vertex graphs are -WL equivalent if their color histograms agree at every round.
A decider for a convention and dimension is a deterministic machine that halts on every encoded pair of -vertex graphs and accepts exactly the equivalent pairs. Its worst-case time is the maximum running time over pairs of -vertex graphs (optionally restricted to connected graphs of diameter at most two).
In Lean (OAI.WLTime), Graph n is a symmetric loopless Boolean matrix on Fin n, tupleColor and histogram define both conventions by recursion on rounds, Equivalent compares all rounds, encodePair encodes and both matrices, and machines are either multitape Turing machines (TM) or logarithmic-word RAMs (RAM) whose word operations are themselves implemented by Turing machines in time polynomial in the word length.
There are absolute constants and such that for every fixed , either convention, either input class (all graphs, or connected graphs of diameter at most two) and every correct deterministic decider in either machine model, there is with
The exponent constant is independent of and of the program; the threshold may depend on both. The bound holds at every large order, not only infinitely often.
The result. Theorem 1.1 rules out any running time with , unconditionally. Earlier lower bounds either concerned the number of refinement rounds, assumed ETH, or treated the dimension as part of the input (coNP- and EXPTIME-hardness), which does not give a fixed-dimension exponent. It covers both standard update conventions and the restricted class of diameter-two graphs.
Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. The Lean statement fixes explicit machine models, so a proof would include a verified padded diagonalization (Theorem 5.2), a verified computation-to-graph reduction (Theorem 4.3) and a verified compressed consistency construction (Theorem 3.2).
Unconditional time lower bounds in concrete models are rare; the only general technique is diagonalization, which yields hard languages but not hard natural problems. The proof must therefore transfer a diagonal language to WL equivalence through a reduction that is efficient enough to preserve an exponent linear in . A polynomial-time computation with exponent proportional to has too many addressed locations to list in a small reduction, and local consistency is symmetric whereas a computation must propagate information forward without forcing false predecessors to become true.
Decides A c k p requires halting and correctness on every pair in the input class at every order ; worstTime is a Finset.sup over pairs in the class.ℝ.The statement is not vacuous: correct deciders exist (direct refinement), so the conclusion constrains real algorithms.
Needed infrastructure: bijective pebble games and their equivalence with refinement (Lemma 2.3), Turing machine simulation and clocking, and the graph constructions of Sections 3–4. Contributions toward any of these components are welcome.
The Weisfeiler–Leman (WL) algorithm refines colors of vertex tuples to test graph isomorphism, and its dimension controls how much tuple information is used. A graph's Weisfeiler–Leman dimension is the least for which -WL refinement identifies , i.e. distinguishes it from every non-isomorphic graph. This is a standard measure of the descriptive complexity of an individual graph, tied to counting logics and pebble games. The question here is how hard it is to compute: given and , decide whether .
Identification differs from testing whether a given pair of graphs is equivalent: it quantifies over every possible comparison graph. The preprint shows the problem is EXPTIME-complete when is part of the input.
All graphs are finite, simple, undirected and uncolored. For the joint-update convention is used: a -tuple starts with its equality and adjacency type, and each round adjoins the multiset over vertices of the vector of colors obtained by replacing each coordinate by . For ordinary color refinement is used. Colors are shared between graphs. means the tuple-color histograms agree at every round. -WL identifies if implies for every graph , and is the least positive such .
The decision problem takes a nonempty graph by its adjacency matrix and a positive integer in binary, and asks whether ; malformed inputs are rejected.
In Lean (OAI.WLIdentification), Graph is an order with a symmetric loopless Boolean adjacency on Fin order; Equivalent, Identifies and WLdim follow the definitions above; inputs are bit words consisting of a unary order header, the row-major matrix and the binary dimension; complexity classes are defined from an explicit deterministic single-tape Turing machine model (Machine, run, DecidesWithin, InEXPTIME, PolytimeManyOne, EXPTIMEComplete).
The language
is EXPTIME-complete under deterministic polynomial-time many-one reductions: it is decidable in time , and every EXPTIME language reduces to it in polynomial time.
The result. Theorem 1.1 settles the complexity of the input-dimension identification problem, strengthening the NP-hardness of Lichter, Raßmann and Schweitzer to EXPTIME-completeness. By Corollary 7.3 hardness persists with in unary, so it does not come from exponentially large numerical dimensions.
Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. A formal proof would include a verified reduction from arbitrary exponential-time Turing machine computations to graphs, and a verified upper bound for WL identification. The Turing-machine model and the WL definitions in the Lean statement are reusable for the companion missions on WL equivalence.
Hardness must handle the all-mates quantifier: an encoding of a computation into a graph must ensure that every graph that is -WL equivalent to it is isomorphic to it exactly when the computation accepts. Local recognition of gadgets, as in earlier NP-hardness proofs, shows each incidence piece of has an allowed pattern, but the encoding here admits a whole family of shifted constraints, and one must show every shift arising from an equivalent mate lifts to a single global isomorphism on accepting instances. Membership in EXPTIME is also not immediate, since identification quantifies over infinitely many comparison graphs.
Fin n-indexed Boolean adjacency matrices; the problem language requires a nonempty graph, a binary word with leading bit true, and a positive value.WLdim G is sInf of the positive identifying dimensions; this set is nonempty for finite graphs (dimension equal to the order identifies), so the infimum is not the default value.The goal is not trivial: membership in EXPTIME and hardness under the explicit machine model are both required.
Needed infrastructure: WL refinement monotonicity, pebble games or an equivalent characterization, CFI-type gadget constructions, and Turing-machine simulation. Contributions toward the upper bound (Proposition 7.1) or the reconstruction results of Sections 3–5 are welcome.
The Weisfeiler–Leman (WL) method is the standard combinatorial heuristic for graph isomorphism: it repeatedly refines colors of -tuples of vertices, and two graphs it cannot tell apart are called -WL equivalent. It is equivalent to counting-logic indistinguishability and, by results of Dvořák (2010) and Dell, Grohe and Rattan (2018), to equality of homomorphism counts from graphs of treewidth below (bags of size at most ). For fixed , direct refinement decides -WL equivalence in time; whether the growing exponent is necessary is a natural complexity question.
This preprint gives an exact reduction from a simple constraint problem (choosing compatible elements from finite domains) to -WL equivalence of two explicit uncolored graphs, and uses it to derive conditional time lower bounds.
Fix . The atomic type of a tuple records all equalities and adjacencies among its entries. In joint refinement a round records the old color of and the multiset over of the vectors . In separate refinement it records the old color and the multisets . Two graphs are -WL equivalent () when their tuple-color histograms agree at every round. The bag parameter is (joint) or (separate).
A choice system on domains consists of finite sets and, for each pair , a finite label set with maps , . A successful choice is with for all . Empty domains are allowed.
In Lean (OAI.ParityWL), ChoiceSystem t packages the domains and labels, template t is the -clique with helpers, baseGraph C replaces template types by domains and labels, and zeroLift C, starLift C are the two parity lifts. Colors are defined by recursion on rounds (jointColor, separateColor) with histograms compared as multisets.
For , either convention and the corresponding , for every choice system on domains the two explicit uncolored simple graphs have equal order and
both with common color names on separate graphs and with pure-tuple comparison in the disjoint union. If every domain and label set has size at most , the common order is at most with
When a successful choice exists, the histograms already differ after two joint rounds or one separate round.
The result. The reduction turns compatible-choice problems, which encode sparse satisfiability, into WL equivalence of uncolored graphs whose size grows only linearly in the domain size. Combined with sparsification it gives Theorem 1.3: under the positive-rate ETH there are , such that no deterministic algorithm decides -WL equivalence of -vertex graphs in time for fixed , even when only early-round histograms are compared. This addresses the expectation stated by Lichter, Raßmann and Schweitzer.
Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. A formalization would also give Lean definitions of both WL conventions, reusable by the companion missions in this family on identification and unconditional lower bounds. The ETH consequence (Theorem 1.3) is not part of the Lean goal.
The forward direction (a successful choice yields a distinguishing homomorphism test detected in few rounds) is constructive. The converse is the hard part: one must show that every bounded-treewidth homomorphism test that distinguishes the lifts yields a successful choice, even when bags do not induce cliques, projected images repeat, and some weights vanish. A naive argument that counts only type-preserving homomorphisms fails because non-type-preserving maps also contribute to .
SimpleGraph on finite types; the lifts' vertex types are sigma types of base vertices with parity tags.Multiset-valued types defined by recursion on the round number; equivalence quantifies over all rounds .orderFactor t = t * 2^(t-2+3*(t-1).choose 2) + 12 * t.choose 3 with natural-number subtraction (harmless since ).Successful is an existential over dependent tuples; empty domains are allowed, in which case no successful choice exists and the lifts must be equivalent.The goal is not trivial: the biconditional pins down equivalence exactly, and the detection clause fixes the round.
Needed infrastructure: tree decompositions and homomorphism counts, the Dvořák/Dell–Grohe–Rattan interface for both conventions, and linear algebra for the parity lifts. Contributions toward either direction of the equivalence are welcome.
Sensitivity and block sensitivity are two of the basic complexity measures of a Boolean function . Sensitivity counts how many single-bit flips change the value; block sensitivity allows disjoint groups of bits to be flipped together. Block sensitivity is polynomially related to decision-tree complexity, certificate complexity, degree and quantum query complexity, so the question of how it compares with sensitivity (the Sensitivity Conjecture, from Nisan's 1989 work on CREW PRAMs) decides whether sensitivity belongs to that same family. Huang's 2019 theorem settled the polynomial question: . Nisan and Szegedy had suggested the stronger bound , and the best known separations were quadratic.
This mission asks for a formal proof that no quadratic bound holds, as claimed in an OpenAI preprint dated September 25, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
For and , let be with the coordinates in flipped. For a total Boolean function ,
and is the largest number of pairwise disjoint nonempty sets with for every ; . Always , and a nonconstant has .
For every integer there are and a nonconstant with and
Since the right side tends to infinity, for every some nonconstant has , which is the first sentence of Theorem 1.1. The goal does not include the fixed-exponent statement of Corollary 4.3 (p. 10).
The result itself. It refutes the quadratic strengthening of the Sensitivity Conjecture suggested by Nisan and Szegedy and leaves the true exponent between and : Huang's theorem gives , while Corollary 4.3 of the preprint gives functions with for some and unbounded block sensitivity. Because spectral sensitivity is at most sensitivity, the separation also strengthens Meiburg's spectral result.
Formalizing it. The objects are finite and elementary, so a formal proof is a complete certificate of an explicit combinatorial construction. Huang's theorem has been formalized in Lean; a formal proof here would place the lower side of the gap on the same footing.
Known separations compose small gadgets, and composition multiplies both measures in a way that keeps the exponent at . To break it, a recursion must grow the number of disjoint sensitive blocks by a factor per level while ordinary sensitivity grows by only . The preprint's nested predicates on a labelled tournament (Section 2) achieve this, but a single bit flip can repair a failed gate condition only by changing two child predicates at once. Controlling sensitivity therefore requires tracking these joint sensitivities alongside ordinary ones at every input, not only at the input where the blocks are found (Proposition 3.1, p. 5), and the random edge labelling must exclude dense local configurations (Lemma 2.1, p. 3).
Fin n → Bool; flip x B flips the coordinates in a Finset. sensitivity and blockSensitivity are Finset.sup over all inputs of the local counts; block families are finsets of pairwise disjoint nonempty finsets, each of which changes the value.ℝ. Nonconstancy (∃ x y, f x ≠ f y) forces , so the division is genuine.Welcome contributions: a reusable library of Boolean-function complexity measures (sensitivity, block sensitivity, certificate complexity) and composition lemmas such as Lemma 4.2 (p. 9).
The discrete Fourier transform of length is computed by the fast Fourier transform with arithmetic operations, and this has been the benchmark since Cooley and Tukey (1965). Whether operations are necessary is one of the basic open questions of algebraic complexity theory. Lower bounds of order are known only under restrictions on the algorithm: bounded coefficients, unitary gates on exactly registers, or bounded conditioning of intermediate maps. In the unrestricted model of linear circuits, where coefficients are arbitrary complex numbers and only arithmetic operations are counted, the question remained open. This mission concerns that unrestricted question.
The source of this mission, an OpenAI preprint dated September 25, 2026, claims that the lower bound fails in the unrestricted complex linear-circuit model.
For let and . A linear circuit of length has inputs and the constant , followed by a finite sequence of gates. Each gate computes , or from previously available values , where is a fixed coefficient; each gate costs one. Values may be reused arbitrarily, and the outputs are designated available values. The circuit computes if its outputs equal for every . Coefficients may depend on and have no bound on size or description; depth, storage and conditioning are unrestricted. Let be the minimum number of gates.
equivalently: for every and every there are and an exact circuit for with fewer than gates. The Lean statement OAI.ExactFourier.main_theorem is this second form and is open on the platform.
The statement does not assert an upper bound for every length, a uniform construction, or anything about numerical stability. A companion OpenAI preprint gives a quantitative all-length bound in a model that also charges coefficient preparation; that result is not part of this mission.
The theorem refutes the assertion that for some fixed and all large in the unrestricted linear model. It shows that the known lower bounds necessarily depend on their restrictions (bounded coefficients, conditioning, unitary gates). The mechanism, a single finite tensor saving amplified through tensor powers, is a general tool: one strict improvement over the standard axis-by-axis algorithm for one tensor power of one nonmonomial matrix yields an exponent improvement for all tensor powers.
The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. The existence part of the argument is non-constructive (it proceeds by contradiction through price functions and compactness), so a formal proof is a meaningful check.
Leading-constant improvements of the FFT do not change the scale, and every classical structural algorithm (Cooley–Tukey, Good–Thomas, chirp) has that scale. A gain in the exponent of the logarithm needs a saving that compounds across many tensor factors; but a saving for one tensor power of a small matrix does not obviously transfer to Fourier matrices of growing length, because Fourier factorizations introduce diagonal twiddle factors and change the coordinate set. In addition, the existence of a single finite saving is itself not exhibited explicitly and must be proved.
Gate w is add i j, sub i j or scale c i with c : ℂ, referencing the values available so far.Program n k is a list of gates in topological order; values are the inputs and value is the constant (via Fin.snoc x 0).Circuit n has size, a program of that size, and outputs : Fin n → Fin (n+1+size); output selection is free.fourierMatrix n j k = zeta n ^ (j*k) with zeta n = exp(2πi/n); Computes is equality with mulVec for every input.MainStatement: for every real and there are and a computing circuit with size < c * n * logb 2 n.A complete development needs tensor products of matrices and circuits, the Chinese Remainder (Good–Thomas) identification of with for coprime , a Toeplitz/Vandermonde factorization of on its own coordinates, and the price-function existence argument (separation, compactness, feedback). Contributions formalizing Lemma 2.3 (tensor amplification) and Proposition 3.4 (transfer of a finite win to Fourier circuits) are natural first steps.
Two-way deterministic finite automata (2DFAs) recognize exactly the regular languages (Rabin and Scott; Shepherdson, 1959), but letting the head revisit the input can change how much finite control is needed. In 1978 Sakoda and Sipser asked for the state cost of converting one-way and two-way nondeterministic automata into 2DFAs: is a polynomial number of states always enough? They identified a complete witness family , now called one-way liveness, whose letters are binary relations on an -element set; a word is live when the product of its letters is nonempty. Lower bounds against unrestricted 2DFAs — whose head may reverse anywhere and arbitrarily often — have been the difficult part of this question.
An automaton has a finite set of states and a read-only head on a word over an alphabet , bracketed by two distinct endmarkers. The head starts on the left endmarker in the initial state; each transition depends on the current state and scanned symbol, changes the state, and moves the head left, right or not at all, never across an endmarker. A deterministic rule gives at most one successor (rules may be partial); a nondeterministic rule allows several. Acceptance means some finite computation reaches an accepting state; infinite nonaccepting computations reject. Two conventions are considered: under the first, an accepting initial configuration counts; under the second (positive convention) at least one transition is required. All states are counted.
For let be the monoid of binary relations on with path-order product, iff and for some , and identity . The one-way liveness language is
where the empty product is , so the empty word is live.
For every :
The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. The theorem gives an exponential separation between one-way nondeterministic automata and unrestricted two-way deterministic automata, improving the quadratic bound of Adeogun and Kapoutsis to an exponential one. Corollary 1.2 of the source deduces that no polynomial bounds the deterministic two-way state cost of -state 2NFAs uniformly over all finite alphabets. The alphabet has letters, so the result does not address a fixed alphabet or logarithmic-space complexity classes. A companion OpenAI preprint uses the same language to prove an exponential lower bound for complementing 2NFAs.
Formalizing it. The statement is a finite combinatorial claim about two explicit machine models. A formal proof would certify the passage from deterministic computations to products in the Brauer diagram monoid and the rank-loss induction with explicit constants ( conjugates, additions, step ).
Earlier exponential bounds rely on restricting how often the deterministic head reverses; an unrestricted 2DFA may revisit a cell arbitrarily often as input length grows, and crossing-sequence arguments then lose control. The central obstacle is to represent repeated visits to a cell by an object that depends only on that cell's symbol, not on its neighbors, so that the machine induces a monoid map onto the relation monoid. Once such a representation exists, one still needs a lower bound on its size that grows exponentially in rather than polynomially.
BRel (Fin h), a structure wrapping Fin h → Fin h → Prop, with the monoid structure given by path-order composition and identity Eq; OWL h is the set of words whose List.prod relates some pair.Symbol Alpha adds left and right endmarkers; moves are left | stay | right; head positions are Fin (w.length + 2) and Move.Rel fixes the position change.NMachine Alpha n and DMachine Alpha s have state types Fin n, Fin s, a set of accepting states, set-valued or Option-valued transitions, and boundary axioms forbidding left moves on the left endmarker and right moves on the right endmarker.FiniteRun positive uses TransGen (at least one step) when positive = true and ReflTransGen otherwise; Recognizes positive L means acceptance exactly on L.NoLeft forbids left moves in the source automaton. The recognizer clause quantifies over both conventions with the same machine.(h - 2) / 31, and s ranges over all natural numbers (an s = 0 machine has no states and cannot recognize the language).Given a finite collection of strings, the shortest common superstring (SCS) problem asks for a shortest string that contains every member of as a contiguous substring. It is a basic model of sequence assembly (reconstructing a long DNA sequence from overlapping fragments) and of data compression, and it is a standard test problem for approximation algorithms. Computing the optimum exactly is hard — Blum, Jiang, Li, Tromp and Yannakakis showed the problem is MAX SNP-hard, so it has no polynomial-time approximation scheme unless P = NP (Blum et al., J. ACM 1994) — so the natural question is the best constant factor achievable in polynomial time. For decades the target has been factor : the classical Greedy conjecture asserts that repeatedly merging the pair with maximum overlap achieves it.
A string is a finite list of symbols; a string is a substring of if for some strings (the empty string is a substring of everything). For a finite list of strings, a common superstring is a string having every as a substring, and
where counts symbols. The alphabet is unbounded: each symbol is given by an explicit binary label, and the input is measured by its total encoded bit length . An algorithm runs in polynomial time if its running time on a bit-level machine is bounded by a polynomial in .
In Lean (namespace OAI.Superstring), a symbol is List Bool, a word is a list of symbols, and an instance is a list of words. Substring containment is Mathlib's infix relation <:+:, opt S is the infimum of lengths of common superstrings, and HasPolynomialImplementation f asks for a Mathlib Turing.TM2ComputableInPolyTime certificate for f with respect to an explicit self-delimiting binary encoding of instances and outputs, with every stack alphabet finite.
There is a function from instances to words, computable in polynomial time in the encoded input length, such that for every instance
The goal is published on the platform with status Open.
The result itself. Factor has been the conjectured benchmark for SCS since 1988, and the best proved polynomial-time ratio before this preprint was (reported in 2026). Theorem 1.1 reaches factor with a new algorithm rather than with Greedy, which a 2026 preprint reports does not achieve factor .
Formalizing it. The statement mixes three components that are each easy to get subtly wrong on paper: the correctness of the output (contiguous coverage of every input), the ratio against the unrestricted optimum, and a running-time bound measured in bits, with symbols of arbitrary label length. The formal statement pins down all three with an explicit machine model. A complete formalization requires both the combinatorial ratio proof and a verified polynomial-time implementation on Mathlib's stack-machine model, which is substantial reusable infrastructure for complexity statements in Lean.
The classical approach builds the overlap (distance) graph, takes a minimum-weight cycle cover as a lower bound, and then opens and concatenates the cycles; the cost of joining cycles is what has kept ratios above . Greedy, the natural candidate for factor , is reported to fail. Any factor- algorithm needs a lower bound on that is tight enough that the cost of connecting all the pieces can be charged to the lower bound a second time without double-counting, uniformly over periodic and highly repetitive inputs. The polynomial running time must also be established at the bit level, with symbols of unbounded encoded length.
List (List (List Bool)): duplicates and empty strings are allowed, and symbols are arbitrary bit lists, so the alphabet is unbounded.List.IsInfix), not subsequence containment.opt is a natural-number sInf; the set is nonempty because the concatenation of all inputs is a common superstring, so the junk value is never used. The ratio is measured in symbols.Turing.TM2ComputableInPolyTime for the encodings encodeInstance and encodeWord (prefix markers for list structure), together with finiteness of every stack alphabet, so the time bound is in input bits on a finite-alphabet machine. A function that is merely computable, or polynomial only in the number of symbols, does not satisfy the goal.In metric -median, a finite set (or ) of clients and a finite set of candidate facilities lie in a common finite metric with rational distances. Given an integer , one opens a nonempty set with and pays
Candidate facilities are part of the input and need not coincide with the clients. It is one of the basic clustering and facility-location objectives, and its approximability has been a testing ground for LP rounding, primal-dual methods and local search. A lower bound has long been known: if , no polynomial-time algorithm achieves a factor below in this candidate-facility model, by a reduction from Feige's coverage gap. The best polynomial-time algorithms had reached , leaving a gap between and .
This mission asks for a formal proof that the threshold is exactly , as stated in an OpenAI preprint dated September 24, 2026 (source): a deterministic polynomial-time -approximation for every fixed , and hence, under , an infimal approximation factor of exactly . The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
An instance consists of points with a rational distance table that is a metric (nonnegative, zero exactly on the diagonal, symmetric, triangle inequality), a client set , a facility set (index sets that may overlap), and an integer , encoded in binary. A feasible solution is a nonempty with . An algorithm is an -approximation if it always outputs a feasible with , and it is polynomial-time if it runs on a deterministic multi-stack Turing machine with finite alphabets in time polynomial in the encoding length.
For every fixed there is a deterministic polynomial-time algorithm which, on every instance, returns a feasible with
If , then
The infimum is not asserted to be attained.
The result itself. It closes the approximability of metric -median with specified candidate facilities up to arbitrarily small additive error in the factor, ending a sequence of improvements from LP rounding through local search (), bi-point rounding (, ) to . It shows that the FPT factor of Cohen-Addad et al. is achievable in polynomial time. The case has a different and still separate lower-bound question.
Formalizing it. The goal combines an algorithmic theorem with a hardness reduction. A formal proof needs: the Li–Svensson reduction from constant-additive pseudo-approximations (Theorem 2.2, p. 4); the grid preparation and iterative rounding with a finite directed comparison inequality whose scalar estimates are proved by rational polynomial certificates (Sections 3–5, Appendix A); derandomization by moment-matching distributions of polynomial size (Section 6); and, for the lower bound, NP-hardness of Feige's coverage gap in the Lean computation model. All are reusable for other clustering and covering problems.
Two obstacles meet. The cardinality budget is hard: allowing a constant number of extra facilities makes good connection cost much easier, and earlier rounding analyses in the iterative graph framework only certify factors at least (p. 2). The preprint's new ingredient is a potential that keeps track of surviving assignment copies after an opening and a finite directed comparison inequality (Theorem 4.1, p. 13) that pays for erasures. Then the randomized rounding must be made deterministic and polynomial-time while keeping the analysis valid, which requires preserving exactly the low-order moments the analysis uses (Lemma 6.1, p. 28; Theorem 6.2, p. 33), before Li–Svensson removes the additive surplus. The hardness side is classical but rests on the PCP-based Max--Coverage gap.
Instance carries n, a Fin n → Fin n → ℚ metric (distance_eq_zero is an iff, so a true metric), client and facility Finsets, and 1 ≤ k ≤ facilities.card. cost sums nearest distances over clients; optimum is the minimum over nonempty facility subsets of size .FactorCorrect α I out requires that mask to describe a nonempty with and .Turing.TM2ComputableInPolyTime with finite tape alphabets, on the fixed binary instance encoding.approximationFactors is the set of admitting such an algorithm, and the goal is sInf approximationFactors = 1 + 2/Real.exp 1 under the hypothesis Complexity.PNeNP, where P and NP are defined in the same machine model (NP via polynomial-length witnesses and a finite-alphabet polynomial-time verifier). The set is nonempty by the milestone and bounded below, so sInf is meaningful.In metric -median, a finite set (or ) of clients and a finite set of candidate facilities lie in a common finite metric with rational distances. Given an integer , one opens a nonempty set with and pays
Candidate facilities are part of the input and need not coincide with the clients. It is one of the basic clustering and facility-location objectives, and its approximability has been a testing ground for LP rounding, primal-dual methods and local search. The hard part of the problem is the facility budget: a solution with small connection cost is much easier to find if a few extra facilities may be opened, and every approximation algorithm must eventually enforce on its output.
This mission concerns two tools for enforcing that budget and their combination into a randomized approximation strictly below factor on arbitrary finite rational metrics, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
Write and . A comparison solution of size assigns each client to a nearest member of (ties broken by fixed priorities); is the cluster of and , with . An anchor is a supplied feasible with . A certificate partitions into good and bad centres and gives distinct proxies for the good centres. A randomized polynomial-time algorithm is a polynomial-time multi-stack Turing machine that reads the encoded instance together with a string of fair random bits whose length is a fixed polynomial in the input length.
Let be disjoint, with distances between distinct indices positive integers bounded by a fixed polynomial in . Fix , and a rational . There is a randomized algorithm that, given an anchor with and a failure parameter , always returns with , runs in time polynomial in and , and, whenever some comparison solution of size and cost admits a certificate with
satisfies with probability at least . The algorithm is not given , or the certificate.
There is an absolute constant such that for every fixed some randomized polynomial-time algorithm for metric -median always returns a feasible (nonempty, , ) and satisfies
The result itself. Theorem 1.1 makes the running time single-exponential in the number of clusters without accurate proxies, so logarithmically many exceptions are tractable; FPT methods with dependence do not give this by setting . Combined with a new proof of bounded-price strictness for one compatible execution of the logarithmic-surplus construction of Cohen-Addad, Grandoni, Lee, Schwiegelshohn and Svensson (Lemma 8.1, p. 43), it yields Theorem 1.2: a randomized approximation strictly below , both with high probability and in expectation, that opens at most facilities on every output. A companion preprint proves a stronger deterministic bound by an independent route; Theorem 1.2's interest is the way recovery and payment accounting together enforce the budget.
Formalizing it. The statements are fully explicit about the machine model, the random bits, and the input encoding. A formal proof would need local-search anchoring (Theorem 3.3), leader/ball sampling with amortized radius guesses (Section 4), a finite categorical continuous-greedy algorithm with explicit error (Lemma 5.1, p. 21), the surplus construction as an external interface (Theorem 7.1, p. 35), and metric rounding and transfer (Lemma 2.1, p. 6). The submodular-optimization and local-search components are reusable.
Every factor- dual-fitting argument charges to a client set served by a comparison facility, which gives exactly ; improving the constant requires saving on connection cost while still paying for all regular openings with one final price, one set of copy lengths and the budgets of one actual replay of the construction (Section 1.2, p. 3). On the recovery side, guessing a good solution from an anchor naively costs ; keeping the dependence single-exponential in the number of bad clusters requires interleaving leader sampling and removals and amortizing radius guesses over disjoint client sets (Section 4). Theorem 1.1 holds only for normalized integral metrics; the global application must construct its anchors after normalization and transfer the final cost bound back (Lemma 2.1, p. 6).
RationalMetricInput: points Fin pointCount, a rational pseudometric table (zero on the diagonal, symmetric, triangle inequality), client and facility Finsets covering all points (they may overlap, so clients and facilities may share locations), a nonempty facility set and a positive budget . Feasible S is , , and nonempty when there are clients; optimum minimizes over nonempty subsets of size .BinaryRandomizedAlgorithm is a TM2ComputableInPolyTime function of (input bits, random bits) with finite alphabets, using randomBits.eval (input length) fair bits; probabilities and expectations are uniform averages over all seeds.Real.rpow); the same algorithm must also satisfy the expectation bound.Input adds disjointness of and , integral distances, positivity between distinct indices, and an anchor with anchor.card = budget; Bounded bound caps distances by a fixed polynomial in ; ζ is passed in unary precision , and PolynomialWork bounds work by . A Certificate encodes with , , the good set, injective proxies into the anchor, the proxy-cost promise with lexicographic tie-breaking, and at most bad centres.A set of unit-length jobs with precedence constraints is to be run on a fixed number of identical machines so that all jobs finish as early as possible. For two machines this was solved in 1969–1972; for a number of machines given as part of the input the problem is NP-complete (Ullman, 1975). Whether the problem is polynomial-time solvable for three machines, written , is problem OPEN8 in the appendix of Garey and Johnson's 1979 book and is one of the best-known open questions on the complexity of scheduling.
The source of this mission, an OpenAI preprint dated September 24, 2026, claims a deterministic polynomial-time algorithm.
The input is a directed acyclic graph on , , given as an explicit list of arcs, and optionally an integer deadline with . A feasible schedule with makespan at most is a map
such that each value is taken at most three times (three machines) and for every arc (precedence). Slot means execution during . There are no release dates, communication delays or other resources. The input length is the length of the binary encoding of the graph and deadline.
There is a single deterministic multitape Turing machine and a constant such that, on every such input of length , halts within
steps and
The exponent is the one stated in the paper and is not optimized; the content of the theorem is that a fixed polynomial bound exists. The Lean statement OAI.ThreeMachine.main_theorem is open on the platform.
The theorem resolves the polynomial-time side of Garey and Johnson's OPEN8: unit-job makespan scheduling with arbitrary precedence constraints on three identical machines lies in P. Previous exact algorithms were either restricted to special precedence structures (forests, bounded height) or subexponential, and approximation schemes did not decide the optimum. The structural statement behind the algorithm, that feasible schedules admit recursive decompositions whose interval job sets have descriptions of bounded size, may be of independent use for other fixed-machine scheduling problems. No practical running time is claimed.
The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. A formal proof would also certify the running-time analysis in an explicit machine model, which is rarely done for algorithmic results of this size.
Removing selected slots from a feasible schedule leaves gaps that can be rescheduled independently, which suggests a recursive search over the job sets of gaps. The obstacle is their number: naming a gap by its two boundary triples does not determine its job set, and intersecting descriptions inherited from ancestors can make the descriptions grow without bound along a recursion of linear depth. The subexponential decomposition of Nederlof–Swennenhuis–Węgrzycki controls the number of subproblems only up to ; a polynomial bound needs every subproblem to have a global description of constant size.
Instance n is a list of arcs on Fin n; acyclic forbids a Relation.TransGen cycle. Jobs are Fin n (shifted to in the encoding).Feasible G T τ: slots in , at most three jobs per slot, strict precedence.CorrectOutput distinguishes the optimization mode (none) and the decision mode (some T).Machine k q g over Fin (g+3) with tapes; input on tape 0 encoded by encodeInput (self-delimiting binary numbers), output read from tape 0 after halting. The time bound is with the encoded length.A complete development needs the combinatorics of the decomposition (separators and bounded global descriptions), a dynamic program over polynomially many descriptions, and its implementation and time analysis on the given Turing machine model. Contributions formalizing the purely combinatorial structure theorem, independently of the machine model, are welcome.
In the trace reconstruction problem an unknown binary word is passed repeatedly through a deletion channel: each bit is deleted independently with known probability and the surviving bits are concatenated in order. Each output, called a trace, reveals its length and its bits but not which positions survived. The question is how many independent traces are needed to recover every word exactly with a fixed success probability. The problem arises in DNA storage and sequencing, in multiple sequence alignment, and as a basic test of how much information a channel with synchronization errors destroys. Its central open question has been whether a polynomial number of traces suffices at a fixed deletion probability.
Fix and . A deletion mask keeps bit when ; it has probability . The trace of under is the list of the bits with , in order. Write for the law of the trace of under a random mask.
An estimator with budget receives independent traces of and returns a random word; it may be randomized and its computation is unrestricted. For , the sample complexity is the least such that some estimator recovers every with probability at least ; it is if no finite works. The one-trace distance is
the sum running over all finite binary words.
In Lean (namespace OAI.TraceReconstruction), words are Fin n → Bool, traceMass q x w is the probability of output w, an estimator is a function A : (Fin m → Trace) → Word n → ℝ giving a probability vector for each sample, sampleComplexity n q s : ℝ≥0∞ is the infimum of sufficient budgets, and minTraceTV n q is the minimum of traceTV q x y over .
Fix and . For every sequence of instances with , and ,
At fixed this gives , so no polynomial number of traces suffices. The goal is published on the platform with status Open.
For every fixed and every ,
The result itself. Theorem 1.1 is the first superpolynomial lower bound for exact worst-case trace reconstruction at a fixed deletion probability; previous lower bounds were of order up to logarithms. It holds against unrestricted computation and any fixed positive success probability, and it settles in the negative the question of whether polynomially many traces suffice. Combined with the 2026 quasipolynomial upper bound of Burudgunte, Valiant and Wang, the sample complexity at fixed is now known to lie between and . Theorem 1.2 isolates the underlying phenomenon: some pairs of distinct words have single-trace laws closer than every inverse polynomial.
Formalizing it. The definitions fix exactly what an estimator may see (only the complete traces, no positions or boundaries) and what "sample complexity" means, including the value . A formal proof would certify a lower bound whose argument is a long multi-scale construction with many quantitative error budgets, the kind of argument where an overlooked loss would invalidate the conclusion.
Earlier lower bounds compare two words that differ by a single local defect and compute their trace distance directly; such pairs are distinguishable from polynomially many traces, so no single-defect construction can give a superpolynomial bound. A superpolynomial bound needs pairs of words whose trace laws agree to every polynomial order, while the argument must remain uniform in the deletion probability (which may tend to slowly), keep all constants below scale margins that shrink as the number of construction stages grows with , and transfer a bound for one trace to a bound for independent traces and for arbitrary randomized estimators.
List Bool; traceTV sums over the finite set of all lists of length at most , which contains the support of every trace law, so it agrees with the source's total variation over all finite words.sampleComplexity is an sInf in ℝ≥0∞; the infimum of the empty set is , matching . The lower bound is compared after ENNReal.ofReal, and the right-hand side uses the real power.n q : ℕ → …, Tendsto n atTop atTop, and Tendsto (q k ^ 3 * log (n k)) atTop atTop; the conclusion is ∀ᶠ k in atTop. Logarithms are natural.minTraceTV n q is a real sInf, attained for ; at the set is empty and the junk value does not affect the limit.Sparsest cut asks for a partition of a weighted graph whose crossing capacity is small compared with the demand it separates. It is a basic graph-partitioning primitive (used for divide-and-conquer algorithms, clustering and expansion testing), and its relaxations are the main bridge between approximation algorithms and the geometry of finite metric spaces. In the uniform version every pair of vertices has demand one. The best known polynomial-time approximation, due to Arora, Rao and Vazirani, uses the Goemans–Linial semidefinite relaxation and achieves ratio . How good this relaxation can be, i.e. its integrality gap on uniform instances, has been a long-standing question.
For uniform demands the gap between the lower bound and the upper bound remained. The source of this mission, an OpenAI preprint dated September 24, 2026, claims a lower bound matching the upper bound up to a power of .
Let be symmetric nonnegative capacities on pairs of distinct vertices of . The uniform sparsest-cut value is
A negative-type semimetric is for vectors in a real Hilbert space, satisfying all triangle inequalities ; distinct points may have distance zero. The Goemans–Linial value is
Normalized cut metrics are feasible, so . The integrality gap of is .
There are an absolute and instances on vertices with such that, for all large ,
The Lean statement OAI.UniformSparsestCut.mainGap is open on the platform.
The bound reaches the exponent in , so the Arora–Rao–Vazirani analysis of the Goemans–Linial SDP is tight for uniform demands up to the factor . It strengthens the Devanur–Khot–Saket–Vishnoi and Kane–Meka refutations of the uniform constant-gap conjecture. Geometrically, it gives a finite negative-type metric for which every -Lipschitz map into preserves only a fraction of the average distance. The theorem concerns the basic Goemans–Linial SDP only, not strengthened hierarchies.
The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists.
The sharp general-demand lower bounds (Heisenberg group, Naor–Young) control worst-pair distortion, and Cheeger–Kleiner–Naor note that those examples have constant average distortion into a line, so they cannot give a diverging uniform gap. A uniform-demand example must force every contraction to lose most of the average distance over all pairs, not merely on a few pairs. At the same time the constructed distance must remain of negative type and satisfy all triangle inequalities exactly, and the passage from a probability measure on points to an exactly uniform demand with positive SDP value must be carried out without losing the bound.
Capacity n stores cap : Fin n → Fin n → ℝ, nonnegative, symmetric, zero on the diagonal.cutRatio C B is the crossing capacity of divided by ; OPT C is the sInf over nonempty proper Finsets .NegativeType d requires points x : Fin n → EuclideanSpace ℝ (Fin n) with and all triangle inequalities; Feasible d adds ; glValue C is the sInf of over feasible .A complete development needs cut-cone duality, a Hilbert-space kernel construction with rounded charts, Gaussian direction families, and contraction estimates for maps into . Cut-cone duality and the reduction to exactly uniform demands are reusable. Contributions formalizing Lemma 6.1 (cut-cone duality) or the weak duality are welcome first steps.
A cell-bounded contingency table is a nonnegative integer matrix with prescribed row sums, column sums and an upper bound on each entry. Bounds of zero forbid entries (structural zeros), and bounds of one give bipartite graphs with prescribed degrees, so the model contains degree-constrained subgraph counting and perfect matchings (the permanent). Counting such tables is central to exact conditional inference in statistics and is equivalent to counting integer flows in bipartite networks. Exact counting is #P-complete even for two-row ordinary tables (Dyer, Kannan and Mount, 1997), so the target is a fully polynomial randomized approximation scheme (FPRAS): a randomized algorithm that, for any , returns a -approximation with probability at least in time polynomial in the input length, and .
The source of this mission, an OpenAI preprint dated September 24, 2026, claims an FPRAS with no restriction on dimensions, margins or caps.
For positive integers , margins , with equal totals, and bounds ,
All numbers are written in binary, so a capacity can be exponentially larger than its description. denotes the total binary input length including the rational accuracy parameters . The algorithm uses independent unbiased random bits and is charged for every bit operation.
One randomized algorithm, given and rational , outputs a nonnegative rational with
outputs exactly on every execution when , and performs at most bit operations on every execution. Lean: OAI.ContingencyTables.counting, open on the platform.
The theorem would answer the question left open by Cryan, Dyer and Randall in 2010: approximate counting of cell-bounded tables (equivalently, integral flows in bipartite networks with arbitrary capacities) without any fixed-dimension, large-capacity, density or balance assumption, with polynomial cost on every execution and no oracle. It contains the 0/1 case handled by Jerrum–Sinclair–Vigoda and the fixed-row results as special cases, and via self-reduction it gives approximate samplers for integer flows. A companion preprint of the same family treats exact uniform sampling of uncapped tables. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists.
Two regimes clash. Large capacities cannot be expanded into that many binary choices without exponential blow-up, so geometric (polytope volume) methods are needed for them; but those methods require every cell to be large. Small capacities need combinatorial Markov chains, which in turn must preserve exactly one unit of mass per table despite the multiplicities created by encoding a bounded integer by binary choices. Arbitrary mixtures of tiny and huge caps, zero caps and variable dimensions defeat each approach used alone.
MatchingFPRAS.RandomMachines: a single finite transition table on an 8-symbol alphabet, one random bit per tick; time is counted in ticks (polynomially equivalent to bit operations).encodeCountingInput); outputs are encoded rationals.count r c b is Fintype.card of bounded tables.CountingStatement: one machine and constants , ; with , every tape of length halts with a rational ; if count = 0 every tape outputs ; and the fraction of tapes with is at least .Needed infrastructure: randomized Turing machines, Markov chain mixing and Poincaré inequalities, log-concavity (Prékopa–Leindler), and network-flow feasibility. The machine model and encodings are shared with the exact-sampling mission of this family. Contributions formalizing Proposition 2.2 (contamination bound), Lemma 3.3 (log-concave tree marginals), Proposition 6.1 (weight evaluation) or Proposition 7.2 are welcome.
A contingency table with margins and is a nonnegative integer matrix whose row sums are and column sums are . Such tables are the basic objects of categorical data analysis: conditional tests of independence (Fisher's exact test and its generalizations) compare an observed table with the uniform distribution on all tables with the same margins, and in practice this requires sampling uniformly from that set. The set is finite but can be exponentially large in the input size when margins are written in binary. Whether one can sample it (approximately or exactly) in time polynomial in both dimensions and in the bit length of the margins has been open since the 1990s.
The source of this mission, an OpenAI preprint dated September 24, 2026, claims both an almost-uniform and an exactly uniform sampler for arbitrary margins.
For nonnegative integer vectors , with common total , let
The input is with margins in binary, so its length is polynomial in , and . An algorithm uses unbiased random bits. For laws on a finite set, .
For each , an algorithm halts on every execution in time and outputs with
An algorithm outputs with
terminates almost surely, and has expected running time , with polynomials uniform over all margins. Lean: OAI.ContingencyTables.exactSampling, open on the platform.
The theorem would give the first unconditional polynomial-time exact uniform sampler for contingency tables with arbitrary dimensions and binary margins, with no positivity, sparsity, balance or fixed-dimension restriction, and with all random bits and integer arithmetic counted. It removes the fixed-row restriction of the Dyer–Greenhill and Cryan–Dyer line and the sparsity condition of Arman–Gao–Wormald. The exponents are deliberately large; the contribution is the existence of a polynomial algorithm. Exact time is polynomial in expectation, not on every run. A companion preprint of the same family gives an FPRAS for counting tables with cell bounds. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists.
Markov-chain approaches mix rapidly for a fixed number of rows, but the bounds degrade with the row count. Geometric (polytope) methods need all margins to be large, and fail when some margins are tiny while others are huge, which is exactly the mixed regime that arbitrary binary margins allow. Making the sampler exact rather than approximate adds a separate difficulty: the residual-mixture correction requires that the actual output law of the approximate sampler can be computed, with cost polynomial in the accuracy bits.
MatchingFPRAS.RandomMachines: a single finite transition table over an 8-symbol tape alphabet; each tick reads one random bit and either moves, writes or halts. Time is counted in ticks, polynomially equivalent to bit operations.encodeNat, encodeMargins); outputs are row-major matrix encodings left on the tape (OutputsTable).tableMass A input t X and haltMass A input t are the fractions of the random tapes of length that halt with output , respectively halt at all, within ticks.ExactSamplingStatement: one machine and constants , such that for all with equal totals: every halted output is in ; tableMass → 1/|Ω| for each table; haltMass → 1; and , the expected running time, is at most .BoundedSamplingStatement: every tape of length halts with a feasible table, and the TV distance to uniform is at most .Needed infrastructure: randomized Turing machines and their output laws, Markov chain mixing (conductance, Poincaré inequalities), and log-concave sampling. Contributions formalizing Theorem 4.3 (graph Poincaré inequality), Theorem 5.1 (dense completion draw), Proposition 6.3 (law tabulation) or the Göbel–Liu–Manurangsi–Pappik correction are welcome.
A matroid abstracts linear independence: a finite ground set with a family of "independent" subsets that is closed under subsets and satisfies the augmentation axiom. Its maximal independent sets, the bases, all have the same size, the rank. Matroid intersection, finding a common basis of two matroids, is one of the central polynomially solvable problems of combinatorial optimization (Edmonds, 1979). Counting common bases is much harder. It contains counting bases of a single matroid (take both matroids equal) and counting perfect matchings of a bipartite graph (take two partition matroids), and exact counting is #P-hard. The natural goal is therefore a fully polynomial randomized approximation scheme (FPRAS): an algorithm whose output is within relative error with probability at least , in time polynomial in the input size, and . The matroids should be accessible only through independence oracles.
Let be matroids of the same rank on the ground set , supplied by exact independence oracles: a query is an -bit indicator of a subset, and the answer says whether it is independent. The quantity to estimate is
the number of common bases. The input also contains rationals ; denotes the binary encoding length of . Oracle calls are counted separately from the bit operations used to build queries and process answers.
There is a single randomized oracle algorithm and a fixed polynomial such that, for all rank- matroids on and rational , it outputs a nonnegative rational with
the output is always when , and on every execution the numbers of oracle calls and bit operations are at most . The algorithm uses only independent fair random bits. The goal statement is published on the platform with status Open.
The result itself. Theorem 1.1 answers the question recorded by Liu (2023) and extends both the single-matroid FPRAS of Anari–Liu–Oveis Gharan–Vinzant and, in the bipartite-matching case, the permanent FPRAS of Jerrum–Sinclair–Vigoda. It needs no representation of either matroid and holds for unrestricted rank, whereas the previous oracle-model scheme was fully polynomial only for . The source derives FPRASs and almost-uniform samplers for common independent sets of prescribed, unrestricted or maximum size, even for matroids of different ranks (Corollary 9.1).
Formalizing it. The Lean goal fixes a concrete machine model, so it states a complete complexity-theoretic claim with no informal "polynomial-time" left. A proof would combine Lorentzian-polynomial inequalities (Brändén–Huh), a transport inequality, a Markov-chain Poincaré bound, and simulated annealing with explicit bit accounting. Each layer is reusable: Mathlib has matroids, but no Lorentzian polynomials, no mixing-time theory of this kind and no randomized-algorithm framework.
For one matroid, the bases-exchange walk mixes rapidly because the basis generating polynomial is log-concave. The intersection of two matroids has no such structure: its common bases need not be connected by short exchanges, and the natural chain on transversals of the paired construction passes through states of exponentially small weight, so positivity and connectivity alone give no polynomial bound. Earlier approaches either lost exponential factors or needed real-stable polynomials that an independence oracle does not provide. The proof must balance defect classes, as in Jerrum–Sinclair–Vigoda, and establish a Poincaré inequality for observables from matroid-theoretic inequalities alone.
Matroid (Fin n) with ground set univ and eRank = r for both. Oracles are functions Bool → (Fin n → Bool) → Bool, required to answer independence queries exactly.Program k s for a register machine with binary stacks: push/pop, fair coin, oracle query on an -bit register, and halt with output (register 6)/(register 7) as a rational. Inputs are loaded in binary.Prescribing the probability that each edge belongs to a random perfect matching does not determine the distribution of the whole matching. The largest entropy compatible with those edge probabilities, , measures how many matching choices can coexist with them, and it links three topics: lower bounds on the number of perfect matchings, convex-optimization approaches to approximate counting, and the facial geometry of the perfect-matching polytope. For bipartite graphs, Schrijver's permanent inequality (Schrijver 1998) and Gurvits' weighted Bethe inequality (Gurvits 2011) give the clean comparison between and sums of one-coordinate entropies. For general graphs, odd cuts make such comparisons harder, and Anari, Oveis Gharan and Vinzant (2018) asked (FOCS version, Conjecture 6) whether the maximum binary-coordinate entropy over the polytope exceeds by only a linear function of the number of vertices.
Let be a finite loopless multigraph with vertex set , , and edge set (parallel edges are distinct coordinates). A perfect matching is a set of edges covering each vertex exactly once; is the set of them and . The perfect-matching polytope is
For put, with natural logarithms and ,
The milestones are listed in attack order: the face of a triangle expansion (Lemma 5.1), the coefficient-eight nonlinear bound (Theorem B.1), deterministic approximate counting (Theorem 1.2) and its singleton-loop variant (Proposition C.1).
If has at least one perfect matching, then for every
The bound holds on the whole polytope, boundary included. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. The upper bound is Shearer's inequality; the content is the lower comparison with coefficient , valid in nonbipartite graphs where the bipartite coefficient fails (the source gives an eight-vertex counterexample, and Corollary 5.3 shows any universal coefficient is at least ). Optimizing over gives , answering the Anari–Oveis Gharan–Vinzant question. Plugging in uniform marginals gives for graphs with edge-disjoint perfect matchings, and for -regular graphs whose odd cuts all have at least edges. The same entropy framework yields a deterministic polynomial-time algorithm approximating within a factor for graphs with binary edge multiplicities (Theorem 1.2).
Formalizing it. The goal is a finite-dimensional inequality about polytopes and entropies, accessible to Mathlib's convexity and analysis libraries. The milestones extend the mission to a certified polynomial-time counting algorithm in Mathlib's Turing-machine model, a rare example of a formally specified approximation algorithm for a #P-hard quantity.
Shearer's inequality gives the upper bound in one line, and in bipartite graphs the lower bound follows from permanent inequalities that have no analogue for general graphs. A direct convexity argument fails because is not differentiable across faces of : at a boundary mean the maximum-entropy law lives on a lower-dimensional face, and its covariance is singular in the ambient edge space. The lower bound must therefore be proved face by face, and it needs the sharp geometric estimate for the minimal face containing ; the earlier rank bound would not give the coefficient .
LooplessGraph V E: endpoint maps left right : E → V with left e ≠ right e, on finite types with decidable equality, so parallel edges are distinct elements of E. A perfect matching is a Finset E with exactly one edge at each vertex.polytope G is the convex hull of matching indicator vectors in E → ℝ; maxMatchingEntropy G x is sSup of the entropies of probability vectors on matchings with mean x. On the polytope this set is nonempty, compact and bounded, so the sSup is the attained maximum; off the polytope it would be junk, which is why the hypothesis x ∈ G.polytope is required.entropy uses Real.negMulLog, so ; complementEntropy x is .0 < m, Fintype.card V = 2 * m, and a perfect matching exists. The coefficient is the real number 2 - 2 / m.Turing.TM2ComputableInPolyTime with finite alphabets, binary encodings of the vertex count and of positive multiplicity records, and require polynomially bounded output length.TM2. The polytope and entropy definitions are reusable for other counting missions.A perfect matching of a graph is a set of edges covering every vertex exactly once. Finding one is easy — Edmonds (1965) gave a polynomial-time algorithm for general graphs — but counting them is hard: Valiant (1979) proved exact counting #P-complete already for bipartite graphs, where the count is the permanent of a 0–1 matrix. Exact counting is tractable only in special classes, such as planar graphs via Pfaffians (Kasteleyn 1963). The natural relaxation is a fully polynomial randomized approximation scheme (FPRAS): an algorithm that, with probability at least , returns the count within relative error , in time polynomial in the input size, and . Whether perfect matchings in general (nonbipartite) graphs admit an FPRAS was explicitly raised by Jerrum and Sinclair in 1989 and has been a benchmark question in approximate counting since. Perfect-matching counts are partition functions of the monomer–dimer model, so the question also connects to statistical physics.
A finite simple undirected graph on vertices is given by a set of edges, each written once as a pair with . A set is a perfect matching if every vertex lies in exactly one edge of , and
(The graph with no vertices has ; any graph with an odd number of vertices has .)
A randomized algorithm is modelled as a single fixed machine with a finite transition table over a finite tape alphabet, which at each step reads the current tape symbol and one fresh fair random bit, then writes, moves, or halts. The input is the graph in binary (number of vertices, number of edges, the sorted edge list) followed by the rationals and in reduced form; the output is a rational number written on the tape when the machine halts.
There are a machine and constants , such that for every graph and rationals , , with :
The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. The theorem answers the Jerrum–Sinclair question affirmatively: perfect matchings in arbitrary graphs can be approximately counted as efficiently, up to polynomial factors, as in the bipartite case. The worst-case time bound holds for every execution, not just in expectation. Via standard reductions, the source also derives counting schemes for edge subsets with prescribed vertex degrees and for matchings of a fixed size (Corollary 10.1). The accompanying samplers for those families always return a feasible object and approximate the uniform law in total variation.
Formalizing it. The statement fixes a concrete machine model, input encoding and time bound, so a formal proof would certify both correctness of the estimator and the polynomial running time of an explicit algorithm — a level of rigor rarely reached for Markov-chain Monte Carlo results, whose analyses involve many interacting constants.
The natural approach extends the Jerrum–Sinclair–Vigoda Markov chain on perfect and near-perfect matchings, with weights learned while edge activities are gradually lowered. In general graphs this approach provably fails: Štefankovič, Vigoda and Wilmes constructed graphs on which every chain of that type, for any hole-dependent weights, has either exponentially small stationary mass on perfect matchings or exponentially slow mixing. Odd cycles (blossoms) are the reason the bipartite canonical-path arguments do not carry over. A solution needs a different state space and a different mixing analysis.
GraphInput is a vertex count n and a Finset (Fin n × Fin n) of edges with strictly increasing endpoints, so loops and duplicate edges are excluded. Perfect G M requires M ⊆ edges and that each vertex is incident to exactly one edge of M; Z G is the number of such M.RandomMachine: a finite transition table on Fin 8 symbols, whose step consumes one random bit and performs a Turing.TM0 write or move, or halts. run folds tick over a list of t bits; halted configurations are absorbing.encodeInput writes the vertex count, edge count and lexicographically sorted edges in binary, then encodeRat ε and encodeRat δ (reduced numerator with sign, denominator). Outputs requires that the machine has halted and the tape to the right of the head is exactly the encoding of the output rational.RandomMachine transitions, Markov-chain spectral-gap bounds, and sampling-to-counting reductions. The machine model and encodings are reusable for other approximate-counting missions.