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?
Proving that explicit Boolean functions need large circuits is the central problem of circuit complexity. Even for very shallow circuits the known bounds are far from what counting arguments suggest. A depth-three OR–AND–OR circuit is an OR of CNFs, with unbounded fan-in and arbitrary sharing; most functions need gates in this model, yet for every explicit function in P the best known lower bounds had the form for a constant . Håstad's switching lemma gave for parity (1989), and Paturi, Pudlák and Zane showed this is tight for parity up to a constant factor (1999), so parity cannot go further. Moving the exponent beyond any constant multiple of for an explicit language was identified as an open problem in the depth-three literature (Gurumukhani, Paturi, Pudlák, Saks and Talebanfard, CCC 2024; Gurumukhani, Kleber, Paturi, Rosin and Talebanfard, CCC 2026). Depth-three lower bounds are also tied to satisfiability algorithms and to Valiant's approach to lower bounds for logarithmic-depth circuits.
This mission asks for a formal proof that one polynomial-time language requires depth-three gates, as stated in an OpenAI preprint dated September 23, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
A literal is a variable or its negation; negations are free. A depth-three OR–AND–OR circuit on inputs has bottom OR gates (clauses) reading literals and optional constants, middle AND gates reading bottom gates, and one top OR gate reading middle gates. Fan-in and fan-out are unbounded and gates may be shared. Its size counts every bottom gate, every middle gate and the output gate. For , is the least size of such a circuit computing exactly. For a language , is its membership function on .
There are a language , a deterministic multi-tape Turing machine deciding , and positive integers such that the machine halts within steps on every input of length , and for every real there is with
The language and machine are fixed before ; no uniformity or bottom fan-in restriction is imposed on the circuits.
The result itself. It is the first explicit depth-three lower bound whose exponent is not , crossing the barrier at which parity, majority and the earlier code-membership functions stop. It is weaker than the bound asked by Håstad, Jukna and Pudlák and gives no fixed improvement of the exponent's power. Because every function has a single-CNF representation when bottom fan-in is unbounded, the result depends on counting all gates, as stated.
Formalizing it. Circuit lower bounds are combinatorial statements well suited to formal proof, but the libraries are thin: a complete development needs a Turing-machine time bound for a concrete polynomial-evaluation language, restriction arguments for CNFs, the Erdős–Rado sunflower lemma, and limited-independence estimates from hashing and polynomial interpolation. All of these are reusable in complexity theory. No machine-checked depth-three lower bound beyond small cases is known.
The classical switching lemma changes the normal form and loses a constant in the exponent, which keeps bounds at the scale, and parity is provably no harder than , so a different hard function and a different argument are needed. The preprint needs a function whose sign has small correlation with every moderately wide CNF, independently of the number of clauses. Its key step (Lemma 3.1, p. 4) expresses each randomly restricted width- CNF as a signed combination of width- CNFs with expected coefficient mass at most two, with no dependence on the clause count. A uniform polynomial-time language cannot search for a hard function at each length, so hardness must come from inputs that carry the parameters selecting a hard slice (Section 5).
Circuit3 (Fin n) has bottomCount raw clauses (lists of literals or Boolean constants), middleCount AND gates given as Finsets of bottom indices, and a top Finset of middle indices; gateCount = bottomCount + middleCount + 1. Computes requires exact agreement with L (List.ofFn x) on every input.FiniteMultiTapeMachine has finitely many tapes, a finite alphabet, finite states, an input tape initialized with the input, and an accept predicate on the halting state. MultiTapeHaltsIn M w (L w) (C*(|w|+1)^a) requires halting within the bound with output L w.ℝ.In the -server problem, labelled servers occupy points of a metric space, requests arrive online, and each request is served by moving one server onto it; the cost is the total distance moved, compared with the offline optimum through the competitive ratio. A companion OpenAI preprint claims that on every metric there exists a randomized policy with ratio against oblivious requests, matching the known worst-case lower bound. That result is an existence statement: it gives no procedure for computing the policy's probabilities.
This mission asks whether the bound can be realized by one uniform algorithm with explicit bit complexity on all finite rational metrics, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
Fix and . A rational metric on is a table that is nonnegative, zero exactly on the diagonal, symmetric, and satisfies the triangle inequality. An initial labelled tuple may have repetitions. For a request word , is the algorithm's total movement and the minimum over all choices of serving labels with knowledge of . denotes the total binary length of the encoding of .
The computational model is a bit machine: a finite control with an input tape, finitely many work tapes over , an output channel, and one fresh unbiased random bit per step. At each request the input tape is replaced by the encoded request, the internal state is retained, and the output after the step budget names the server to move.
There are an absolute constant and a polynomial such that a single uniform randomized online algorithm, on every instance as above,
with independent of and of its length.
The result itself. It converts the existence theorem into an algorithm whose ratio is independent of , using only unbiased random bits and polynomial work per request in the input length and the bit length of the request counter. The price is an additive constant with no size bound: the algorithm may serve a very long initial stretch with a fixed label while its constructor runs. Coester and Cosson obtain stronger time and randomness guarantees but with ratio on general metrics; the two results are incomparable.
Formalizing it. The goal is stated in an explicit machine model, so a formal proof certifies both the competitive bound and the bit-complexity bound. It needs the companion existence theorem (Theorem 2.1 here, p. 4) as an input; a full development therefore also requires formalizing that theorem or taking it as a separate milestone. Exact rational linear algebra (Fourier–Motzkin elimination), dyadic rounding of probabilities, and step-counted machine simulation are reusable.
Knowing that a good policy exists does not give its probabilities, and a finite horizon alone does not control a long input on which the optimum barely moves. The preprint (pp. 3–4) solves a rational linear system for each horizon, then filters requests so that only those missed by some strongly lazy service with bounded moves are retained, which bounds the retained word length; a marking fallback pays for trajectories exceeding the move cap. The constructor's running time is uncontrolled, so the algorithm simulates it for only steps at request (Proposition 4.2, p. 14), and the delayed activation is absorbed into .
RationalMetric n is a Fin n → Fin n → ℚ table with the metric axioms; configurations are Fin k → Fin n; offlineCost is the sInf over label histories matching the request word (a finite, nonempty set of costs).BitMachine has finitely many controls and tapes and a transition consuming one coin per step. Preprocessing (boot) runs steps with all coins , so it is deterministic; this is satisfied by the source's deterministic constructor, and Theorem 1.1 does not require randomness there.requestBudget c e L t steps (Nat.clog 2 (t+1)) and must have yielded with output value for every reachable state and every coin string; requests are encoded by a fixed self-delimiting binary code.machineExpectedCost averages over all coin strings of the step budget, i.e. uniformly random bits; the bound is required for every request list w, with chosen after and before w.In the -server problem, servers sit at points of a metric space; requests arrive one at a time, and each request must be served by moving some server onto it, at a cost equal to the distance travelled. An online policy sees only the requests revealed so far, and its quality is measured by its competitive ratio: how much more it moves, in expectation, than the offline optimum that knows the whole sequence. The problem was introduced as a common framework for paging, caching and other online service problems, and the question of the best ratio achievable by randomized policies has driven the development of metric embeddings, online primal-dual methods and entropic regularization.
This mission asks for a formal proof that randomized -server has competitive ratio on every metric space, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
Let be a metric space and the initial positions of labelled servers; repeated positions are allowed. To serve a request , a policy chooses one label and moves server to , leaving the others fixed (a server already at may be chosen at zero cost). For a finite request sequence , is the total distance moved and is the minimum of this cost over all label sequences, chosen with knowledge of . A randomized online policy chooses, at each step, a probability distribution over labels as a function of the past requests, its own past choices and the current request. Requests are fixed in advance, independently of the policy's randomness (the oblivious adversary).
There is an absolute constant such that for every , every metric space with at least points, and every , there are a randomized online policy and a finite with
for every finite request sequence . The same policy serves all sequences and horizons; may depend on , and but not on ; and when the entries of are distinct.
The result itself. Combined with the Bubeck–Coester–Rabani lower bound, it identifies as the worst-case order of the randomized competitive ratio over all metrics. The bound has no dependence on the number of points, the aspect ratio, finiteness or boundedness of , removing the factor left by static tree embeddings. No computational efficiency is claimed; a companion preprint turns the existence statement into a uniform algorithm on finite rational metrics.
Formalizing it. The statement is elementary to state, but its proof combines a rank-based allocation on separated trees, slowly varying simplex trackers, a compact potential for partition edits, online partitions with an embedded comparator, balanced rounding, and a compactness argument (Tychonoff) producing one policy for all finite inputs. None of these online-algorithm tools exist in a formal library, and a machine-checked competitive analysis of a randomized -server algorithm on general metrics is not known.
Embedding the metric into a random hierarchically separated tree and running an tree algorithm loses the embedding distortion, which is in the worst case and is not bounded in terms of . Removing it requires changing the tree as requests arrive, and the cost of re-partitioning must be paid for. A previous dynamic approach (Lee's fusible HSTs) had its general claim withdrawn after a gap in that accounting (p. 3). In the preprint, the partition schedule is driven by the posterior measure of a hidden comparator, and the edit costs and the travel of parked mass are bounded separately (Sections 7–8). Passing from finite metrics and finite horizons to one policy on an arbitrary, possibly infinite and unbounded, space with a fixed constant requires a further compactness step (Section 10).
X : Type u carries an arbitrary MetricSpace instance; "at least points" is an injection Fin (k+1) → X. No finiteness, separability or boundedness is assumed.Policy k X maps the history (list of past requests with the labels used) and the current request to a LabelDistribution k, i.e. a probability vector on Fin k. Every step moves exactly one server (Function.update), as in the source.expectedCost is the finite sum over all label sequences of the path probability times the service cost; optimalCost is the sInf over all label sequences of the service cost (nonempty finite set, so the infimum is a minimum). Restricting the offline optimum to one-server-per-request service does not change it (triangle inequality).Function.Injective s → B = 0 encodes the distinct-start clause.Real.log).The permanent of an matrix ,
has the same monomials as the determinant but no signs. The determinant can be computed in polynomial time; the permanent is #P-hard (Valiant, 1979). Valiant's algebraic theory makes this contrast precise: the determinant is complete for small formulas and branching programs, the permanent is complete for the class VNP, and VP ≠ VNP, the algebraic analogue of P ≠ NP, would follow if the permanent cannot be written as a determinant of polynomially larger size with affine-linear entries. Mulmuley and Sohoni's geometric complexity theory reformulates this through orbit closures, which leads to the border version of the question studied here.
Until this work the best lower bounds for both exact and border determinantal complexity of the permanent were quadratic. The source of this mission, an OpenAI preprint dated September 24, 2026, claims a cubic lower bound in the border model.
For a complex polynomial , the determinantal complexity is the least positive integer with
The border determinantal complexity is the least positive such that is a coefficientwise limit of such determinants of size (the size stays fixed along the sequence; the matrices are arbitrary). Clearly .
If , , , and the lowest nonzero homogeneous term of has degree and defines a smooth projective hypersurface, then
For every ,
The constants are those stated in the paper and are not optimized. The Lean statement OAI.PermanentBorder.permanent_cubic_lower_bounds is open on the platform.
The theorem raises the exponent of the best lower bound for the permanent versus determinant problem from (Mignon–Ressayre, Landsberg–Manivel–Ressayre) to , in the border model and hence also in the exact model. Through determinant reductions it also gives lower bounds on the size of affine-linear algebraic branching programs for the permanent. It remains a polynomial bound: superpolynomial determinantal complexity of the permanent, which would separate VP from VNP-type classes, is still open. The smooth-form bound of Corollary 9.3 applies to any polynomial with a smooth initial form, not only the permanent.
The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. Formalizing it would certify the polar-degree counting argument and the coefficient-projection construction that extracts a smooth form of linear degree and quadratic dimension from the permanent.
The Hessian method stops at the quadratic scale: the Hessian of an order- determinant has rank at most at a singular matrix, while the permanent's Hessian has rank at most , so it cannot give more than . Singular-locus methods give only linear bounds for the permanent because its singular locus has small codimension. A cubic bound needs an invariant that grows multiplicatively in degree and dimension, and in the border model it must survive limits, so any intersection count used must be shown to persist for a single sufficiently close determinant.
MvPolynomial σ ℂ; the permanent is permanentPolynomial m on variables Fin m × Fin m.affineMatrixPolynomial n A₀ A is with complex matrices.HasExactDeterminant n p: and equals such a determinant. HasBorderDeterminant n p: and sequences whose determinant polynomials converge to coefficient by coefficient. Instead of defining as a minimum, the goal states that every admissible size obeys the bound, which is equivalent.affineSubstitution a I g is , homogeneousComponent extracts , and smoothness is stated on the affine cone: the only common zero of and all its partial derivatives is .Real.exp 1 for .A complete development needs projective smoothness and polar intersections (Bézout-type counts with simple points), adjugate and kernel-line computations for determinant pencils, and dimension estimates for matrix fibers. Contributions formalizing Lemma 2.1 (affine substitution preserves the closure), Proposition 2.2 (equivalence of border models) or Theorem 2.3 are welcome.
Multiplying two matrices by the schoolbook method costs about operations. The matrix-multiplication exponent of a field is the infimum of exponents such that matrices over can be multiplied with additions, subtractions and multiplications. It governs the asymptotic cost of a central bilinear operation and of the many algorithms built from it (determinants, inversion, linear systems). Bounding has driven algebraic complexity theory since 1969. In recent years the bounds have moved in the third and fourth decimal place, with each improvement coming from a finer analysis of the same tensor-power framework.
Fix a field . An arithmetic program is a straight-line sequence of gates, each a constant from , an input entry, or the sum, difference or product of two earlier gates. Its cost counts the addition, subtraction and multiplication gates. A program multiplies matrices if designated registers equal the entries of for every pair of input matrices over . A real number is admissible if for every there is such that for every some correct program has cost at most , and
In Lean this is MatrixAllFields.MatrixMultiplication.Arithmetic.omega F, defined for every F : Type u with [Field F].
The Lean statement also contains the numerical comparison , which carries no mathematical content (the source writes the comparison as ). This is Theorem 1.1 of the source. The goal is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. If the source's argument and certificate are correct, the theorem lowers the best stated bound on from (Dupont et al.) to , and it does so uniformly over all fields, with exact algorithms in every positive characteristic. Any improvement in lowers the exponent of every algorithm reducible to matrix multiplication. The method — pooling directional capacities across extraction depths and staggering lots so that one lot sits at each splitting stage — shows that combination losses in the asymmetric framework can be traded across depths.
Formalizing it. Bounds of this type rest on long chains of tensor-power constructions, recovery arguments and large rational parameter tables, checked in the source by an accompanying verifier with interval certificates for logarithms. A machine-checked proof would certify the whole chain from the arithmetic model to the final rational inequality. It would also give Mathlib the asymptotic sum inequality and Coppersmith–Winograd machinery, which every future bound on needs.
Every recent improvement fights extraction losses. Restricting a tensor power to a direct sum of independent matrix products wastes variables whenever whole blocks must be disjoint, while the final products only need disjoint subsets. Prescribed marginals may also allow several joint distributions. Earlier analyses take the minimum of three directional capacities separately at each depth, so a shortage on one side at one depth is lost. Using capacity across depths requires that variables deleted in earlier extractions (to resolve conflicts or impose type conditions) can still be recovered exactly, over the original field and with only subexponentially many extra copies. Positive characteristic rules out arguments that divide by small integers or rely on characteristic-zero identities.
F : Type u, with free constants from and unit cost for add, sub and mul. This matches the source's "scalar additions and multiplications".AdmissibleExponent F τ asks, for each , for one constant that works for every . omega F is the sInf of the admissible set, which is nonempty (schoolbook algorithm) and bounded below by the output size, so a junk value cannot make the strict inequality true.A graph is three-colorable if its vertices can be colored with three colors so that adjacent vertices get different colors. Deciding three-colorability is NP-complete. The approximate coloring problem asks how much a promise helps: given a graph promised to be three-colorable, can one efficiently find a coloring with a few more colors, or at least a large independent set? Every three-colorable graph on vertices has an independent set of size (its largest color class). The best polynomial-time algorithms use colors, while hardness results long reached only small palettes and needed extra conjectures for stronger gaps. Problems of this kind are central test cases for the PCP theorem, Label Cover and the theory of promise constraint satisfaction.
A 3-CNF formula is a conjunction of clauses, each a disjunction of at most three literals (variables or their negations); it is satisfiable if some truth assignment makes every clause true. For a finite simple undirected graph with vertices, is the size of a largest independent set, a set of pairwise nonadjacent vertices. A polynomial-time reduction is a deterministic algorithm that, on an explicit binary encoding of its input, runs in time polynomial in the encoding length and outputs an explicit encoding (here the full adjacency matrix) of the output graph.
For every fixed real there is a deterministic polynomial-time algorithm mapping each explicitly encoded 3-CNF formula to a nonempty finite simple graph with
The running time and output size are polynomial in the binary length of , with constants depending only on . The goal statement is published on the platform with status Open.
The result itself. Theorem 1.1 shows that, even with the full promise of three-colorability, it is NP-hard to find an independent set of any fixed positive density. It implies hardness of distinguishing -colorable graphs from non--colorable graphs for all fixed (Corollary 1.2), the long-standing conjecture recorded by Barto–Bulín–Krokhin–Opršal. Unlike the routes through -to- games and arc graphs, it keeps the independent-set soundness together with three-colorable completeness, and unlike Dinur–Khot–Perkins–Safra it does not delete vertices. Earlier results with this combination were conditional (Dinur–Mossel–Regev; Braverman–Khot–Lifshitz–Minzer).
Formalizing it. The statement is fully explicit: Mathlib's TM2ComputableInPolyTime fixes the machine model, and the formula and graph encodings are spelled out bit by bit. A formal proof would require a machine-checked PCP theorem with perfect completeness (Label Cover), a dimension-independent junta approximation theorem, and the paper's alignment and list-decoding lemmas. Any of these is a substantial and reusable formalization project; complexity-theoretic reductions are barely represented in Mathlib today.
Gap reductions from Label Cover to coloring traditionally use long-code or dictatorship tests whose soundness analysis loses control either of three-colorability of every vertex (completeness) or of independent sets of arbitrarily small density (soundness). Known unconditional routes reach constant-palette coloring hardness only by composing reductions that lose the independent-set guarantee, and routes keeping it required unproven games conjectures with structural assumptions. The proof must decode a labeling from any independent set of density in a graph that is genuinely three-colorable on every vertex when is satisfiable, without bounds on projection-fiber sizes.
Graph records: vertices Fin n, a symmetric loopless Boolean adjacency. Independence number is the maximum card of an independent Finset; three-colorability is a proper map to Fin 3.RealGraphReduction δ packages a function reduce : List Bool → Graph with a Turing.TM2ComputableInPolyTime witness (identity input encoding, graphBits output encoding, finite stack alphabets), an explicit polynomial output-size bound, completeness and strict soundness on encoded formulas. The reduction must be total and polynomial-time on all bit strings, which is harmless since malformed inputs can be sent to a fixed graph.A projection game (label cover) asks for labels on the two sides of a bipartite multigraph so that, on each edge, the right label is the image of the left label under a prescribed map. In a 2-to-1 game the left alphabet has labels, the right alphabet , and every edge map has exactly two preimages of each right label. Khot introduced the 2-to-1 and Unique Games conjectures in 2002 (STOC 2002) as hypotheses that yield tight hardness of approximation. The 2-to-1 Games Conjecture with perfect completeness asserts that, for every fixed , it is NP-hard to tell satisfiable 2-to-1 games from games in which every labeling satisfies at most a fraction of edges. Perfect completeness matters for problems whose YES instances must be exactly satisfiable, such as graph coloring: hardness with completeness does not imply it.
This mission asks for a formal proof of the conjecture, as stated in an OpenAI preprint dated September 23, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
For an integer , a 2-to-1 instance has finite left and right vertex sets and a nonempty list of edge occurrences , where is given by an explicit table with for every . Parallel occurrences, possibly with different maps, are allowed and counted with multiplicity; there are no weights. A labeling assigns and and satisfies when . The value is the maximum, over labelings, of the fraction of satisfied occurrences. 3-SAT inputs are bit strings that decode to conjunctions of three-literal clauses (repetitions allowed); malformed inputs count as unsatisfiable.
For every fixed rational there are an integer and a deterministic polynomial-time reduction from 3-SAT to 2-to-1 instances with alphabets and such that
The running time is polynomial in the binary input length, with degree and constants depending only on .
The result itself. It removes the conditional hypothesis from perfect-completeness reductions. The preprint derives NP-hardness for maximum -colorable subgraph at soundness through Guruswami and Sinop's reduction (Corollary 1.2, p. 3), and recovers satisfiable Not-Two and three-query PCP hardness (Corollary 1.3, p. 4), the latter already known unconditionally by Håstad (SICOMP 2014). A companion preprint uses it for hardness of finding large independent sets in three-colorable graphs.
Formalizing it. No PCP-style hardness result of this strength has been machine-checked. A complete development needs a perfect-completeness PCP gap (Theorem 2.1, p. 5), projection-game parallel repetition (Theorem 2.2, p. 6), the Grassmann expansion theorem (Theorem 2.3, p. 7) and inverse shortcode estimates (Theorem 2.6, p. 9), on top of a polynomial-time Turing-machine framework. These components are shared with the Unique Games formalization and would be reusable.
Near-perfect completeness does not give perfect completeness: the reductions need not produce any finite satisfiable game. Amplifying a constant-soundness perfect-completeness game by parallel repetition destroys the 2-to-1 structure, since -fold repetition gives preimages per right label. The preprint therefore builds a new tree-structured construction (Section 3) whose joint-partition questions keep two-element fibers and satisfy exact identities, and the soundness analysis must decode labelings through a rank test whose tested rows depend on the decoded form itself (Sections 5–6), before projection-game repetition gives the contradiction (Section 7).
ProjectionTable q is a Vector (Fin q) (2*q) with exactly two preimages of every b : Fin q. Instance q lists edges as a List with a nonemptiness proof, so value = maxSatisfied / edges.length never divides by zero; maxSatisfied is a Finset.sup over all labelings.BinaryGapReduction δ fixes alphabet ≥ 2, a construct map, a Turing.TM2ComputableInPolyTime witness from raw input bits (identity encoding) to the explicit bit encoding gameBits, finite tape alphabets, completeness value = 1 on encodings of satisfiable formulas, and soundness value ≤ δ on all other inputs.value = 1 requires a labeling satisfying every edge.A directed feedback vertex set of a finite digraph is a set of vertices meeting every directed cycle, equivalently one whose removal leaves acyclic; is the minimum size of such a set. The problem arises wherever cyclic dependencies must be broken — deadlock resolution, circuit testing, scheduling — and a topological order of certifies a solution in polynomial time.
The best general approximation guarantee is , originating in Seymour's work on fractional packing of directed circuits (Combinatorica 1995) and made constructive by Even, Naor, Schieber and Sudan (Algorithmica 1998). On the hardness side, NP-hardness was known only for particular constants (via Vertex Cover), while ruling out every constant factor required the Unique Games Conjecture. Whether a constant-factor approximation exists under P ≠ NP alone was open.
This mission asks for a machine-checked proof that approximating DFVS within any fixed factor is NP-hard on unweighted digraphs, as claimed in an OpenAI preprint dated September 23, 2026 (source, Theorem 1.1, p. 2). The preprint has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal is open.
A digraph is finite and loopless, given by a vertex count and a duplicate-free list of arcs with ; opposite arcs are allowed. A directed cycle is a cyclic sequence of distinct vertices with every successive arc present, including the closing one. is a feedback set if it meets every directed cycle, and is the least size of one.
A language is in NP if there are a polynomial and a deterministic polynomial-time verifier (a multi-stack Turing machine with finite alphabets) with iff some certificate with makes accept.
For every real and every language there is a deterministic polynomial-time map with such that
In Lean this is OAI.DirectedFeedback.main : DirectedFeedback.MainStatement. The preprint states Theorem 1.1 as a reduction from an NP-hard promise problem (the 2-to-1 game gap of Theorem 2.1, p. 5) to ; composing with that promise problem's NP-hardness gives the Lean form, which quantifies over all NP languages directly. A deterministic polynomial-time -approximation would then decide every NP language (proof of Theorem 1.1, p. 28).
The preprint also proves Corollary 8.3 (p. 28) for directed feedback arc set; it is not formalized on the platform.
The result itself. Theorem 1.1 shows that a constant-factor approximation for DFVS exists if and only if P = NP, removing the Unique Games hypothesis from the Guruswami–Manokaran–Raghavendra and Svensson results. It does not determine the true growth of the optimal factor between constants and .
Formalizing it. No machine-checked inapproximability result of this kind is known to exist. A complete development needs the 2-to-1 Games Theorem with imperfect completeness (Theorem 2.1, p. 5, external input), Friedgut's junta theorem in a dyadic fixed-bias form (Theorem 2.2 and Corollary 2.3, p. 6), finite Ramsey theory and von Neumann's minimax theorem, and the preprint's rank-graph construction (Definition 3.1, p. 8; Proposition 3.7, p. 12), pivotality budget (Definition 6.1, p. 20) and weighted soundness (Proposition 7.4, p. 25). An NP and Karp-reduction library on TM2 machines (including Cook–Levin) would be reusable across the whole family of hardness missions.
The central difficulty (Introduction, pp. 3–4) is extracting a game labeling from an arbitrary acyclic remainder: a topological order exists, but it can interleave the many vertices representing one local test arbitrarily. Comparisons in that order must first be made consistent and then read as Boolean functions; Friedgut-type junta bounds must hold at many biases simultaneously for the same random function, so a separate influence bound at each scale does not suffice. The coordinate lists must also be fixed before the tested game edge is drawn, or they do not define a game labeling. Gadget reductions from Vertex Cover cannot go beyond the Vertex Cover constants.
DirectedFeedback.Digraph: n : ℕ, a Nodup list of arcs in Fin n × Fin n, loopless; cycles are injective maps Fin (r+1) → Fin n with all successive arcs (including the wrap-around) present, so 2-cycles count and 1-cycles cannot occur. dfvs is the least cardinality of a feedback Finset.NPVerifier: a polynomial certificate bound and a polynomial-time TM2 verifier with finite alphabets on the unary-framed pair encoding pairBits; no SAT-specific definition is used.GapReduction A L is a polynomial-time TM2 machine (finite alphabets, raw-bit input) producing a GapInstance (digraph plus k > 0), encoded explicitly in unary-framed form by GapInstance.bits; completeness and soundness are as displayed, with soundness compared in ℝ.TM2 verifiers plus the 2-to-1 Games reduction.k > 0 and the strict inequality rule out a trivial reading (e.g. empty graphs with k = 0).Welcome contributions: Friedgut's junta theorem, finite Ramsey and minimax in usable forms, the 2-to-1 Games Theorem, and Cook–Levin for Turing.TM2ComputableInPolyTime.
Min-UnCut asks, for a finite simple graph , for the minimum number of edges whose deletion makes bipartite. Equivalently, for a bipartition let count the edges with both endpoints on the same side, and set . The quantity measures distance from bipartiteness. Although it equals minus the maximum cut, a good multiplicative approximation for Max-Cut gives nothing multiplicative for Min-UnCut on nearly bipartite graphs, which is exactly the regime of interest.
The best known algorithm (Agarwal, Charikar, Makarychev, Makarychev, STOC 2005) achieves an factor. Before the source preprint, NP-hardness was known only for specific constant factors below about , and hardness for every constant factor was known only under the Unique Games Conjecture.
This mission asks for a machine-checked proof that Min-UnCut has no polynomial-time approximation within any constant factor unless P = NP, as claimed in an OpenAI preprint dated September 23, 2026 (source, Theorem 1.1, p. 2). The preprint has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal is open.
A graph is finite, simple, undirected and unweighted, given by a vertex count and a symmetric loopless Boolean adjacency table. A cut is a map ; the parts may be empty or unbalanced. counts unordered edges with , and is its minimum over all cuts.
3SAT formulas are conjunctions of three-slot clauses over natural-number variable names (repeated variables allowed), given to the reduction by a canonical prefix-free binary encoding.
For every fixed integer there is a deterministic polynomial-time reduction to an explicit simple graph and a binary integer with
with graph size and running time polynomial in the bit length of for each fixed . Choosing shows that a deterministic polynomial-time -approximation for any real would imply P = NP. The positive threshold is what separates this from bipartiteness testing. In Lean this is OAI.MinUncut.main : Nonempty MinUncut.Reduction.
The preprint also derives Corollary 1.2 (p. 3): minimum 2CNF clause deletion is NP-hard to approximate within every fixed factor . It is not formalized on the platform.
The result itself. Theorem 1.1 settles the constant-factor approximability of Min-UnCut in the hardness direction without the Unique Games Conjecture, and by an exact cost-preserving transformation the same holds for Min 2CNF Deletion. Together with the algorithm, it places these problems strictly between constant-factor approximable and inapproximable within logarithmic factors (the remaining gap concerns super-constant factors).
Formalizing it. No machine-checked proof of super-constant-type inapproximability for any natural graph problem is known to exist. A complete development needs Håstad's parity gap (Theorem 2.2, p. 6) and uniform parallel repetition (Theorem 2.3, p. 7), used as external inputs, plus the preprint's inner decoding theorem (Theorem 3.2, p. 9), the composition gap for bit comparisons (Proposition 6.1, p. 27) and the finite constructions (Lemmas 7.1 and 7.2, pp. 31 and 34). PCP and parallel-repetition infrastructure would be reusable across many hardness missions.
A natural route is to compose a long-code test with a projection game, as in Håstad's work. The obstacle is extracting a label from an arbitrary folded bit proof with a probability and coefficient size independent of the label alphabet: the alphabet grows as the outer soundness is driven down, and every inner constant must be fixed before it (Introduction, pp. 3–4). In addition, the decoder's choices depend on shared background affine functions, so the outer game's soundness must survive such shared hints. Gadget-based approaches yield only isolated constants (up to about ); unbounded constants previously required the Unique Games hypothesis.
MinUncut.Output packages the graph (vertex count, symmetric loopless Bool adjacency) with a threshold threshold ≥ 1; uncut counts pairs u < v that are adjacent and on the same side, and opt is the minimum over all Fin N → Bool cuts (nonempty, so always defined).MinUncut.Reduction is a single TM2 machine taking the pair (encoded by inputBits) with finite tape alphabets, a polynomial time K bounding the running time in the formula's bit length, and a polynomial size K bounding vertices plus output length; yes/no hold for every K ≥ 2.formulaBits φ, the canonical encoding including variable names.Welcome contributions: Fourier and Gaussian analysis on -affine spaces, the long code with folding, parallel repetition for projection games, and Turing-machine complexity infrastructure.
A vertex cover of a graph is a set of vertices meeting every edge; denotes the minimum size of one. Computing exactly is NP-hard, but a two-line algorithm — take both endpoints of a maximal matching — always returns a cover of size at most . Whether any polynomial-time algorithm achieves a fixed factor is one of the best-known questions in approximation algorithms. Unconditional NP-hardness was known below and, after the 2-to-2 Games Theorem, below ; factor-two hardness was known only under Khot's Unique Games Conjecture.
This mission asks for a machine-checked proof that every fixed approximation factor below two is NP-hard, as claimed in an OpenAI preprint dated September 23, 2026 (source, Corollary 1.2, p. 1). The preprint's direct reduction starts from ordinary perfect-completeness Label Cover. It has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal is open.
A graph is finite, simple, undirected and unweighted, given explicitly by its vertex count and a duplicate-free list of edges with . A set of vertices is a cover if every edge has an endpoint in , and is the least size of a cover. An -approximation algorithm is a deterministic polynomial-time machine that, on every graph, outputs a duplicate-free list of vertices that covers all edges and has length at most .
3SAT inputs are bit strings decoding canonically to a conjunction of three-slot clauses; malformed strings are NO instances. A 3SAT decider is a deterministic polynomial-time machine answering membership correctly on every input.
For every integer there is a deterministic polynomial-time reduction from 3SAT to explicit simple graphs with
The ratio of the thresholds is . In Lean: OAI.VertexCover.explicit_cover_gap.
For every real with , an -approximation algorithm for Vertex Cover yields a polynomial-time 3SAT decider:
In Lean: OAI.VertexCover.every_fixed_factor_below_two. The preprint derives it from Theorem 1.1 in its final section (pp. 23–24) by choosing from and comparing the returned cover with an exact rational threshold. Together with the matching algorithm, it identifies as the approximation threshold unless P = NP.
The result itself. The statement removes the Unique Games hypothesis from the Khot–Regev theorem and closes the gap between the elementary factor- algorithm and hardness. The density gap of Theorem 1.1 is also a statement about independent sets: YES graphs have independent sets of density nearly , NO graphs have none of density above .
Formalizing it. No machine-checked proof of any super-constant Vertex Cover hardness bound is known to exist. A complete development requires the perfect-completeness Label Cover theorem (Theorem 2.1, p. 4; PCP theorem plus parallel repetition, used as an external input), the explicit graph construction and its polynomial-time implementation (Proposition 3.3, p. 7), and the preprint's analytic soundness argument. The Label Cover input and a library for polynomial-time gap reductions on TM2 machines are reusable for many other hardness missions.
Soundness requires extracting short lists of candidate labels from an arbitrary large independent set, where each list may depend only on its own position's query. If a list also sees the opposite endpoint of a constraint or its occurrence index, the pair-decoding argument against Label Cover soundness breaks down (Introduction, pp. 3–4). Classical approaches either need the stronger Unique Games source promise (Khot–Regev) or only reach densities near (the 2-to-2 route), which gives factor rather than . Averaging to impose the information restriction can erase all variance; the analytic core is retaining it without any dependence on the label alphabet sizes.
VertexCover.ExplicitGraph: n : ℕ and a Nodup list of pairs in Fin n × Fin n with e.1 < e.2; coverNumber is the least cardinality of a covering Finset (always defined since univ covers).ExplicitGraph.bits (vertex count, all vertex names, edge count, edge endpoints, each with prefix-free binary framing); an approximation's output list is encoded by natListBits.Approximation α bundles a polynomial-time TM2 program on graph encodings with finite tape alphabets, whose output is duplicate-free, in range, covers every edge and has length at most α * coverNumber. ThreeSATDecision is a polynomial-time TM2 decider correct on every input.Approximation α must be correct on every graph.ℝ with strict inequalities as in the source.Welcome contributions: Label Cover hardness (PCP theorem + parallel repetition), Efron–Stein decompositions and variance inequalities on product spaces, and general complexity-theoretic infrastructure for Turing.TM2ComputableInPolyTime.
Max-Cut asks for a partition of the vertices of a graph that maximizes the number of edges crossing it. Its decision version is one of Karp's original NP-complete problems, so the natural question is how well it can be approximated in polynomial time. Goemans and Williamson's semidefinite-programming algorithm with random-hyperplane rounding achieves ratio approaching
(GW 1995). Whether any polynomial-time algorithm can beat this constant is a central question of approximation algorithms: unconditional NP-hardness was known only above , and optimality of was known only under Khot's Unique Games Conjecture.
This mission asks for a machine-checked proof that approximating Max-Cut within any fixed ratio is NP-hard, even on simple unweighted graphs, as claimed in an OpenAI preprint dated September 23, 2026 (source, Theorem 1.1, p. 1). The preprint gives a direct reduction from the 2-to-1 Games Theorem, not via the Unique Games Conjecture. It has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal is open.
A simple unweighted graph on vertices is given by a symmetric, loopless Boolean adjacency table. A cut is a map from the vertices to ; its size is the number of unordered edges with , and is the largest cut size. An algorithm is an -approximation if it always returns a cut of size at least .
3SAT inputs are bit strings decoding canonically to a conjunction of three-slot clauses (repeated variables and literals allowed); malformed strings are NO instances. A gap reduction for consists of rationals and with , and a deterministic polynomial-time map outputting a graph together with a positive integer scale such that
Given such a reduction, an -approximation algorithm would decide 3SAT by comparing its output with .
For every real with , a gap reduction for from 3SAT to simple unweighted Max-Cut exists:
In Lean this is OAI.OptimalMaxCut.main : OptimalMaxCut.MainStatement. The preprint proves it from a sharper weighted gap (Theorem 1.2, p. 2): for rational , and , it is NP-hard to distinguish from on graphs with a rational edge distribution; Appendix B (p. 35) converts weighted graphs to simple unweighted ones.
The result itself. Theorem 1.1 shows that the Goemans–Williamson algorithm is optimal among polynomial-time algorithms unless P = NP, removing the Unique Games hypothesis from the result of Khot, Kindler, Mossel and O'Donnell. It is the most prominent instance of an SDP-tight threshold, and the gap form (Theorem 1.2) gives a whole curve of completeness/soundness pairs.
Formalizing it. No machine-checked proof of any optimal inapproximability result for Max-Cut exists. A full development requires the 2-to-1 Games Theorem in the affine form stated as Proposition 2.2 (p. 6) and derived in Appendix A, the Majority Is Stablest theorem (Lemma 2.1, p. 5), and the paper's new ingredients: tree-code Fourier analysis (Section 5), a vector-valued affine hashing lemma (Lemma 6.1, p. 14), dimension-independent extraction (Proposition 7.1, p. 18) and decoding (Proposition 8.4, p. 24). Several of these — Majority Is Stablest, Boolean Fourier analysis, polynomial-time gap reductions on Turing machines — are reusable libraries in their own right.
The classical long-code test for Max-Cut, analysed via Majority Is Stablest, identifies an influential coordinate of an arbitrary cut. Under the Unique Games Conjecture that coordinate is directly a label of the source game. Starting instead from 2-to-1 games, the influential coordinate is indexed by a gate input of the test, not by a source-game label, and the two endpoints of a source edge cannot in general reconstruct a common context without knowing their projection. The decoding loss must also be independent of the source alphabet, because the alphabet dimension is chosen after the target soundness; a dimension-dependent loss would make the parameter choice circular (Introduction, pp. 3–4).
OptimalMaxCut.Graph: a vertex count with a symmetric loopless Bool adjacency function; maxCut maximizes cutSize over all Fin n → Bool, counting each unordered crossing edge once.ScaledGraph with an explicit positive integer scale; the YES/NO bounds compare maxCut / scale in ℝ, and 0 < scale rules out division by zero.alphaGW is defined as the sInf of over ; this set is nonempty and bounded below, so the infimum is the true constant.Turing.TM2ComputableInPolyTime machine with finite tape alphabets, from raw input bits (identity encoding) to ScaledGraph.bits (delimited vertex count and scale, then the full adjacency table); the rational bounds and the machine are fixed before the input.noBound < α * yesBound with 0 < yesBound, so there is no trivial reading. No assumption P ≠ NP is built in.Welcome contributions: Boolean and Gaussian Fourier analysis (noise stability, influences, Borell's theorem), Majority Is Stablest, the 2-to-1 Games Theorem, and a reusable library for polynomial-time gap reductions on TM2 machines.
A Unique Game is a system of constraints between pairs of variables, each constraint saying that the label of one endpoint is a fixed permutation of the label of the other. Deciding whether all constraints can be satisfied is easy (propagate labels along a spanning tree), so the interesting question is approximate: given an instance in which almost all constraints can be satisfied, can a polynomial-time algorithm find a labeling that satisfies even a small fraction?
Khot's Unique Games Conjecture (UGC, 2002) asserts that it cannot, unless P = NP. The conjecture matters because many optimal approximation thresholds have been proved conditionally on it: the Goemans–Williamson ratio for Max-Cut (KKMO 2007), the factor for Vertex Cover (Khot–Regev 2008), the basic-SDP threshold for every constraint satisfaction problem (Raghavendra 2008), and hardness for ordering, multicut/sparsest-cut and correlation-clustering problems. An unconditional proof would turn all of these into NP-hardness results.
This mission asks for a machine-checked proof of the Unique Games Theorem as stated in an OpenAI preprint dated September 23, 2026 (source), which claims a positive resolution of the conjecture. The preprint has not been peer reviewed, and its claim has not been independently verified; on the platform the Lean goal below is open.
Fix a finite alphabet . An instance has a finite vertex set and a nonempty list of oriented constraints with a permutation of ; repeated list entries count with multiplicity, and no weights are allowed. A labeling assigns a label to every vertex and satisfies when . The value of is the fraction of satisfied constraints and is the maximum over labelings.
An instance is simple bipartite if its vertices split into two sides, every constraint goes from the first side to the second, and no two list entries join the same ordered pair. It is a translation instance over if every constraint has the form .
3SAT inputs are bit strings decoding to a conjunction of clauses with exactly three literal slots (repeated variables and literals allowed); the input is a YES instance when it decodes to a satisfiable formula.
For every there exist and a deterministic polynomial-time map to simple bipartite translation instances over such that
The alphabet, the program and the running-time polynomial depend only on ; the two errors are chosen independently, before the alphabet. In Lean this is OAI.UniqueGamesTheorem.theorem11, which asserts that the structure BinaryGapReduction ε δ is inhabited.
The result itself. The conjecture is the hypothesis behind a large body of tight approximation thresholds; the preprint's Section 8 (pp. 39–43) records how Theorem 1.1 feeds the earlier reductions for Max-Cut, Vertex Cover, Raghavendra's CSP theorem, ordering CSPs, multicut/sparsest cut and correlation clustering. Those reductions and thresholds are due to their original authors. The statement also fixes the conjecture's quantifier order (errors first, then alphabet), which is exactly what the known algorithms above do not contradict.
Formalizing it. No machine-checked proof of the UGC, or of the 2-to-2 theorem it builds on, is known to exist. A complete development would have to formalize Håstad's parity gap, classical parallel repetition for projection games, the Khot–Minzer–Safra Grassmann/shortcode inverse theorem (used as an external input via Theorem 5.1, p. 22 of the preprint), and the preprint's new latent-alphabet gadget and matrix test. Each of these is reusable well beyond this mission.
The central obstacle, identified in the preprint's introduction (pp. 2–4), is completeness: in a unique constraint every label permits exactly one reply, so the natural codeword tests lose a constant fraction of constraints even on honest proofs. For example, on the rank-one matrix shortcode the evaluation is preserved by a random rank-one update only with probability about . The 2-to-2 theorem gives soundness but only near- completeness, and pushing completeness to while keeping soundness independent of the alphabet is a separate problem that the earlier programme left open.
Foundations.Target.Instance q over alphabet Fin q, with constraints given by explicit forward/inverse permutation tables and a nonemptiness proof; the value is countSatisfied / constraints.length in ℝ, so division by zero cannot occur.Turing.TM2ComputableInPolyTime program from raw input bits (identity encoding, so runtime is measured in the raw input length including sparse variable names) to the bit encoding gameBits; its tape alphabets must be finite.coordinates : Fin alphabet ≃ (Fin s → ZMod 2) fixes the structure, and translations requires every constraint to be a translation in these coordinates; simpleBipartite gives the orientation and the no-parallel-edge condition on list positions.BinaryLanguage.language: inputs that decode (canonically) to a satisfiable three-slot formula. Malformed inputs are NO instances and must be mapped to low-value games.Welcome contributions: a reusable Lean library for PCP-style gap reductions on TM2 machines, Fourier analysis over , parallel repetition for projection games, and the Grassmann expansion theorem.
Edit distance , the least number of single-symbol insertions, deletions and substitutions turning into , is the standard distance on strings. Embedding strings into with small distortion would make edit distance amenable to the fast nearest-neighbour and sketching tools available for , so the least achievable distortion is a central quantity in metric embedding theory. A single insertion shifts every later symbol, yet cyclically shifting a word costs only two edits; this tension between position and alignment is what makes edit distance hard to embed.
This preprint gives two independent constructions of binary word sets whose least distortion is , two binary coding arguments that transfer large-alphabet constructions to binary, and a complete histogram embedding attaining the matching upper scale. Together they determine the exponential scale of the distortion.
For a finite alphabet with and an integer , let be the words of length at most , including the empty word. For an injective ,
The longest common subsequence and the deficit for words of length are used in the coding results. A binary substitution replaces each letter by a codeword.
In Lean (OAI.FiniteCircle), editDistance is the least script length, lcs and deficit are as above, optimalDistortion is the infimum of distortion over injective maps into lp (fun _ : ℕ => ℝ) 1, E α d is the least distortion of words of length at most , and maskWord, excludedWord are the two finite-circle constructions with prime-period parameters.
finiteCircle_fullMainThe conjunction of the paper's main statements, with common absolute constants:
and the same bounds for .
The result. The lower bounds reach the Ostrovsky–Rabani scale, so the order of is ; this improves the previous lower bound to . The histogram embedding gives an explicit, alphabet-uniform upper bound including all shorter words.
Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. Unlike the companion paper, the upper bound here is proved in full (Section 8) rather than imported, so the goal is self-contained relative to the preprint. The edit-distance and distortion definitions are reusable across the edit-distance missions.
Lower bounds for edit distance must control every increasing matching of the two words, including matchings crossing the row boundaries used to construct them. A cheap translation of phases moves row lists at low edit cost, while a simultaneous half-turn at every leaf must be expensive; proving the latter for arbitrary alignments, and then showing that every image must distort one of these comparisons, requires combining a combinatorial separation estimate with a Fourier argument on the finite phase space that forces large total frequency.
List α with Fintype α; the domain is a subtype by length; the empty word is included.distortion uses sSup over finite sets of ratios; optimalDistortion is sInf over injective maps into ; exponentScale d = sqrt(log d · log log d) with natural logarithms.MaskPrimes, ExcludedPrimes, depth parameters) and require a common positive length .UniformUpper asks for a map into Fin M → ℝ with the norm written as a finite sum.The goal is not vacuous: a set with one element would have least distortion , so witnesses must be nontrivial, and both bounds are required uniformly.
Needed infrastructure: LCS and alignment combinatorics, cut decompositions of finite metrics, Fourier analysis on finite cyclic groups, prime counting estimates, and random partition arguments for the upper bound. Contributions toward any component are welcome.
Edit distance is the least number of single-symbol insertions, deletions and substitutions transforming a string into . It is the basic similarity measure for strings, but it is expensive to compute and awkward to index. A standard way around this is to embed strings into so that distances approximate edit distances; the quality of such a map is its distortion. Low-distortion embeddings give fast approximate nearest-neighbour search and sketching for edit distance, so the best possible distortion has been studied for two decades.
This preprint determines the exponential scale of the optimal distortion: for strings of length at most , it is , uniformly over finite alphabets.
For a finite alphabet and , let be the set of strings of length at most , including the empty string. Edit scripts may pass through strings of any length. Let be the space of absolutely summable real sequences. Define
the infimum over injective maps with no restriction on dimension or computability.
In Lean (OAI.EditDistortion), edit x y is the least length of a Script true n x y of unit insertions, deletions and substitutions on List Alpha; L1 = lp (fun _ : ℕ => ℝ) 1; distortion ρ f is the product of the two maximal ratios for an embedding f : X ↪ L1; leastDistortion is the infimum over embeddings; E Alpha d applies this to {x : List Alpha // x.length ≤ d}; exponentScale c d = exp(c·sqrt(log d · log log d)).
There are absolute and such that for every and every finite alphabet with ,
The lower bound is witnessed by a finite set of binary strings of one common length at most , and the same two bounds hold for .
The result. Theorem 1.1 shows that the Ostrovsky–Rabani embedding is optimal up to the constant in the exponent, closing the gap between (Krauthgamer–Rabani) and . It rules out any embedding of edit distance with distortion , which limits -based approaches to approximate edit-distance search.
Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. The upper bound relies on Ostrovsky and Rabani's fixed-length theorem (Theorem 5.1 in the preprint, taken from the literature) plus reductions proved in the preprint, so a full formalization also requires formalizing the Ostrovsky–Rabani embedding. The lower bound (Sections 2–4) is the new contribution.
Any lower bound must control every alignment of two strings, including matchings that cross the boundaries of the blocks used to build them, because an insertion or deletion shifts an entire suffix. Earlier Fourier-analytic arguments (Khot–Naor) and recursive constructions (Krauthgamer–Rabani) lose too much to reach the exponent; reaching it requires a construction whose combinatorial separation and an displacement inequality match at that scale.
List Alpha with Fintype Alpha, 2 ≤ card Alpha; the domain includes the empty string and all lengths up to .edit is an sInf over script lengths, which is attained since scripts always exist.distortion uses sSup over finitely many ratios (the domain is finite), so no default values arise; leastDistortion is sInf over all injective maps into .BinaryWitness c d asks for a finite nonempty set of Boolean lists of common length whose least distortion is at least exponentScale c d; a singleton has least distortion , so the witness must be nontrivial.The statement cannot be met trivially: both bounds are required with constants uniform in the alphabet.
Needed infrastructure: cut decompositions of finite metrics, Fourier analysis on finite abelian groups, prime-number estimates (Rosser–Schoenfeld), and the Ostrovsky–Rabani construction. Contributions toward the displacement inequality (Proposition 2.2) or the recursive construction (Proposition 3.1) are welcome.
A metric space is doubling if every ball can be covered by a bounded number of balls of half the radius. Every subset of a finite-dimensional Euclidean space is doubling, so doubling is a necessary condition for a metric space to embed bi-Lipschitzly into some . Whether it is also sufficient, for subsets of Hilbert space, is the Lang–Plaut problem. It sits at the meeting point of metric geometry and algorithm design: doubling is a standard notion of "intrinsic dimension" for data, and a positive answer would mean that intrinsically low-dimensional Euclidean data can always be represented in a bounded number of coordinates with bounded distortion.
The Hilbert case () remained open. The source of this mission, an OpenAI preprint dated September 25, 2026, claims a negative answer.
A metric space is doubling with constant at most if for every and , the ball of radius about is covered by at most balls of radius with centers in . A map is a bi-Lipschitz embedding with distortion at most if some scale satisfies
Real is the Hilbert space of square-summable real sequences indexed by ; subsets carry the induced distance.
There is a universal such that every infinite-dimensional real Banach space contains a compact set with doubling constant at most that admits no bi-Lipschitz embedding into any finite-dimensional real normed space at any finite distortion.
The set is fixed once, independently of and of the distortion. The Lean statement OAI.DoublingHilbert.main is open on the platform. The constant comes from the paper's covering count; any finite universal constant would answer the Lang–Plaut problem, but the Lean goal records the paper's value.
The theorem answers the Lang–Plaut problem negatively: there is no function of the doubling constant alone that bounds both the dimension and the distortion for doubling subsets of Hilbert space. It extends the Lafforgue–Naor and Bartal–Gottlieb–Neiman obstructions from to the Hilbert case, which is the case of most interest for applications. By Gaussian isometric embedding the same metric space sits in every , (Corollary 5), and by Dvoretzky's theorem a compact version sits in every infinite-dimensional Banach space (Corollary 6). Assouad's theorem shows that any snowflake of the set does embed, so the obstruction is specific to the original distance.
The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. A previous announced proof of this statement (Schioppa, 2017) was withdrawn, which makes an independent formal verification particularly informative.
Doubling gives covering control at every scale, and Assouad's theorem shows that any loss in the exponent of the metric removes the obstruction, so a counterexample must be sharp at the level of exact Lipschitz bounds. The constructions rely on uniform convexity estimates of that degenerate at , and Hilbert space has the most symmetric geometry available, so the standard Laakso and diamond-type obstructions do not transfer. The set must also be chosen before the target dimension and distortion, so a single set has to defeat every and every simultaneously.
RealL2 := lp (fun _ : ℕ => ℝ) 2; is a Set RealL2 with the subspace metric.DoublingAtMost S bound: for each and there is a Finset of at most bound centers in such that every with satisfies for some center (open balls; centers in ).AdmitsBiLipschitzEmbedding S k: there are EuclideanSpace ℝ (Fin k), and with the two-sided bound above.CompactBanach.main quantifies over all complete real normed spaces that are not finite-dimensional and all finite-dimensional real normed targets, with the doubling constant chosen before .A complete development needs Hilbert direct sums, the explicit strip-colored set, covering estimates, a.e. differentiability of Lipschitz maps on open subsets of (Rademacher), and a Euclidean packing bound. Rademacher's theorem and packing estimates are reusable well beyond this mission. Contributions formalizing Proposition 2 (the doubling bound) are a natural first step.
Given vectors in the Euclidean unit ball of that sum to zero, can they always be reordered so that every partial sum stays in a ball whose radius depends only on ? Steinitz's lemma, from his work on rearrangements of conditionally convergent vector series, says yes: in any norm, radius suffices (Grinberg–Sevast'yanov 1980). For the Euclidean norm, the expected answer is , the Euclidean Steinitz–Bergström conjecture. A closely related prefix discrepancy problem asks for signs , chosen once and for all, such that every signed prefix is , independently of . Both questions are basic in discrepancy theory and combinatorial vector balancing, with applications to scheduling, rounding and the analysis of online and streaming algorithms.
Work in Euclidean space with norm , and let satisfy ; repetitions and zero vectors are allowed. A prefix sum is for (the empty sum is ). For a zero-sum family, the Steinitz quantity
is the best achievable maximal prefix norm over all orderings. The Euclidean Steinitz constant is its supremum over all such families.
There is an absolute constant such that for all and all with :
The constant is not fixed. The simplex example in the source shows , so the order is optimal. The goal statement is published on the platform with status Open.
The result itself. Theorem 1.2 settles the Euclidean Steinitz–Bergström conjecture: . Theorem 1.1 settles the prefix-discrepancy question of Bansal et al., removing the term in Banaszczyk's bound. A single choice of signs controls all prefixes at once, unlike terminal balancing results that bound one sum. The source also derives finite-dimensional Steinitz bounds and a colorful Steinitz theorem (Corollaries 8.1–8.2). The result is existential and gives no efficient algorithm.
Formalizing it. The statement is finite and elementary. The deduction of Theorem 1.2 from Theorem 1.1 is a short transference argument (Section 1.1 of the source), suitable as a first formalization step. The proof of Theorem 1.1 uses Gaussian measures of convex bodies, Dirichlet energies, Steiner symmetrization and Brownian survival estimates, which would make substantial reusable additions to Mathlib's probability and convex-geometry libraries.
Signing each prefix separately is easy, by terminal balancing results, but one common signing must work for all prefixes. Union bounds over prefixes and Banaszczyk's Gaussian-measure method lose a factor, because the probability that a random walk stays in a ball of radius for steps decays with . The proof must therefore control a single body of coefficients enforcing all prefix constraints, with bounds independent of the number of steps.
EuclideanSpace ℝ (Fin d), indexed by Fin N, with and .SignedPrefixBound C asks for signs (as reals) with every signed prefix at most . OrderingPrefixBound C asks, for zero-sum families, for a permutation with every reordered prefix at most . The goal is ; the same constant serves both, as stated in the source.Split Euclidean space into finitely many measurable cells and record, for each cell, its Gaussian first moment, the integral of against the standard Gaussian measure over that cell. How large can the sum of the squared lengths of these vectors be? The propeller conjecture predicts that, with at least three cells in dimension at least two, the answer is , attained by three planar sectors of angle (a "propeller") times the orthogonal complement. The question arose in Khot and Naor's work on approximate kernel clustering (Mathematika 2009), where this Gaussian partition parameter determines both the approximation ratio of Gaussian rounding and the matching Unique-Games hardness threshold. The surprise is that more cells or more dimensions do not help: the optimum uses only three cells in a plane.
This mission asks for a formal proof of the propeller bound in every dimension, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
Let be the standard Gaussian probability measure on , with density . For a measurable set , its centroid is the unnormalized vector
A measurable partition of consists of measurable sets such that almost every point (for ) lies in exactly one of them; empty cells and arbitrary cell probabilities are allowed. Its value is . The propeller is the partition of , , into the three sets , where are the planar sectors of opening bounded by the rays at angles and , with any further cells empty.
For all positive integers and every measurable partition of ,
and for , the propeller is a measurable partition attaining equality.
The result itself. It settles the propeller conjecture in all dimensions and for all numbers of cells, without constraints on cell masses. Through Khot and Naor's analysis, the constant fixes the loss factor of Gaussian rounding for identity-target kernel clustering; combined with the companion Unique Games preprint, the preprint deduces NP-hardness of any better fixed loss factor (Theorem 6.1, p. 18). The bound also gives a sharp inequality for expected Gaussian maxima (Corollary 5.1, p. 17).
Formalizing it. A formal proof needs Gaussian measures on Euclidean space (available in Mathlib as stdGaussian), a compactness argument for extremal partitions, the convex case of the Ehrhard inequality, and the three-dimensional theorem of Heilman, Jagannath and Naor, which the preprint uses as an established input and which itself relies on a finite computer verification. Each of these is a reusable component; the three-dimensional case alone would be a substantial formalization.
The optimization runs over all measurable partitions, with both shapes and probabilities free. Khot and Naor's reduction gives conical extremizers whose nonzero centroids span an -dimensional space, so the three-dimensional theorem disposes of active cells. The remaining cases cannot be handled by any fixed finite computation. The preprint constrains them in two ways: deleting one score costs a definite amount of expected maximum, via concavity from the Ehrhard inequality (Section 3), and competition against two residual scores constrains a covariance determinant (Section 4, Lemma 4.1 and Corollary 4.2, pp. 11–12). Combining these must rule out every configuration with five or more cells.
Space d is EuclideanSpace ℝ (Fin d) and the measure is stdGaussian. IsPartition A asks each cell to be measurable and almost every point to lie in exactly one cell, matching the paper's convention that partitions are taken up to null sets.centroid A is the Bochner integral of the identity over A; value sums squared Euclidean norms. Integrability holds because Gaussian measures have finite first moments.propeller d k (cells empty) is a partition with value exactly . The sectors are written with closed inequalities, so they overlap only on null rays.The Johnson–Lindenstrauss lemma (1984) says that any points of a Hilbert space can be placed in -dimensional Euclidean space with distortion at most any prescribed . This dimension reduction is used throughout analysis, geometry and algorithm design. Johnson and Lindenstrauss also asked what analogues hold in other Banach spaces. For the spaces with the question splits into several versions: whether one needs the map to be linear, whether one discretizes a whole subspace or only a finite set, and whether the target is a coordinate space with the same exponent. This mission concerns the finite-set, coordinate-target, nonlinear version: how many coordinates are needed so that every -point subset of embeds into with distortion at most ?
The source of this mission, an OpenAI preprint dated September 23, 2026, claims that for every fixed , , and the dimension is .
All spaces are real. Fix , an integer and . Let be the least integer such that for every measure space and every distinct points there are and a scale with
The map is arbitrary, not required to be linear. Put
For fixed , :
Since , the upper bound is . The Lean statement OAI.SubpolynomialLp.source_main is open on the platform.
For the best previous finite-set bounds were polynomial in (linear for ), and for logarithmic dimension is impossible. The theorem places at for every fixed , in contrast with exact embeddings, where the dimension is of order . Thus the exponent jumps from at to for every . The upper exponent and the logarithmic lower bound are not claimed to be optimal. The theorem is existential; no embedding algorithm is asserted.
The result is claimed in an OpenAI preprint and has not been peer reviewed; no machine-checked proof exists. A formal proof would include a probabilistic construction (stable laws, Poisson sampling, Rosenthal-type moment inequalities), an electrical-flow localization estimate, and a convex-separation argument.
Linear maps cannot work: fixed-distortion linear maps on some configurations need dimension proportional to when . Subspace discretization theorems apply to the span of the points, which has dimension up to , so they also give only polynomial bounds. The Johnson–Lindenstrauss approach relies on Gaussian rotation invariance, which has no analogue in . One needs a single random scalar map whose increments have nearly equal normalized -th moments simultaneously for all pairs, with relative (not additive) error control.
coordinateDistance p y z is on Fin d → ℝ.GoodDimension p n D d quantifies over every measure space (Ω, mΩ, μ) in a fixed universe and every injective x : Fin n → Lp ℝ (ENNReal.ofReal p) μ; the target is Fin d → ℝ with the distance and a scale .dimension p n D is the sInf of the good dimensions in ℕ. The goal also asserts that this infimum is good, so the default value of sInf ∅ cannot make the bounds trivial.gamma p is as above; the exact-embedding lower bound uses natural-number division, i.e. the floor.Tendsto statement along n : ℕ for each .A complete development needs spaces, -stable random variables, Poisson sampling and moment inequalities, effective resistance and electrical flows on complete graphs, and Carathéodory's theorem for the exact-embedding upper bound. Contributions formalizing the exact-embedding bounds (Ball's upper bound and the antipodal lower bound) and the weighted moment criterion are welcome.
The Brunn–Minkowski inequality is a cornerstone of convex geometry, with consequences ranging from the isoperimetric inequality to concentration of measure. The Brunn–Minkowski theory of Firey and Lutwak replaces the Minkowski combination, whose support function is , by a -mean of support functions. As the -mean becomes the geometric mean , giving the logarithmic combination of two bodies. In 2012 Böröczky, Lutwak, Yang and Zhang conjectured that, for origin-symmetric convex bodies, the logarithmic combination already satisfies the multiplicative Brunn–Minkowski bound. This would be a strict strengthening of the classical inequality in the symmetric case. The conjecture is equivalent to a logarithmic Minkowski inequality for cone-volume measures and, by work of Saroglou, implies the (B)-conjecture for even log-concave measures. Symmetry is essential: the inequality fails for general bodies.
A convex body is a compact convex set with nonempty interior; it is origin-symmetric if , in which case is an interior point. Its support function is
which is strictly positive for origin-symmetric bodies. For a positive function on the sphere, the Wulff body is
The logarithmic combination of with parameter is . In general is not itself a support function, which is why the Wulff body is needed. denotes Lebesgue measure.
For , origin-symmetric convex bodies and ,
The goal statement is published on the platform with status Open.
The result itself. By the arithmetic–geometric mean inequality, , so the theorem strengthens the multiplicative Brunn–Minkowski inequality for symmetric bodies. It implies the symmetric Brunn–Minkowski inequality for every (Corollary 1.2 of the source), the logarithmic Minkowski inequality for cone-volume measures, and, through Saroglou's transfer, the (B)-conjecture: is log-concave for every even log-concave measure and origin-symmetric convex body (Corollary 8.1 of the source).
Formalizing it. The statement uses only Euclidean space, support functions and Lebesgue measure, all in Mathlib. The proof uses smooth approximation of polytopes, moment coordinates, a variance bound and a tensor estimate. A formal proof would put a long-standing conjecture of convex geometry on a machine-checked footing; Mathlib does not yet contain the classical Brunn–Minkowski inequality in this generality, and that would be a natural reusable milestone.
The classical proofs of Brunn–Minkowski (Prékopa–Leindler, mass transport) apply to Minkowski sums, but the logarithmic combination is not a Minkowski sum and is not a support function, so these tools give only the weaker inclusion bound. Local (second-variation) approaches reduce the problem to a spectral gap for the Hilbert–Brunn–Minkowski operator on even functions, but local-to-global arguments had only been completed near the ball, for zonoids, or under extra symmetry. Without symmetry the inequality is false, so any argument must use the evenness of the bodies.
EuclideanSpace ℝ (Fin n) with ; convex bodies are compact, convex, with nonempty interior; symmetry is x ∈ K ↔ -x ∈ K.sSup of over , nonempty and bounded for a convex body, so it is the true maximum. Real powers rpow are applied to positive support values (positivity follows from symmetry and nonempty interior).volume in ℝ≥0∞, with ℝ≥0∞-valued powers and . At the inequality reduces to (resp. ), so the edge cases are consistent.How densely can equal disks be packed in the plane? The hexagonal arrangement, with centers on the triangular lattice, covers a fraction of the plane, and Thue's theorem says no packing does better. In 2003 Cohn and Elkies introduced a linear programming bound for sphere packing: a single auxiliary function whose values are nonpositive outside a ball and whose Fourier transform is nonnegative certifies an upper bound on packing density. Viazovska (dimension 8) and Cohn, Kumar, Miller, Radchenko and Viazovska (dimension 24) found auxiliary functions for which the bound is sharp, solving sphere packing in those dimensions. Cohn and Elkies conjectured that a sharp function exists also in dimension 2 (Conjecture 7.3 of their paper). The planar packing problem itself is classical; the question here is whether the Fourier method certifies it exactly.
The source of this mission, an OpenAI preprint dated September 23, 2026, claims an explicit sharp planar certificate.
Scale disks to radius , so a packing is a set of centers with for distinct centers. The Fourier transform is
A Schwartz function is smooth with all derivatives decaying faster than any inverse power of . A function is radial if depends only on ; for real radial integrable , is real and radial. The Cohn–Elkies theorem says that if is admissible, for and , then every packing of radius- disks has density at most .
There is a real radial Schwartz function with
Lean: OAI.sharp_fourier_certificate, open on the platform.
With the Cohn–Elkies bound equals , the hexagonal density, so the theorem answers the two-dimensional case of Cohn–Elkies Conjecture 7.3 affirmatively and gives a Fourier-analytic proof of Thue's theorem for arbitrary (not only periodic) packings. Its zero structure also recovers uniqueness of the triangular lattice among periodic optimal packings. The certificate does not satisfy the additional zero-set requirement of Cohn–Elkies Conjecture 8.1, which remains a separate question. The construction methods feed into the companion work on universal optimality of the triangular lattice in the same family. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists. By contrast, Viazovska's dimension-8 theorem has been the subject of formalization efforts, so a planar certificate would be a natural low-dimensional companion.
In dimensions 8 and 24 the magic functions come from modular forms, whose symmetries control a function and its Fourier transform at once. No such modular construction is known to produce the planar certificate, and Sardari's nonuniqueness theorem shows that prescribing values and derivatives on the lattice shells does not pin a function down. Numerical Laguerre–Gaussian searches (Cohn–Elkies) approach the bound but do not attain it. The hard part is an exact construction together with rigorous sign control of both (for ) and (everywhere), including between interpolation nodes and in the tails.
EuclideanSpace ℝ (Fin 2); the function is a SchwartzMap Plane ℝ.SharpPlanar.fourier f ξ is the Bochner integral of ; for a Schwartz function it is the usual transform.SharpCertificate f: Radial f, fourier f 0 = 1, f 0 = 2 / √3, for every ξ the transform has zero imaginary part and nonnegative real part, and f x ≤ 0 when 1 ≤ ‖x‖.A complete development needs Fourier transforms of radial functions in the plane (Hankel transforms, Gaussian pairings) and rigorous interval or Bernstein-polynomial sign certification. Formalizing the Cohn–Elkies bound itself (certificate implies density bound) would be a valuable reusable companion. Contributions formalizing Proposition 2.2, Proposition 3.4 or Proposition 4.3 are welcome.
Which arrangement of points in the plane minimizes interaction energy? For many repulsive interactions the expected answer is the triangular (hexagonal) lattice. Universal optimality, formulated by Cohn and Kumar (2007, doi:10.1090/S0894-0347-06-00546-7), asks for a single configuration that minimizes energy simultaneously for every completely monotone potential of squared distance, which includes all Gaussians and all inverse powers. It was proved in dimensions 8 and 24 for and the Leech lattice; in dimension two it was a conjecture. The question matters in mathematical physics (crystallization, vortex lattices, Coulomb and Riesz gases) and in the theory of Fourier interpolation.
The source of this mission, an OpenAI preprint dated September 26, 2026, claims the full planar statement against all locally finite configurations of density one. A companion OpenAI preprint reaches the same energy conclusion by a different (modulo-12) interpolation construction.
Let and , the triangular lattice of covolume one. Let be the closed disk of radius about the origin. A set is locally finite if each is finite, and has centered disk density one if , where .
A smooth is completely monotone if for all , . The lower energy per particle is
summing over ordered pairs. The Fourier transform is and is the dual lattice.
For every there is a real radial Schwartz with
given for by the paper's explicit atomic interpolation construction.
For every smooth nonnegative completely monotone and every locally finite of centered disk density one,
Lean: OAI.AtomicTriangular.universal_energy_minimum, open on the platform.
Theorem 1.1 would settle the planar case of the Cohn–Kumar universal-optimality conjecture in a density-based competitor class with no periodicity or perturbation assumption, for every completely monotone potential including those (such as with ) whose lattice sums diverge. By Bernstein's theorem such potentials are mixtures of Gaussians, so the sharp Gaussian certificates of Theorem 1.2 are the analytic core. The theorem identifies the minimum value; it does not classify minimizers. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists. A formalization would also produce reusable Fourier-analytic tools in Lean (Poisson summation for lattices, linear-programming energy bounds).
Lattice-restricted results (Rankin, Montgomery) compare only lattices; a competitor here may be nonperiodic, have arbitrarily close pairs, and have large local clustering. The Fourier linear-programming method handles general competitors but needs, for each Gaussian, an auxiliary function that is simultaneously a pointwise minorant, has nonnegative Fourier transform, and is sharp: it must touch the Gaussian on every lattice shell and its transform must vanish on every dual shell. Constructing such functions for all at once, with rigorous sign control between the interpolation nodes, is the central obstacle. A second issue is passing from the density hypothesis alone (no averaging over translates) to the energy inequality.
EuclideanSpace ℝ (Fin 2); A is Set.range triangularPoint.AdmissiblePotential g: ContDiffOn ℝ ⊤ g (Ioi 0), and iteratedDeriv r g t for .energy g C is the liminf over of diskEnergy, valued in ℝ≥0∞; latticeEnergy g is a tsum in ℝ≥0∞, so divergent sums are allowed and no summability hypothesis is needed.C and the equality latticeEnergy g = energy g A.realFourier is Mathlib's 𝓕 (kernel ) applied to the complexified function; the clause names the paper's explicit coefficients (R, R0, Yf, Uplus, Uminus) and error bounds.Contributions formalizing Lemma 2.1 (reciprocal Gaussian parameters), Proposition 2.3 (density-only linear programming), Lemma 4.1 (finite certificate) and Proposition 5.1 (exact interpolation and approximation) are welcome.
A finite metric embeds into exactly when it is a nonnegative combination of cut metrics . This makes distortion the right measure for the flow–cut gap: given edge capacities and pairwise demands, the ratio between the sparsest cut value and the maximum concurrent flow . Linial, London and Rabinovich (1995) and Aumann and Rabani (1998) developed this connection, and Gupta, Newman, Rabinovich and Sinclair (2004) proved that the worst flow–cut gap on a fixed graph equals the worst distortion of its weighted shortest-path metrics. They conjectured that every proper minor-closed family embeds into with uniformly bounded distortion (the GNRS conjecture). Graphs of bounded treewidth form one of its basic cases.
Let be a finite connected graph with edge lengths . The shortest-path metric is the least total length of a path from to .
A tree decomposition of is a finite tree with bags () such that the bags cover , each edge has both endpoints in some bag, and for each vertex the nodes whose bag contains induce a connected subtree. In this mission, as in the source, bounds the bag cardinality , so the treewidth bound is .
A map has distortion at most if .
For every integer there is a constant such that for every nonempty finite connected graph with a tree decomposition of bag size at most and every , there are and with
is independent of the number of vertices, the decomposition and all ratios of edge lengths; the goal asserts only its existence. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. The theorem settles the bounded-treewidth case of the GNRS conjecture. Through the GNRS equivalence, it gives for every multicommodity instance on graphs of treewidth less than . By the Robertson–Seymour excluded-planar-minor theorem it also covers every family excluding a fixed planar minor. Combined with known approximation algorithms for the minimum distortion (Gupta–Talwar–Witmer 2013; Cohen-Addad–Mömke–Verdugo 2024), it yields fixed-parameter-time embeddings of distortion . With the planar companion preprint it covers the almost-embeddable families of Lee and Sidiropoulos.
Formalizing it. The proof constructs cut measures directly on a tree decomposition and combines them with padded random partitions from the literature. A formal proof would certify that the constants depend only on , the point at which earlier approaches lost uniformity.
The successful pathwidth approach embeds the graph stochastically into dominating trees, but that route cannot work here: some series-parallel metrics require expected tree distortion (GNRS 2004, Theorem 5.6). Local-consistency approaches assume that small vertex sets admit compatible isometric cut representations, which a general bounded-treewidth metric need not provide. Multiscale constructions from padded partitions give good separation at each scale, but summing their contributions loses a factor growing with the number of scales. The construction must handle arbitrary branching of the decomposition tree and arbitrary edge-length ratios without such accumulation.
V is any nonempty Fintype with decidable equality; G : SimpleGraph V is connected.HasTreeDecomposition G k: a tree T on Fin n, bags Fin n → Finset V covering all vertices and all edges, with the bags containing each vertex inducing a connected subgraph of T, and all bags of cardinality at most k.ℓ : G.edgeSet → ℝ, strictly positive. shortestPathDistance is the sInf of lengths of paths (IsPath) from to ; this set is finite and nonempty for a connected finite graph, so the infimum is the true distance.PiLp 1 (Fin m → ℝ) with chosen per graph; this is the source's remark (p. 2) that the target can be taken to be finite-dimensional , and it is at least as strong as an target.C depends only on k and is quantified before the graph.A finite metric space embeds into exactly when its metric is a nonnegative combination of cut metrics . For this reason the least distortion with which a graph metric embeds into governs the gap between multicommodity flow and sparsest cut: Linial, London and Rabinovich (1995) and Aumann and Rabani (1998) connected metric embeddings to the approximate max-flow/min-cut theorem, and Gupta, Newman, Rabinovich and Sinclair (2004) proved that the worst flow–cut gap on a fixed graph equals the worst distortion of its weighted shortest-path metrics. They conjectured (the GNRS conjecture) that every proper minor-closed graph family embeds into with uniformly bounded distortion. The planar case has been the central open instance.
Let be a finite connected simple graph on vertex set with symmetric edge lengths on edges. The graph metric is the infimum of over walks from to . is planar if it has a drawing in : distinct points for vertices and, for each edge, an injective arc between its endpoints whose interior avoids every vertex and meets the interior of no other edge.
A map into the real space of some measure space has distortion at most if for all .
There is a constant such that for every , every connected planar graph on vertices and every symmetric positive edge-length function , there are a measure space and with
The constant is not fixed: the goal asserts only existence, so any improvement of the constant is compatible with it. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. The theorem settles the planar case of the GNRS conjecture. By the Gupta–Newman–Rabinovich–Sinclair equivalence it gives a universal constant bound on the fractional flow–cut gap for arbitrary demands in planar graphs. With the bounded-treewidth companion preprint it also yields constant distortion for the fixed-parameter almost-embeddable families of Lee and Sidiropoulos (Corollary 10.1 of the source). The general clique-sum closure needed for the full GNRS conjecture is not established.
Formalizing it. The statement is elementary (finite graphs, arcs in the plane, an space), yet the proof combines a geometric column model of planar graphs, random multiscale cut constructions and packing estimates. A formal proof would certify every scale-combination step, where errors in uniformity are easy to make.
Standard random-partition methods for planar graphs separate pairs at each distance scale with good probability, but naive summation over scales costs a factor proportional to the number of scales, which is unbounded when edge lengths vary. Embedding first into Euclidean space cannot work: Newman–Rabinovich show Euclidean distortion is necessary already for series-parallel graphs. The difficulty is to combine separations at different scales while keeping a single uniform upper bound on every edge.
Fin n; the graph is a SimpleGraph (Fin n) with G.Connected (so ). Singletons are allowed.IsPlanar G asks for an injective vertex placement in ℝ × ℝ and, for each ordered adjacent pair, an injective continuous arc on the unit interval with the right endpoints, whose interior avoids all vertex points and meets the interior of another arc only if it is the same unoriented edge.Fin n → Fin n → ℝ, symmetric, and positive on adjacent pairs; values on non-adjacent pairs are irrelevant. graphDistance is the sInf of walk lengths; for a connected graph with nonnegative edge lengths the set of walk lengths is nonempty and bounded below, so the infimum is the genuine shortest-path distance.MeasureTheory.Lp Ω ℝ 1 μ for an existentially chosen measure space, and the inequalities are stated without a rescaling factor (the rescaling is absorbed into ).The projection body of a convex body is the convex body whose support function in a unit direction is the -dimensional volume of the shadow of on . Petty showed that is affinely covariant, so the normalized volume
is invariant under invertible affine maps, and its extremal values are natural affine isoperimetric questions. Petty's conjecture concerns the minimum (ellipsoids). For the maximum, Brannen conjectured in 1996 that simplices maximize among all convex bodies (Mathematika 1996); the simplex value is .
This mission asks for a formal proof of an explicit counterexample in dimension , as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
A convex body in is compact and convex with nonempty interior, and is -dimensional volume. For the brightness is , and
Let be the standard simplex and
The benchmark constant is , which equals of every -simplex (Proposition 5, p. 4).
It is not true that for every convex body .
is a convex body and
The result itself. Brannen's conjecture fails: in dimension the simplex is not the maximizer of normalized projection-body volume. The mechanism is the product identity for polytopes (Proposition 3, p. 3), which shows that is a lower bound for any universal upper constant in dimension ; iterating it gives an exponential excess for all large (Corollary 6, p. 6). The counterexample in dimensions was obtained independently by Feng, Hu, Liu and Xu; the contribution here is an explicit product witness with an exact rational value. The optimal upper constant and its maximizers remain separate questions.
Formalizing it. Every ingredient is elementary: the facet formula for projection bodies of polytopes (Cauchy's formula, Lemma 2, p. 2), the facet structure of a Cartesian product, affine covariance (Lemma 4, p. 3), and a fiber computation of . A formal proof would supply Mathlib with projection bodies of polytopes and Cauchy's projection formula, both reusable. The final comparison is an exact rational identity.
There is no shortcut through general inequalities: the statement is a strict comparison of two explicit volumes in dimension , so both and must be computed exactly. Computing of a product directly from shadow volumes is unwieldy; the efficient route goes through facet area-normal vectors, which requires proving that, up to a null set, each point of a shadow lies over exactly two facet interiors, and that the facets of are exactly and . The simplex value needs the volume of a cube plus a segment.
EuclideanSpace ℝ (Fin 20). In the goal, projectionVolume is the induced Lebesgue measure on the submodule of the orthogonal projection of ; brightness u = ‖u‖ * projectionVolume, so the support-function inequality is imposed for all (the homogeneous extension).productWitness is the set of whose first and last ten coordinates both lie in standardSimplex 10; the goal includes that it is compact, convex, with nonempty interior.simplexConstant 20 is the explicit number , not ; the goal states the exact ratio, its reduced fraction, the strict inequality, and .euclideanHausdorffMeasure (d-1) of the image under the orthogonal projection, and compares with ratio (simplex 20), so it implicitly needs Proposition 5.toReal; all bodies involved are bounded, so no infinite value is hidden.The projection body of a convex body packages the areas of all shadows of into a single convex body: its support function in direction is the -dimensional volume of the orthogonal projection of onto . The normalized volume is invariant under translations and invertible linear maps, so asking for its extremizers is an affine isoperimetric problem. Petty's projection-volume conjecture (Petty, 1971) predicts that this ratio is minimized exactly by ellipsoids. It is related to, but distinct from, Petty's projection inequality for the polar body , which is a classical theorem; inequalities in this family underlie affine Sobolev inequalities and isoperimetric inequalities in normed spaces.
This mission asks for a formal proof of the conjecture in every dimension , as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
A convex body is a compact convex set with nonempty interior, and denotes -dimensional Lebesgue volume. For a unit vector , let be the orthogonal projection of onto the hyperplane and the Lebesgue measure on that hyperplane. The projection body is
the convex body with support function . Write for the volume of the Euclidean unit ball . An ellipsoid is a set with and an invertible linear map. Since , the ball has ratio .
For every integer and every convex body ,
with equality if and only if is an ellipsoid.
The result itself. Together with the separately proved three-dimensional case, it settles Petty's conjecture for all (in dimension the ratio is constant up to the standard identification). The preprint derives from it the Lutwak–Petty lower-degree inequalities, a mixed determinant-gradient inequality strengthening the Sobolev–Zhang affine inequality, and the sharp Holmes–Thompson isoperimetric inequality in normed spaces (Corollaries 7.1–7.3, pp. 27–29). Those corollaries for rely on the external three-dimensional theorem.
Formalizing it. The proof uses the first variation of volume, spherical harmonics with explicit cosine and Funk transform multipliers, a strict harmonic estimate for arbitrary norms, a variational representation of support functionals, and Brouwer's fixed-point theorem. Mathlib has Brouwer-type results only in limited forms and has no spherical-harmonic decomposition of ; these would be reusable. No machine-checked proof of any case of the conjecture is known.
Previous results are local: they require the body, after a linear change of variables, to be close to the ball, because the harmonic analysis of the projection operator only controls perturbations of the ball. A global argument must handle arbitrary bodies without symmetry or regularity. In the preprint (pp. 2–3) the degree-two spherical harmonic component is not a zero mode of the relevant sign-test operator and has to be removed by choosing affine coordinates; this needs a continuous family of variational minimizers extended to singular matrices and a fixed-point argument (Proposition 5.5, p. 23). Harmonics of degree at least four are controlled by a strict norm estimate valid for every norm (Theorem 4.1, p. 12). The equality case must come out of the same estimates.
Space n is EuclideanSpace ℝ (Fin n); IsConvexBody K is compact, convex, nonempty interior; .shadowVolume K u is the measure, in the induced Euclidean volume on the submodule , of the image of under orthogonalProjectionOnto. projectionBody K is the intersection of half-spaces over unit vectors, which has support function shadowVolume K because that function is itself a support function.projectionRatio K = volume.real (projectionBody K) / volume.real K ^ (n - 1); for a convex body both volumes are finite and the denominator is positive.pettyConstant n = kappa (n-1) ^ n * kappa n ^ (2 - n) with an integer exponent, the volume of the closed unit ball.IsEllipsoid K: for a linear equivalence .iff equality characterization; neither part is vacuous for .