The mathematical foundations of computation: which problems can be solved, by what algorithms, and at what cost in time, space, or communication. Distinguished by its emphasis on rigor and unconditional lower bounds, it spans computational complexity, algorithm design, automata and computability, cryptography, and the analysis of Boolean functions.
Exponential PSD rank of positively shifted matching matricesOpen Problem
Motivation
Semidefinite representations may be smaller than linear descriptions of a polytope. Lower bounds for their matrix size require a factorization obstruction that applies to arbitrary positive-semidefinite factors. The source manuscript presents the surrounding research claim.
Setting
For even n, columns are perfect matchings of the complete graph. Rows comprise edges and odd vertex subsets. The unshifted slack matrix has edge-incidence entries and odd-cut entries |M∩δ(U)|−1. Its real PSD rank is the least positive r admitting trace products of positive-semidefinite r×r factors.
Formalization target
Prove that every positive real power is eventually exceeded:
∀C>0∃n0≥4∀ even n≥n0,nC<psdRank(n).
The separate lift target gives the same superpolynomial lower bound for every exact affine PSD lift.
The selected formal goal excludes polynomial-size factorizations. The manuscript dated October 5 states exponential bounds for positively shifted matching matrices; that stronger shifted statement is not the existing published target. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Difficulty
Factors are unrestricted real PSD matrices, with no rank-one or symmetry requirement. Lower bounds for nonnegative rank alone do not rule them out.
Formalization scope
The target concerns the full unshifted row set and uses real exponentiation with C fixed before n₀. The affine-lift companion quantifies over affine sections and affine images of PSD cones. Independent definition groups are retained separately. The description deliberately makes no exponential or positive-shift claim for these references.
Polynomial Hitting Lists for Noncommutative Rational FormulasOpen Problem
Motivation
Inversion gates create domains of definition as well as nonzero-value conditions. A rational hitting list must find a point where every inverse exists and where the final value is invertible. The source manuscript presents the surrounding research claim.
Setting
A noncommutative rational formula over ℚ has variables, constants, sums, ordered products and inverse gates, with tree-node size. Evaluation is a relation requiring genuine two-sided inverses. Admissible means defined at some positive-dimensional rational matrix tuple; nonzero means one such defined value is nonzero.
Formalization target
Construct one deterministic finite-state Turing machine and positive integers C,k which, on unary n,s≥1, outputs a list H of common positive-dimensional rational tuples with
dimH,∣encode(H)∣,time(H)≤C(n+s+1)k,
and every admissible nonzero size-s formula has a defined invertible value at some tuple in H.
The output-length bound controls the full binary representation, including rational entries and all tuples. No separate inverse-depth or coefficient-height parameter is added. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Difficulty
A tuple detecting one rational expression may encounter a singular inverse in another. Definedness and invertibility must be guaranteed at a list point for every eligible formula.
Formalization scope
Matrices and constants are rational; scalars use the algebra map. The fixed TM0 alphabet and state space, self-delimiting binary output and unary parameter input are explicit. The matrix dimension is shared across the entire list and required positive.
One Rational Matrix Hitting Point for Noncommutative FormulasOpen Problem
Motivation
Testing a noncommutative polynomial at scalar points can lose its ordered-word structure. Matrix evaluation preserves noncommutativity and permits a single prescribed tuple to test an entire bounded-size formula class. The source manuscript presents the surrounding research claim.
Setting
A division-free formula has scalar and variable leaves and addition or ordered multiplication gates. Its size counts every tree node. Nonzero means that at least one coefficient of its word series is nonzero. The published generator is an explicit tuple of rational matrices depending only on n and s.
Formalization target
For all n,s≥1, every characteristic-zero field F and every formula f of size at most s, prove
f=0⟹f(T1,…,Tn)=0,
where the rational tuple T is coerced into F and has dimension 2ns², except for the specified one-variable size-one case.
One tuple is universal for the whole size class and every characteristic-zero coefficient field. The formal goal establishes its hitting property. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Difficulty
Nonzero word coefficients must survive the same matrix substitution uniformly across all formulas. Choosing a point separately for each f would reverse the required quantifiers.
Formalization scope
Formula coefficients are defined by word convolution; evaluation uses scalar matrices and the explicit rational generator. The theorem asserts nonzero matrix output, not invertibility. The manuscript’s deterministic construction-time claim is not a separate statement in this selected Lean target.
Selected references
OpenAI, One Rational Matrix Hitting Point for Noncommutative Formulas, preprint, 2026. Pinned manuscript.
One Sample Suffices for Matroid Prophet Inequalities against an Almighty AdversaryOpen Problem
Motivation
Online selection must commit before all values arrive, while the offline optimum sees the full vector. The mission asks how much one independent sample per item can recover under a matroid feasibility constraint. The source manuscript presents the surrounding research claim.
Setting
A matroid on Fin n specifies feasible independent subsets. An online rule sees the full initial sample vector, a finite random seed and the arriving label/value prefix. Sample and value coordinates are jointly independent, corresponding marginals agree, and the seed is independent of all of them.
Formalization target
For every labeled matroid, construct a distribution-independent rule and seed law such that every prefix is feasible and, for every measurable arrival permutation,
E[reward]≥2−310E[OPT].
The arrival order may depend on all samples, all values and the entire seed. Reward integrability is also required.
The rule and its seed distribution depend only on the known matroid. The allowed adversary is stronger than an order chosen before the values or random seed are revealed. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Difficulty
Independence of the input coordinates does not imply independence of the adversarial order. The guarantee must survive an order selected with full information while decisions remain irrevocable.
Formalization scope
Values are nonnegative almost surely, and only the actual offline optimum is assumed integrable. The hidden-vector target with ratio 2⁻²⁹³ provides an available supporting milestone. The duplicated one-sample formulation and secretary consequence remain references in their independent source group.
Selected references
OpenAI, One Sample Suffices for Matroid Prophet Inequalities against an Almighty Adversary, preprint, 2026. Pinned manuscript.
Complex Matrix Multiplication Below 2.258 and Rectangular BoundsOpen Problem
Motivation
Rectangular matrix products arise when the two outer dimensions are much larger than the inner dimension. The dual exponent records the largest inner growth rate compatible with arithmetic exponent two. The source manuscript presents the surrounding research claim.
Setting
For k∈[0,1], ω_ℂ(1,k,1) is the infimum of exponents for multiplying an n×⌈nᵏ⌉ matrix by a ⌈nᵏ⌉×n matrix over ℂ. The dual exponent α is the supremum of k for which this infimum equals two.
Formalization target
Prove the strict bound
αC>20093=0.465.
The additional published rectangular endpoint asserts ω_ℂ(1,709/1000,1)<523/250=2.092.
Strictness is part of both statements. The supplied goal concerns the complex dual exponent; the manuscript title’s square bound and broader field claims are not attached formal targets. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Difficulty
An algorithm for one size does not establish an asymptotic exponent. The definition quantifies over every positive slack and all positive sizes with one bound constant for each slack.
Formalization scope
Algorithms are division-free arithmetic programs with constants and input gates of cost zero and addition, subtraction and multiplication of cost one. Correctness is quantified over all input matrices. The dual exponent is a real supremum of exact exponent-two shapes, using the prescribed inner-dimension ceiling.
Weak and strong normalization in pure type systemsResearch Paper
Motivation: does having a normal form imply termination?
Pure type systems (PTSs) are a uniform framework covering the simply typed λ-calculus, System F, the calculus of constructions and the type theories behind proof assistants such as Coq and Lean. A system is specified by its sorts (like ∗ and □), axioms (∗:□) and product rules (which dependent function types may be formed). Normalization is the key metatheoretic property: it underlies logical consistency and decidability of type checking. There are two versions. A term is weakly normalizing if some sequence of β-reductions reaches a normal form, and strongly normalizing if every reduction sequence is finite. Strong normalization is what implementations need (any evaluation strategy terminates) but it is much harder to prove. The Barendregt–Geuvers–Klop conjecture asserts that, for pure type systems, the system-wide weak property already implies the strong one.
Timeline
1989 — Girard's Proofs and Types presents the Tait–Girard reducibility method for strong normalization (book).
1993 — Geuvers states the system-wide conjecture for β and βη reduction in his thesis (Logics and Type Systems, Nijmegen, Conjecture 8.1.2) (thesis).
1997 — Sørensen proves the implication for generalized nondependent, clean, negatable systems via continuation-passing translations (thesis, Copenhagen, Theorem 3.5.20).
2001 — Barthe, Hatcliff and Sørensen prove a uniform nondependent version (TCS 2001).
2006 — Barthe and Coquand show that erasing λ-domain annotations can identify non-convertible terms in non-normalizing PTSs (JFP 2006), a constraint on erasure-based approaches.
2014 — Roux and van Doorn develop a structural theory of PTSs, preserving weak normalization under sums and added rules (RTA–TLCA 2014).
2023 — Mull reduces the conjecture within tiered systems to an irrelevance-eliminating translation (TYPES 2022, LIPIcs 2023) and extends the nondependent results in his thesis (Chicago, 2023).
2025 — Roux proposes internal strong-normalization proofs for specific systems (TYPES 2025 abstract).
2026 — An OpenAI preprint, Weak and strong normalization in pure type systems (OpenAI Math Release, September 25, 2026), claims the β-version of the conjecture for every PTS, with no functionality assumption. The preprint has not been peer reviewed and its theorem is not formally verified.
Setting
A specification consists of a type S of sorts, an axiom relation A⊆S2 and a rule relation R⊆S3; neither is assumed functional. Expressions are
M,N,A,B::=x∣s∣MN∣λx:A.M∣Πx:A.B,s∈S,
up to renaming of bound variables. β-reduction is the compatible closure of (λx:A.M)N→βM[x:=N], with steps allowed everywhere, including inside the annotation A of a λ and both parts of a Π. TypingΓ⊢M:A is generated by the seven standard PTS rules (axiom, variable, weakening, product, abstraction, application, conversion up to =β). A context is valid if each declared type is typed by a sort in the preceding prefix, and M is legal in Γ if Γ⊢M:A or Γ⊢A:M for some A.
The system is weakly (strongly) normalizing if every legal expression in every valid context is weakly (strongly) normalizing.
Formalization targets
Goal: β-Barendregt–Geuvers–Klop (Theorem 1)
For every specification P=(S,A,R),
(∀Γvalid,∀Mlegal in Γ:Mis weakly β-normalizing)⟹(∀Γvalid,∀Mlegal in Γ:Mis strongly β-normalizing).
Both quantifiers range over the whole system; the theorem does not claim that an individual weakly normalizing term is strongly normalizing, and it says nothing about η-reduction. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
Significance
The result itself. For any PTS, a proof that every legal term has a normal form now yields termination of every β-reduction strategy, including reductions inside types and annotations that may continue after the computational body is normal. Earlier results needed nondependent products, cleanliness, negatability, a tiered sort hierarchy, or a translation requiring extra product rules; the general case — arbitrary sorts and nonfunctional rules — was not covered by any earlier result since Geuvers' 1993 formulation.
Formalizing it. The statement is entirely syntactic and finitary, so it is a natural target for a proof assistant, and the relevant objects (de Bruijn syntax, substitution, typing derivations) are standard formalization material. The proof in the source is long (over 70 pages) and combines reducibility candidates with a fixed-point construction over sort profiles; a machine check would substantially raise confidence. A formal PTS metatheory library (substitution lemmas, confluence, subject reduction) would be reusable for other type-theory formalizations.
Difficulty
The obvious route — reducibility candidates à la Tait–Girard — needs a model of types built by recursion on sorts, which fails for impredicative or nonfunctional specifications where a type can have several sorts and no hierarchy is available. Translation methods (CPS or irrelevance elimination) need specific product rules to preserve typing, which a general specification may lack. Weak normalization of one term cannot be used alone; the argument must exploit normal forms of other open expressions. Annotations add a further complication: erasing them can change the equational theory (Barthe–Coquand), so reduction inside annotations must be tracked rather than erased.
Formalization scope
Expressions use de Bruijn indices (Expr S with var, sort, app, lam, pi), so α-equivalence is syntactic; substitution is parallel substitution with lifting.
Beta is full compatible closure, including lam_domain, pi_domain and pi_body steps; conversion is Relation.EqvGen Beta.
HasType has exactly the seven PTS rules; contexts are lists stored newest-first, each declaration typed in its prefix (ValidContext). Legal includes expressions occurring as types.
Weak normalization is reduction to a normal form; strong normalization is accessibility for the converse of Beta.
The sort type S is arbitrary (any universe), and axioms and rules are arbitrary relations: no functionality, finiteness or hierarchy assumptions.
Needed infrastructure: renaming/substitution lemmas, confluence of β, subject reduction for PTSs, reducibility candidates. All are reusable for any PTS formalization.
G. Barthe, J. Hatcliff and M. H. Sørensen, Weak normalization implies strong normalization in a class of non-dependent pure type systems, Theoret. Comput. Sci. (2001). https://doi.org/10.1016/S0304-3975(01)00012-3
G. Barthe and T. Coquand, Remarks on the equational theory of non-normalizing pure type systems, J. Funct. Programming (2006). https://doi.org/10.1017/S0956796803004726
Witnessed symmetric choice is strictly stronger than choiceless polynomial time with countingResearch Paper
Motivation
A logic for unordered finite structures (graphs, databases, relational inputs given up to isomorphism) must give answers that do not depend on how the input elements are named. Many polynomial-time algorithms nevertheless make arbitrary intermediate choices, for example the pivot in Gaussian elimination, without changing their final answer. Choiceless polynomial time with counting (CPT), introduced by Blass, Gurevich and Shelah (1999), forbids such choices entirely: it computes with hereditarily finite sets over the input elements and can count, but can never pick one element from a set merely because the set is nonempty.
Witnessed symmetric choice (WSC), in the form of Lichter and Schweitzer (2022, arXiv version 3), adds a controlled form of choice: the logic may pick an element of a set provided it also constructs automorphisms of the input showing that all elements of that set are interchangeable, so the answer cannot depend on which one was picked. Lichter and Schweitzer asked whether CPT + WSC is strictly more expressive than CPT. This mission concerns a proof that it is.
Timeline
1992. Cai, Fürer and Immerman construct graph pairs that hide a global parity obstruction from bounded-variable counting logic (doi:10.1007/BF01305232).
1998. Gire and Hoang introduce a fixpoint logic with a symmetry-based choice construct (doi:10.1006/inco.1998.2712).
2003. Dawar and Richerby define a fixed-point logic with symmetric choice, with parameters and nesting (doi:10.1007/978-3-540-45220-1_16).
2008. Dawar, Richerby and Rossman show that preordered CFI queries are CPT-definable, and that bounded-rank CPT fails on them (doi:10.1016/j.apal.2007.11.011).
2022–2023. Lichter and Schweitzer define CPT + WSC, show that definable isomorphism testing yields canonization, and ask whether WSC strictly adds expressive power (arXiv:2205.14003).
The source of this mission is an OpenAI preprint dated September 24, 2026; its companion preprint (September 23, 2026) proves that CPT does not capture polynomial time.
Setting
Let A be a finite set of atoms and HF(A) the hereditarily finite sets over A. CPT terms are built from variables, ∅, Atoms, Pair(a,b)={a,b}, Union, Unique (the member of a singleton, else ∅), Card (the von Neumann ordinal ∣a∣), comprehensions {s(aˉ,u):u∈t(aˉ),θ(aˉ,u)} and iteration from ∅; formulas use input relations, equality and Boolean connectives. A sentence(Φ,p) pairs a closed formula with a polynomial p that bounds the number of iteration steps and the hereditary size of all intermediate objects on inputs with n atoms; exceeding the bounds yields a default or a failure value †.
A WSC operator iterates a step term in which, at each stage, a choice term proposes a nonempty set D; one element is chosen, and a witness term must produce automorphisms of the entire input that fix the parameters and all earlier stages and map any element of D to any other. If the witnesses are valid along every possible choice sequence, the output formula's value on the terminal state is returned; otherwise the value is †.
The true-model class of a sentence is the set of finite structures on which it returns true; false and † are both outside it.
Formalization targets
Goal: Theorem 1.1
For the fixed vocabulary τ of eight binary relations there is a CPT + WSC sentence (Φ,p) with exactly one WSC occurrence such that
(i)(Φ,p)returns true or false on every finite τ-structure;(ii)TrueModels(Φ,p)=TrueModels(Ψ,q)for every CPT sentence (Ψ,q).
The Lean statement OAI.WitnessedChoice.main (via BGS.MainStatement) is open on the platform.
Significance
Since every CPT sentence is a CPT + WSC sentence, Theorem 1.1 gives a strict inclusion of definable Boolean queries and answers the expressiveness question posed by Lichter and Schweitzer in the true-model sense. The separation holds against CPT with counting and sets of arbitrary finite rank, not a rank-restricted fragment. It leaves open whether CPT + WSC captures polynomial time and the effect of nesting WSC operators.
The result is proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists.
Difficulty
Two different tasks must be done. The upper bound requires a legal WSC definition on all inputs, not only on the intended grid structures: witnesses must be genuine automorphisms of the whole input fixing the full history, which the sentence must check, with a fallback when the input is not of the intended shape. The lower bound must defeat every CPT sentence, including those that build nested sets of large rank; rank-sensitive support arguments (Dawar–Richerby–Rossman) do not suffice. The paper uses a nonabelian automorphism group whose central subgroup has rank-independent small supports, then a counting equivalence and a bounded-width description of complete CPT evaluations.
Formalization scope
Syntax is a mutual inductive Term n / Formula n with de Bruijn-style Fin n variables, including iterate and the wsc formula; wscCount counts WSC occurrences.
Evaluation returns Option (none is †). resource p n = ⌊p(n)⌋ bounds iteration length and transitive-closure size.
WSC validity (GoodWSC) quantifies over all choice prefixes; witnesses are permutationGraph g for permutations g that are input automorphisms, fix the free parameters and every earlier stage, and act transitively on the choice set.
FiniteInput packs any finite carrier type with the eight-symbol relations (Ed, Cf, EB, VB, I, Z δ, δ : ZMod 3). Sentence.isCPT means wscCount = 0.
A complete development needs hereditarily finite sets with permutation actions, support and counting-equivalence theory, and the grid structures; much of this is shared with the companion CPT noncapture mission. Contributions formalizing Proposition 4.4 (a total all-input definition), Proposition 5.3 (transitivity for every parameter tree), Theorem 5.5 (opposite grid answers), Proposition 6.3 (small-orbit support bound), Theorem 8.1 (transfer through small supports) and Theorem 9.3 (eventual equality for every CPT sentence) are welcome.
A. Blass, Y. Gurevich, S. Shelah, On polynomial time computation over unordered structures, J. Symbolic Logic, 2002. https://doi.org/10.2178/jsl/1190150152
A. Dawar, D. Richerby, B. Rossman, Choiceless polynomial time, counting and the Cai–Fürer–Immerman graphs, Ann. Pure Appl. Logic, 2008. https://doi.org/10.1016/j.apal.2007.11.011
J.-Y. Cai, M. Fürer, N. Immerman, An optimal lower bound on the number of variables for graph identification, Combinatorica, 1992. https://doi.org/10.1007/BF01305232
F. Gire, H. K. Hoang, An extension of fixpoint logic with a symmetry-based choice construct, Inform. and Comput., 1998. https://doi.org/10.1006/inco.1998.2712
Choiceless polynomial time with counting does not capture polynomial timeResearch Paper
Motivation
Descriptive complexity asks whether complexity classes can be characterized by logics, without reference to machines. Immerman and Vardi (1982) showed that on ordered finite structures, first-order logic with a least fixed-point operator expresses exactly the polynomial-time queries. On unordered structures, such as graphs given only up to isomorphism, an algorithm must not depend on an arbitrary ordering of the input, and whether some logic captures polynomial time there is a central open question (Chandra–Harel 1982, Gurevich 1988).
Choiceless polynomial time with counting (CPT), introduced by Blass, Gurevich and Shelah (1999), was for decades the strongest candidate: it computes with hereditarily finite sets built over the input elements, can count, and is invariant under automorphisms by construction. Blass, Gurevich and Shelah conjectured that CPT is still a proper fragment of polynomial time. This mission concerns a proof of that conjecture.
2000. Shelah claims noncapture for counting extensions; later accounts continue to list the problem as open.
2008. Dawar, Richerby and Rossman show that CFI queries over ordered base graphs are CPT-definable, and that bounded-rank CPT with counting fails on them (doi:10.1016/j.apal.2007.11.011).
With unknowns (λa)a∈X and (μy)y∈Y (separate families), the system consists of
a∈Xt∑λa=1(t∈X),μy=a∈Xt∑λaC(y,a)
for every (t,y)∈X×Y such that some a∈Xt and x∈Y satisfy I(a,x) and EB(y,x). The queryQ(A) says this system is consistent over F3. No promise is imposed on the input.
A CPT program is a fixed finite set of rules that updates dynamic functions whose values are hereditarily finite sets over the atoms of A, using pairing, union, comprehension, equality, membership, the input relations, and the cardinality operation (which returns a von Neumann ordinal). A program definesQ if for fixed polynomials T,S, on every input of size n it halts within T(n) steps, touches at most S(n) hereditarily finite objects, and accepts exactly when Q(A) holds. No bound on set rank is imposed.
Formalization targets
Goal: Theorem 1
Qis isomorphism-invariant,Q∈P(from an ordered encoding),Q∈/CPT.
The Lean statement OAI.CPTSeparation.main is the conjunction of these three clauses. It is open on the platform.
Significance
The theorem confirms the Blass–Gurevich–Shelah noncapture conjecture for the full counting formalism: CPT does not capture polynomial time on unordered structures. It removes the leading candidate logic from Gurevich's question, which itself remains open. Because Q is expressible in fixed-point logic with a solvability or rank operator over F3 (Corollary 3, p. 3), it also shows that neither of those logics is contained in CPT. The lower bound holds for programs of arbitrary set rank, unlike the bounded-rank lower bounds of Dawar–Richerby–Rossman.
The result is proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists.
Difficulty
The polynomial-time upper bound is Gaussian elimination. The obstacle is the lower bound against every CPT program, including those that build sets of unbounded rank. Bounded-variable counting games handle fixed-point logic with counting but do not by themselves control CPT, which is strictly stronger (it decides CFI queries over ordered base graphs). Rank-dependent support arguments give lower bounds only for each fixed rank. The paper needs support bounds independent of rank, for which it uses a nonabelian automorphism group acting on grid structures, then a counting equivalence for all supported objects, and finally a transfer to complete computations via an interpretation characterization of CPT.
Formalization scope
Input A gives a Boolean-valued binary relation for each Symbol (Ed, Cf, EB, VB, I, Z δ with δ : ZMod 3). Input.query is the existence of λ, μ satisfying the normalization and consistency equations exactly as above; an empty system is consistent.
OrdinaryPolynomialTime asks for a function on ordered tables and a Turing.TM2ComputableInPolyTime machine with finite alphabets computing it from the cell-by-cell table encoding, agreeing with the query for every ordering of every structure.
FullCPT defines terms and rules over hereditarily finite sets (Lists quotient), a state of finitely many nonempty locations, synchronous consistent updates, halt/accept flags, and the set of occurring objects (active elements plus roots of evaluated terms). EvaluationDefinable Q asks for one program and polynomials time, space that accept exactly the inputs satisfying Q, halting within time and with at most space occurring objects.
This is the original operational formulation; the paper's proof passes through the interpretation characterization of CPT (Grädel–Pakusa–Schalthöfer–Kaiser), which a formal proof must either formalize or bypass.
A complete development needs: hereditarily finite sets and automorphism actions on them, support theory, counting equivalence games, the grid structures with their automorphism group, and a CPT-to-interpretation translation. Contributions formalizing Proposition 2 (polynomial-time decidability), Proposition 8 (small-orbit support bound), Proposition 13 (quantitative homogeneity) and Theorem 14 (transfer through small supports) are welcome.
A. Blass, Y. Gurevich, S. Shelah, On polynomial time computation over unordered structures, J. Symbolic Logic, 2002. https://doi.org/10.2178/jsl/1190150152
J.-Y. Cai, M. Fürer, N. Immerman, An optimal lower bound on the number of variables for graph identification, Combinatorica, 1992. https://doi.org/10.1007/BF01305232
A. Dawar, D. Richerby, B. Rossman, Choiceless polynomial time, counting and the Cai–Fürer–Immerman graphs, Ann. Pure Appl. Logic, 2008. https://doi.org/10.1016/j.apal.2007.11.011
E. Grädel, W. Pakusa, S. Schalthöfer, Ł. Kaiser, Characterising choiceless polynomial time with first-order interpretations, LICS, 2015. https://doi.org/10.1109/LICS.2015.68
Polynomial removal fails for ordered binary matricesResearch Paper
Motivation: removal lemmas and property testing for ordered matrices
A removal lemma says that an object far from having a forbidden substructure must contain many copies of it. Such statements are the combinatorial backbone of property testing: if every matrix that is ϵ-far from avoiding a pattern H contains at least cHϵCHn2k copies of H, then sampling a number of rows and columns polynomial in 1/ϵ detects the pattern with constant probability. Whether removal bounds are polynomial determines whether testers are efficient. For binary matrices whose rows and columns carry a fixed order, qualitative removal is known, and the polynomial version was conjectured.
Timeline
2007 — Alon, Fischer and Newman prove polynomial-query testing for fixed finite forbidden families of binary matrices when row and column order is ignored, and raise the ordered question (SIAM J. Comput. 2007, §7).
2007 — Fischer and Rozenberg obtain nonpolynomial lower bounds for a fixed 2×2 pattern in ternary host matrices, order ignored (APPROX–RANDOM 2007).
2017 — Alon, Ben-Eliezer and Fischer establish qualitative removal for ordered graphs and matrices: a positive copy density exists for each fixed positive distance (FOCS 2017).
2020 — Alon and Ben-Eliezer prove polynomial removal for families closed under row (or column) permutations and polynomial bounds for many entry-disjoint copies, and pose the polynomial removal question for finite families of ordered binary matrices (Problem 1.4) (Order 2020).
2022 — Gishboliner and Tomon classify polynomial induced removal for ordered graphs, a different single-order symmetric model (Combinatorial Theory 2022).
2025 — The singleton version appears as Conjecture 4.5 in the survey of Gishboliner and Shapira (Comput. Sci. Rev. 2025).
2026 — An OpenAI preprint, Polynomial removal fails for ordered binary matrices (OpenAI Math Release, September 25, 2026), claims a fixed 66×66 binary pattern for which no polynomial removal bound holds. The preprint has not been peer reviewed and its theorem is not formally verified.
Setting
A binary matrix of order n is a map A:[n]×[n]→{0,1} (in Lean BinaryMatrix n := Fin n → Fin n → Bool). For a k×k binary pattern H, an ordered copy of H in A is a pair of strictly increasing maps r,c:[k]→[n] with A(ri,cj)=H(i,j) for all i,j: zeros must match as well as ones, and rows and columns are chosen independently. NH(A) is the number of ordered copies, and A is H-free if NH(A)=0. The normalized distance to H-freeness is
where every cell may be changed in either direction.
The polynomial ordered binary matrix-removal conjecture asserts that for each fixed H there are cH,CH>0 such that NH(A)≥cHϵCHn2k whenever distH(A)≥ϵ, for all n≥1 and 0<ϵ<1.
The pattern H is explicit: with s=64 and ηb(a)=⌊a/25−b⌋mod2, the 64×64 anchor S has S(u,v)=ηv−59(u−33) for 33≤u≤64, 60≤v≤64, and S(u,v)=1[u=v] otherwise, and
H=Se1Te2Te111e201∈{0,1}66×66.
Formalization targets
Goal: no polynomial removal bound for H
For every c,C>0 there exist n≥1, ϵ∈(0,1) and a binary n×n matrix A with
distH(A)≥ϵandNH(A)<cϵCn132.
This is the "consequently" clause of Theorem 1.1 of the source, i.e. the negation of the conjecture for this fixed H (here 2k=132). The source proves more: for every h≥1, with nh=(386h+2)2h and ϵh=(386h+2)−2, an explicit Ah has distH(Ah)≥ϵh and NH(Ah)≤ϵh2−hnh132. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
Significance
The result itself. A single explicit pattern shows that ordered binary matrix removal can be super-polynomial, answering the finite-family question of Alon and Ben-Eliezer negatively and disproving the singleton conjecture recorded by Gishboliner and Shapira. It also gives a testing lower bound (Corollary 5.1): a canonical row–column sampler needs q≥exp(Ω(ϵh−1/2)) sampled positions per axis on these examples. Earlier non-polynomial examples needed a third symbol in the host; here the host is binary. The example separates hitting all existing copies (a set of 2h cells meets them) from repairing the matrix (at least 4h edits are needed).
Formalizing it. The statement is fully finite and explicit, so a formal proof would certify both the construction and the two counting estimates. The construction is intricate (tree-indexed blocks with interleaved orders, a 66-cell pattern), which is exactly where a machine check adds confidence.
Difficulty
Two estimates pull in opposite directions. The distance bound must hold against every binary repair, including repairs that create new copies elsewhere; the obvious argument — delete one cell per copy — fails because changing cells can create copies, and the source must show any repair needs at least m2 edits. The copy bound requires locating every ordered copy of the 66-cell pattern in the unedited host, not only the designated anchors, which forces a rigidity analysis of how the anchor S can embed.
Formalization scope
Matrices are Fin n → Fin n → Bool; ordered copies are pairs of StrictMono maps Fin k → Fin n, counted by copyCount. fixedH : BinaryMatrix 66 encodes H with 0-based indices (the anchor rule becomes etaBit (u-32) (v-58) for 32≤u, 59≤v).
fixedMinEdits A is the minimum Hamming distance from A to an H-free matrix (the all-zero matrix is H-free, so the minimum is attained by a genuine matrix, and the sentinel n2+1 is never selected); fixedDistance divides by n2.
The bound cϵCn132 uses Real.rpow; c,C are arbitrary positive reals, and n,ϵ,A are existentially chosen, so the statement is exactly the failure of the conjectured inequality for this H. It is weaker than the explicit quantitative family of Theorem 1.1; a stronger milestone recording nh,ϵh and the bound ϵh2−h would be welcome.
Needed infrastructure: the explicit tree matrices Ah, counting of ordered copies, and a lower bound for Hamming distance to H-freeness.
Selected references
N. Alon, E. Fischer and I. Newman, Efficient testing of bipartite graphs for forbidden induced subgraphs, SIAM J. Comput. (2007). https://doi.org/10.1137/050627915
E. Fischer and E. Rozenberg, Lower bounds for testing forbidden induced substructures in bipartite-graph-like combinatorial objects, APPROX–RANDOM 2007. https://doi.org/10.1007/978-3-540-74208-1_34
N. Alon, O. Ben-Eliezer and E. Fischer, Testing hereditary properties of ordered graphs and matrices, FOCS 2017. https://doi.org/10.1109/FOCS.2017.83
A polynomial-time construction of strong thin treesResearch Paper
Motivation
A thin spanning tree of a graph is a spanning tree that uses only a small fraction of the edges of every cut. Thin trees were introduced for the asymmetric traveling salesman problem: Asadpour, Goemans, Mądry, Oveis Gharan and Saberi showed that a thin tree of low cost can be augmented into a cheap tour, giving an O(logn/loglogn)-approximation (doi:10.1287/opre.2017.1603). Goddyn conjectured that high edge connectivity forces thin trees; the strong thin tree conjecture asks for thinness C/k in every k-edge-connected multigraph. For applications one wants not just existence but an efficient algorithm that finds such a tree, also when parallel-edge multiplicities are huge and written in binary.
Background. The maximum-entropy rounding of Asadpour et al. constructs O(logn/(kloglogn))-thin trees. Oveis Gharan and Saberi constructed O(1/k)-thin trees on planar and bounded-genus graphs (2011, doi:10.1137/1.9781611973082.75). Anari and Oveis Gharan proved existence of poly(loglogn)/k-thin trees in general (2015, arXiv:1411.4613), without a polynomial-time construction. Klein and Olver (2023, doi:10.1109/FOCS57990.2023.00011) and Klein, Olver and Yeoh (2026, doi:10.4230/LIPIcs.ICALP.2026.129) handled laminar families and near-minimum cuts. A companion OpenAI preprint claims the existence statement of the strong conjecture.
The source of this mission, an OpenAI preprint dated September 23, 2026, claims a deterministic polynomial-time construction.
Setting
Graphs are finite undirected loopless multigraphs; parallel copies count separately. For ∅=S⊊V(G), δG(S) is the multiset of edges with exactly one endpoint in S, and G is k-edge-connected if ∣δG(S)∣≥k for every such S. A spanning tree T is α-thin if ∣δT(S)∣≤α∣δG(S)∣ for all such S. Two input formats are allowed: an explicit list of labelled edge copies, or a list of endpoint pairs with multiplicities written in binary (so the number of edges can be exponential in the input length). Running time is measured in the total binary input length.
Formalization targets
Goal: Theorem 1.1 (algorithmic strong thin trees)
There is an absolute constant C and a deterministic algorithm that, given k≥1 and a k-edge-connected multigraph G on at least one vertex (in either format), returns in time polynomial in the input length a spanning tree T with
∣δT(S)∣≤kC∣δG(S)∣(∅=S⊊V(G)),
returning the empty tree for a one-vertex graph. Lean: OAI.AlgorithmicThinTrees.algorithmic_strong_thin_trees, open on the platform.
Significance
The theorem would give an algorithmic resolution of the strong thin tree conjecture: not only do C/k-thin trees exist, they can be found deterministically in polynomial time, even for exponentially many parallel edges. It also yields simultaneous cost-and-cut rounding (Corollary 7.1): from a fractional point whose mass on every cut is at least one, a tree in its support with every cut load and total cost within constant factors, with no metric assumption on costs. The order 1/k is optimal. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists.
Difficulty
Existence proofs for thin trees go through the Marcus–Spielman–Srivastava interlacing-families theorem and a fixed-point argument, neither of which is constructive: they show that some choice works without locating it. The algorithm must replace these by explicit, rational, polynomially sized computations (checked signings, rational positive semidefinite decompositions, bounded denominators) and must work with binary multiplicities, where even listing the edges is exponential. Certifying thinness on all exponentially many cuts must also be done without enumerating them.
Formalization scope
Graphs: StrongThinTree.MultiGraph n m (vertices Fin n, edges Fin m, loopless). Inputs are ExplicitInput or BinaryInput (ordered, distinct endpoint pairs with multiplicities); a binary input's edge copies are Σ i, Fin (multiplicity i).
Valid x: n≥1, k≥1 and EdgeConnected k.
The machine model is CurrentKS.Machine: a deterministic machine with finitely many binary stacks and a finite instruction table, run for a fuel bound. Inputs and outputs are self-delimiting binary encodings (CurrentKS.encodeNat).
AlgorithmicStrongThinTrees: ∃ C > 0, ∃ M a degree, 0 < a ∧ ∀ x, Valid x → after a * (len + 1)^degree steps M has halted and its output stack encodes a duplicate-free edge list forming a ThinTree C k; for n=1 the output is empty.
One machine and one polynomial serve all inputs in both formats.
Needed infrastructure: the existence theory of the companion mission, a model of deterministic computation with polynomial-time bounds, exact rational linear algebra, and constructive spectral sparsification. Contributions formalizing Proposition 2.5, Proposition 3.1, Lemma 6.1, Theorem A.1 (rational rank-one signing) or Corollary 7.1 are welcome.
OpenAI, The strong thin tree conjecture, preprint, September 23, 2026.
A. Asadpour, M. X. Goemans, A. Mądry, S. Oveis Gharan, A. Saberi, An O(log n/log log n)-approximation algorithm for the asymmetric traveling salesman problem, Oper. Res., 2017. https://doi.org/10.1287/opre.2017.1603
N. Anari, S. Oveis Gharan, Effective-resistance-reducing flows, spectrally thin trees, and asymmetric TSP, FOCS, 2015. https://arxiv.org/abs/1411.4613
O. Svensson, J. Tarnawski, L. A. Végh, A constant-factor approximation algorithm for the asymmetric traveling salesman problem, J. ACM, 2020. https://doi.org/10.1145/3424306
A spanning tree keeps a graph connected with as few edges as possible. A spanning tree is thin if, in addition, it uses only a small fraction of the edges of every cut. Thin trees were introduced as a tool for the asymmetric traveling salesman problem (ATSP): Asadpour, Goemans, Mądry, Oveis Gharan and Saberi showed that thin trees, together with cost control, can be augmented cheaply into tours, which gave an O(logn/loglogn)-approximation (doi:10.1287/opre.2017.1603). Goddyn's thin tree conjecture asks whether high edge connectivity alone forces an ε-thin spanning tree, independently of the number of vertices; the strong form asks for thinness C/k in a k-edge-connected graph.
Background. Goddyn recorded the conjecture in a 2004 problem list. The Nash–Williams–Tutte theorem (1961) gives ⌊k/2⌋ edge-disjoint spanning trees in a k-edge-connected graph (doi:10.1112/jlms/s1-36.1.445, doi:10.1112/jlms/s1-36.1.221), so each cut is used about 2/k times on average, but no single tree need be good for every cut. Oveis Gharan and Saberi proved the bound for planar and bounded-genus graphs (2011, doi:10.1137/1.9781611973082.75). Anari and Oveis Gharan obtained thinness poly(loglogn)/k in general (2015, arXiv:1411.4613), using the Marcus–Spielman–Srivastava interlacing-families method (doi:10.4007/annals.2015.182.1.8). Klein and Olver handled any prescribed laminar family of cuts (2023, doi:10.1109/FOCS57990.2023.00011), and Klein, Olver and Yeoh controlled all near-minimum cuts (2026, doi:10.4230/LIPIcs.ICALP.2026.129). Constant-factor ATSP approximations were obtained by other means (Svensson–Tarnawski–Végh 2020, doi:10.1145/3424306; Traub–Vygen 2022, doi:10.1137/20M1339313), but the thin tree question stayed unresolved.
The source of this mission, an OpenAI preprint dated September 23, 2026, claims the strong thin tree conjecture.
Setting
Let G=(V,E) be a finite undirected multigraph without loops; parallel edges are counted separately. For a nonempty proper subset ∅=S⊊V, let δG(S) be the set of edges with exactly one endpoint in S. G is k-edge-connected if ∣δG(S)∣≥k for every such S. For an edge set T⊆E, δT(S)=δG(S)∩T. A spanning tree T is α-thin if ∣δT(S)∣≤α∣δG(S)∣ for every nonempty proper S.
Formalization targets
Goal: Theorem 1.1 (strong thin trees)
There is a universal constant C>0 such that for every k≥1, every finite loopless k-edge-connected multigraph with at least two vertices has a spanning tree T with
∣δT(S)∣≤kC∣δG(S)∣(∅=S⊊V).
Lean: OAI.StrongThinTree.strongThinTree, open on the platform.
Significance
The order 1/k is optimal (two vertices joined by k parallel edges). The theorem would settle both Goddyn's thin tree conjecture and its strong form, removing the poly(loglogn) loss of Anari–Oveis Gharan. It shows that connectivity alone controls all cuts at once, and gives a structural route to ATSP integrality-gap bounds through thin trees. An algorithmic version (deterministic polynomial-time construction) is the subject of the companion mission in this family. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists.
Difficulty
Averaging over a Nash–Williams–Tutte packing controls each cut on average but not all cuts simultaneously: there are exponentially many cuts and a union bound over them loses a factor depending on n. Spectral approaches control all cuts via a matrix inequality, but spectrally thin trees need not exist when some edges have large effective resistance, which is why previous spectral arguments lost loglogn factors. One must instead keep a large tree packing on low-resistance edges through a sequence of sparsifications whose relative losses stay bounded.
Formalization scope
MultiGraph n m: vertices Fin n, edges Fin m with endpoint maps and a looplessness proof; parallel edges are distinct edges.
cut G T S: the edges of T with exactly one endpoint in S. Connected G T: every nonempty proper S is crossed by T. SpanningTree G T: T connected and every proper deletion disconnects.
EdgeConnected G k: every nonempty proper cut has at least k edges.
MainStatement: ∃ C > 0, ∀ k ≥ 1, ∀ n ≥ 2, ∀ G k-edge-connected, ∃ T spanning tree, ∀ S nonempty proper, |cut T S| ≤ (C/k)|cut G S| (real arithmetic).
Needed infrastructure: graph Laplacians and effective resistance, the Nash–Williams–Tutte theorem, the Marcus–Spielman–Srivastava mixed-characteristic-polynomial bound, and a Brouwer-type fixed point theorem (the paper proves the finite-dimensional case via Sperner's lemma). Contributions formalizing Theorem 2.3 (Nash–Williams–Tutte), Theorem 3.2, Theorem 4.1, Proposition 6.2 or Theorem A.1 are welcome.
L. A. Goddyn, Some open problems I like, problem list, 2004.
A. Asadpour, M. X. Goemans, A. Mądry, S. Oveis Gharan, A. Saberi, An O(log n/log log n)-approximation algorithm for the asymmetric traveling salesman problem, Oper. Res., 2017. https://doi.org/10.1287/opre.2017.1603
N. Anari, S. Oveis Gharan, Effective-resistance-reducing flows, spectrally thin trees, and asymmetric TSP, FOCS, 2015. https://arxiv.org/abs/1411.4613
A. W. Marcus, D. A. Spielman, N. Srivastava, Interlacing families II: mixed characteristic polynomials and the Kadison–Singer problem, Ann. of Math., 2015. https://doi.org/10.4007/annals.2015.182.1.8
Subsphere methods for memory-sample lower bounds in noiseless Gaussian regressionResearch Paper
Motivation
An exact linear equation can carry arbitrarily fine real information: d independent Gaussian equations Yt=⟨Xt,s⟩ determine a vector s∈Rd almost surely. A streaming learner that keeps only finitely many persistent states cannot retain those equations at arbitrary precision. The question is how many fresh equations such a learner needs to estimate a direction to angular accuracy ϵ when the information passed between observations is bounded in bits.
This preprint proves an explicit answer for memory o(d2): at least 2−16dlog2(1/ϵ) samples, uniformly in 0<ϵ≤1/10. With real-valued registers, randomized Kaczmarz needs only order dlog(1/ϵ) samples, so the bound shows that bounded memory cannot beat that scale.
Background
2015. Steinhardt and Duchi show memory restrictions affect statistical risk in sparse noisy regression.
2016. Steinhardt, Valiant and Wager relate bounded-memory inference to communication and statistical queries and pose a quadratic-memory versus exponential-sample question for parity learning; Raz proves the separation through finite-width branching programs.
2019. Sharan, Sidford and Valiant prove, for Gaussian covariates with uniform noise of half-width 2−d/5, memory at most d2/4 bits and Euclidean accuracy d−r, an Ω(dlogr) sample lower bound; their Section 7 uses high moments with independent copies and successive orthogonalization. Dagan, Kur and Shamir prove space lower bounds for different linear-prediction tasks.
2026. The OpenAI preprint Subsphere methods for memory-sample lower bounds in noiseless Gaussian regression (dated September 27, 2026) proves the explicit 2−16dlog2(1/ϵ) bound for exact observations. It has not been peer reviewed; the Lean goal is open on this platform.
Setting
Fix d≥2, M≥0, T≥0, and 0<ϵ≤1/10. For a signal s∈Sd−1 the observations are Xt∼N(0,Id) independent and Yt=⟨Xt,s⟩ exactly. A finite-state Gaussian stream learner reads the pairs in order; at every index its persistent state has at most 2M values. Transition and stopping rules may depend on the index, d,M,T,ϵ, the current state, the whole current pair and fresh randomness, with unrestricted computation. It stops at some τ≤T and outputs s^∈Sd−1 from the terminal state, τ and fresh randomness. A shared seed may choose the rules; seed and initial state are independent of the signal and rows. The experiment is jointly measurable.
For a linear space H and z⊥H, r>0 with ∥z∥2+r2=1, the affine subspherez+rS(H) is a test set of dimension dimH. A block of b exact Gaussian rows leaves the target, conditionally, uniform on a random residual subsphere of dimension dimH−b.
In Lean (OAI.SubsphereCurrent), learners are SeededLearner d M T Ω built from KernelLearners (Markov-kernel transitions on completed observations, states Fin (2^M)), with Admissible measurability, uniformSuccess and per-signal success.
Formalization targets
Goal: full_current_main_scope
The conjunction of the paper's main statements:
Theorem 1.2 with Corollary 1.3 (explicit noiseless precision bound). For every M(d)=o(d2) there is a threshold such that for larger d, every 0<ϵ≤1/10 and every learner with uniform-prior success at least 2/3, or success at least 2/3 at every signal,
T≥2−16dlog2(1/ϵ).
Corollary 6.3: with uniform-prior success at least 1/2, T≥cdlog2(1/ϵ) for an absolute c>0.
Theorem 6.1 (radius-weighted block estimate, with its terminal bound), Proposition 7.1 (all-affine suffix bound), Proposition 8.1 (dimension-parameterized success bound: for m-dimensional targets, jk samples and 2d2 states, Pr{∥s^−s∥≤η}≤(Cj+1η)d/32), and the beta-mixture estimate of Section 9.
Significance
The result. Theorem 1.2 gives explicit constants for the Ω(dlog(1/ϵ)) memory–sample bound with exact Gaussian observations and o(d2) memory, e.g. T≥2−16rdlog2d at accuracy d−r. The block estimates are statements about uniform measures on random affine subspheres that are independent of the learning application.
Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. Companion missions on the same family of preprints (memory and precision, posterior replicas, projection moments) share the learner model; this one is distinguished by explicit constants.
Difficulty
Conditioning on an exact Gaussian block makes the posterior of the signal singular: it is uniform on a lower-dimensional residual subsphere determined by the data. Density-based information arguments therefore fail after one block. The bound must control the success probability of the remaining computation, started from any state, averaged over every affine subsphere of large dimension, uniformly over learners that may process each real-valued pair without limit.
Formalization scope
Vector d = EuclideanSpace ℝ (Fin d), signals in the unit sphere with normalized surface measure, rows i.i.d. stdGaussian.
Thresholds: success ≥2/3 (and ≥1/2 for the Corollary 6.3 conjunct), in ℝ≥0∞; the constant 2−16 is written (2:ℝ)⁻¹ ^ 16 and the logarithm is Real.logb 2.
Block sizes are natural-number floors d/16, d/32, d/8; the fixed-length estimate uses Fin (2^(d^2)) states.
The seed space is an arbitrary probability space; randomized learners are covered by seeds.
The goal cannot be satisfied vacuously: hypotheses range over all admissible learners and the success thresholds are attainable with large T.
Needed infrastructure: Haar measure on Grassmannians or orthogonal groups, beta laws of projected directions, spherical caps, measurable selection of Borel rule versions. Contributions proving individual conjuncts are welcome.
Replacing Gaussian observations in memory-constrained inferenceResearch Paper
Motivation
A finite message chosen from data changes the conditional distribution of those data. In memory-constrained inference this matters directly: a learner observing a signal S through exact Gaussian equations keeps a finite state W, and after conditioning on W the rows that were used to select it are biased. An independent Gaussian matrix has the same unconditional law as those rows, but once its labels are revealed it need not leave the same information about S.
This preprint quantifies the cost of that replacement. For a uniform signal on the sphere and a message of entropy at most d2, replacing the actual rows by fresh independent rows increases the remaining conditional information by at most O(d). As an application, learners with o(d2) persistent bits need Ω(dlog(1/ϵ)) exact Gaussian observations to reach angular accuracy ϵ.
2015–2017. Steinhardt and Duchi establish memory-dependent minimax bounds for sparse noisy regression; Raz proves branching-program time–space lower bounds for parity learning (2016) and broader discrete problems (2017).
2016–2017. Russo and Zou bound the bias of a selected statistic by the information used for selection; Xu and Raginsky give an information-theoretic bound on generalization via a sub-Gaussian test under the product law.
2019. Sharan, Sidford and Valiant prove an Ω(dlogr) sample lower bound for Gaussian regression with small uniform noise and d2/4 bits at Euclidean accuracy d−r. Dagan, Kur and Shamir prove quadratic-space lower bounds for related linear-algebra tasks.
2026. The OpenAI preprint Replacing Gaussian observations in memory-constrained inference (dated September 27, 2026) proves the replacement comparison and its streaming consequence. It has not been peer reviewed; the Lean goal is open on this platform.
Setting
Let σ be uniform probability on Sd−1, γk the law of a k×d matrix with i.i.d. N(0,1) entries, H discrete entropy and I(⋅;⋅∣⋅) conditional mutual information, all in nats. Put
m=⌊d/10⌋,ℓ=⌊d/2⌋,r=ℓ−m.
Let S∼σ and A∼γm be independent, and let W be a countable message with an arbitrary joint law with (S,A).
In the aligned experiment, keep (S,A,W) and append an independent r-row Gaussian matrix C, so the analyst sees G1=(A;C) and G1S.
In the independent experiment, keep (S,W) and draw a fresh ℓ-row Gaussian matrix G0 independent of (S,W).
In Lean (OAI.CurrentProjection), the joint law of ((S,W),A) is a probability measure P on (Sphere d × W) × Rows (d/10) d whose (S,A) marginal is uniformSphere d ⊗ gaussianRows (d/10) d; alignedExperiment and P.fst.prod (gaussianRows ...) are the two experiments; exposedInformation is I(S;W∣G,GS) computed as a relative entropy via condKernel; shannonEntropy is H(W).
Formalization targets
Goal: Theorem 4.1 (Critical-radius comparison)
There are an absolute K and d0 such that for d≥d0 and every such countable W with H(W)≤d2,
I0(S;W∣G0,G0S)≤I1(S;W∣G1,G1S)+Kd.
Milestones
Theorem 3.1 (mixed projection moment and exact density version): for ℓ=m+r<d−1, r≥q, and a finite measure ρ on the sphere with ρ(B(z,t))≤Btℓ and ρ(B(z,t))≤Dtd−1,
Proposition 3.2 (actual-row tilt and exact-label limit).
Propositions 5.3 and 5.4 (one-level and two-label auxiliary-row comparisons).
Proposition 6.1 (averaged information increase per block, hybrid route).
Proposition 7.1 (information through a Gaussian block, fiber route) and Lemma 7.2 (two-point Gaussian fiber measure identity).
Significance
The result. Theorem 4.1 converts a statement about the actual, selection-biased rows into one about fresh rows at an additive cost of O(d), which is the step that lets block-by-block information bounds be iterated along a stream. With the residual-sphere endpoint it gives the lower bound T=Ω(dlog(1/ϵ)) for learners with o(d2) bits (Theorem 8.4, Corollary 8.7). The mixed projection moment (Theorem 3.1) is a reusable estimate on exact Gaussian projections of measures with local mass control.
Formalizing it. All results are in an unrefereed preprint, with no machine-checked proofs. The streaming theorems themselves (Theorem 8.4, Theorem 8.6, Corollary 8.7) are not among the published Lean targets and remain future work.
Difficulty
Conditioning on W biases A in a way that depends on the unknown signal, so the two experiments have different joint laws even though their (S,W) and (S,G) marginals agree. A direct comparison of densities fails because the exact label density under the actual law can be large on a selection-dependent set; controlling it requires a high moment of the projected density with the row-information charge I(A;W∣S)≤H(W) entering only with coefficient 1/q.
Formalization scope
Signals live on Metric.sphere (0 : EuclideanSpace ℝ (Fin d)) 1 with normalized surface measure; rows are Fin k → EuclideanSpace ℝ (Fin d) with stdGaussian entries.
Messages are countable types with measurable singletons (finite types for some milestones); entropies and informations are ℝ≥0∞-valued.
Row counts are d/10, d/2 - d/10, d/32, d/8, d/4, d/3 as in each source statement.
The goal is not vacuous: it quantifies over all joint laws with the stated marginal and entropy bound, and the right side is finite for many of them.
Needed infrastructure: conditional mutual information for standard Borel variables, chain rules, exact density versions of Gaussian projections, local mass bounds on the sphere. Contributions toward any milestone are welcome.
P. Mattila, Hausdorff Dimension, Orthogonal Projections and Intersections with Planes, Ann. Acad. Sci. Fenn. 1 (1975). https://doi.org/10.5186/aasfm.1975.0110
Projection moments, positive cap domination, and Riesz estimates on the sphereResearch Paper
Motivation
A linear projection can concentrate a measure even when the measure has no atoms; how much depends on how much mass sits near the affine subspaces that the projection collapses. Quantitative versions of this principle go back to the potential-theoretic projection method of Kaufman and Mattila, which relates ball-growth bounds ν(B(x,r))≤Krβ to the behaviour of projections. This preprint proves explicit, dimension-dependent versions for random exact projections and applies them to a learning question: how many noiseless Gaussian measurements ⟨xt,s⟩ does a learner with M bits of memory need to recover a unit vector s to angular accuracy ϵ?
The answer proved here is that M=o(d2) bits force T≥cdlog(1/ϵ) measurements, matching the real-valued randomized Kaczmarz scale, and more generally T≥cdlog(1/ϵ)/(1+M/d2) for every M.
Timeline
1975. Mattila relates Hausdorff dimension, orthogonal projections and ball-growth measures through inverse-distance energy averaging.
1984. Drury's affine-plane change of variables for k-plane transforms contains the simplex-volume Jacobian used in projection calculations.
2014–2016. Shamir's finite-message framework includes bounded-memory online learning; Steinhardt and Duchi (2015) prove memory-dependent minimax rates for sparse regression; Steinhardt, Valiant and Wager (2016) relate memory, communication and statistical queries; Raz (2016) proves the quadratic-memory versus exponential-sample separation for parity learning.
2019. Sharan, Sidford and Valiant prove an Ω(dlogr) sample bound for Gaussian regression with small uniform noise, d2/4 bits and Euclidean accuracy d−r, using high-moment expansions and successive orthogonalization. Dagan, Kur and Shamir prove quadratic-space bounds for two other linear-prediction tasks.
2026. The OpenAI preprint Projection moments, positive cap domination, and Riesz estimates on the sphere (dated September 27, 2026) gives three independent proofs of the Ω(dlog(1/ϵ)) bound for exact observations and o(d2) memory. It has not been peer reviewed; the Lean goal is open on this platform.
Setting
Let σ be uniform probability on Sd−1⊂Rd. A finite measure ν on Rd satisfies an all-ball mass bound with constants K,β if ν(B(x,r))≤Krβ for every ball. For an orthonormal k-frame P, P#ν is the image measure on Rk and g(P,⋅) its density. The Riesz functional of h:Sd−1→[0,1] is V(h)=supz∫h(s)∥s−z∥−d/2dσ(s).
In the finite-state regression experiment, the signal S∼σ; at each step a row xt∼N(0,Id) arrives with its exact label ⟨xt,S⟩. A learner keeps one of 2M states, may use arbitrary measurable randomized transitions of the current state and pair, stops by a deterministic horizon T, and outputs a unit vector from its terminal state, stopping index and fresh randomness. Success means arccos⟨S^,S⟩≤ϵ.
In Lean (OAI.ProjectionMoments, OAI.NoiselessRegression), learners are FiniteKernelLearner d M T (Markov-kernel transitions on completed observations, states Fin (2^M)), mixed over a seed space Ξ with probability ρ; seededSuccess is uniform-prior success; AllBallMass ν K β, coordinateDensity, frameLaw, capMeasure, rieszPotential encode the geometric objects.
Formalization targets
Goal: OAI.ProjectionMoments.main
A conjunction of the paper's results, including:
Theorem 2.4 (finite-memory precision bound). There is an absolute c>0 such that for every M(d)=o(d2), eventually in d, uniform-sphere success at least 2/3 at accuracy 0<ϵ≤1/10 forces
T≥cdlog(1/ϵ),
also under an every-signal guarantee.
Corollary 2.5, in the weakened form that M≤Ad2 gives T≥cAdlog(1/ϵ) (the paper proves T≥cdlog(1/ϵ)/(1+M/d2)).
Theorem 3.3 (integrated orthonormal-projection moment). If ν is finite, supported in B(z,R), with ν(B(x,r))≤Krβ, and k+q≤d, 0<β≤d, β−k−(q−2)≥1, then
Theorem 3.5, Corollary 3.4 and Proposition 3.7 (normalized and all-radii moments, one-block propagation), Proposition 4.1 (positive domination by countable sums of cap measures), Lemma 5.3 (projection density at deterministic offsets), and the explicit success bounds of Propositions 3.8, 4.4 and 5.4 for arbitrary M.
A bridge showing the kernel learner model agrees with the seeded deterministic learner model.
Significance
The result. The projection moment estimates are general statements about finite measures with ball-growth control and apply beyond learning. In the learning application they give three proofs, with different stopping and accuracy costs, that o(d2) bits cannot beat the dlog(1/ϵ) sample scale for exact Gaussian measurements, plus an explicit trade-off for all M.
Formalizing it. The results are in an unrefereed preprint; there is no machine-checked proof. The conjunct FixedQuadraticMemory coincides with part of the goal of the companion mission on Memory and precision in noiseless Gaussian regression, so progress here is shared.
Difficulty
Integrated density norms do not determine density values on a matrix-dependent graph, so pointwise statements need an explicitly chosen density version. The high moments of projected densities require controlling collisions of q independent points under projection, which leads to inverse affine heights whose integrability must be extracted from the ball-growth hypothesis at all scales. In the learning application, conditioning on an exact label produces a singular posterior, so arguments that track a posterior density fail.
Formalization scope
Space is EuclideanSpace ℝ (Fin d); frames are orthonormal families Fin k → E drawn by frameLaw; densities are ℝ≥0∞-valued with explicit measurable versions.
Parameters are natural-number floors (d/4, d/8, d/16); block counts appear as (T+k-1)/k.
Learners: FiniteKernelLearner with CompletedRules almost surely in the seed; success probabilities are ℝ≥0∞.
The goal has no trivial reading: each conjunct quantifies over all measures or learners satisfying the stated hypotheses, and the hypotheses are satisfiable.
Needed infrastructure: Stiefel and Haar measures, Gaussian polar decomposition of matrices, Gram–Schmidt Jacobians, spherical caps, Riesz potentials. Contributions proving individual conjuncts (for example Theorem 3.3) are welcome.
P. Mattila, Hausdorff Dimension, Orthogonal Projections and Intersections with Planes, Ann. Acad. Sci. Fenn. Ser. A I Math. 1 (1975). https://doi.org/10.5186/aasfm.1975.0110
S. W. Drury, Generalizations of Riesz Potentials and Lp Estimates for Certain k-Plane Transforms, Illinois J. Math. 28 (1984).
Localization costs and information growth for exact Gaussian observationsResearch Paper
Motivation
An exact linear observation ⟨x,S⟩ of a real signal can carry arbitrarily many bits. A finite message computed from a block of such observations cannot, but its information content is not controlled by the number of observations alone: if earlier messages have already concentrated the signal in a small region, the next block can exploit that concentration. Bounds of this kind are the engine of memory–sample lower bounds for noiseless Gaussian regression, where a learner with M bits of memory must recover a unit vector to angular accuracy ϵ from a stream of exact Gaussian measurements.
This preprint asks how to restore a geometric spread condition on the posterior while paying for the information revealed in doing so, and proves that, for a cube-shaped prior on a spherical patch, t blocks of Θ(d) exact measurements with messages of at most exp(Ad2) values reveal only OA(dt) nats.
Background
2015. Steinhardt and Duchi prove memory–sample trade-offs for noisy sparse regression.
2016. Steinhardt, Valiant and Wager formulate a memory/sample conjecture for parity learning; Raz proves a quadratic-memory versus exponential-sample separation for parities, extended to a broad class of finite problems in 2017.
2019. Sharan, Sidford and Valiant prove an Ω(dlogr) sample lower bound for Gaussian regression with small additive noise, memory at most d2/4 bits and Euclidean accuracy d−r; their Section 7 expands projection moments into independent signal copies. Dagan, Kur and Shamir prove quadratic-memory lower bounds for approximately solving a consistent linear system in random order.
2026. OpenAI preprints on exact observations: Posterior replicas and conditional information in Gaussian regression, Replacing Gaussian observations in memory-constrained inference, and the present Localization costs and information growth for exact Gaussian observations (dated September 27, 2026), which supplies several localization routes to the Ω(dlog(1/ϵ)) lower bound for o(d2) memory. None of these preprints is peer reviewed; the Lean goal is open on this platform.
Setting
Let d be large, n=d−1, k=⌊n/16⌋, m=⌊n/8⌋. The cube prior is normalized Lebesgue measure μ0 on the half-open cube Q0=[−1/(2n),1/(2n))n, and the chartϕ(z)=(z,1−∥z∥2) maps it into Sd−1. Dyadic cells of level J subdivide Q0 into 2nJ half-open subcubes of side 2−J/n.
Draw Z∼μ0. In block i=1,…,t an independent standard Gaussian k×d matrix Xi is drawn, and (Xi,Xiϕ(Z)) is observed exactly. A messageWi∈{1,…,N} is drawn from a Borel probability kernel of the block data, whose choice may depend on the preceding messages W1,…,Wi−1. Information is measured in nats by mutual information I(⋅;⋅), defined as a relative entropy.
In Lean (OAI.RepeatedLocalization), Coordinate n = Fin n → ℝ, cubePrior n is Lebesgue measure conditioned on initialCube n, chart is ϕ, a Cell n is a level J with a multi-index in Fin (2^J), a BlockRule n N is a measurable probability vector on Fin N indexed by block data, Rules n N t chooses a rule for each block from the past history, and experimentLaw rules is the joint law of (Z,W1,…,Wt).
There is an absolute c>0 such that for every C0>0 there is C with the following property, for d large. If
(2/m+e−ck)logN≤C0d,
then one can reveal nested dyadic cells Q0⊃Q1⊃⋯⊃Qt containing Z, with Qi a finite-valued measurable function of Z and W1,…,Wi, such that the augmented transcript Πt=(W1,Q1,…,Wt,Qt) satisfies
I(Z;Πt)≤Cdt,EJt≤Ct,
where Jt is the level of Qt. An alphabet of size N≤exp(Ad2) satisfies the hypothesis with C0 depending only on A.
Milestones (results from the paper's other routes)
Lemma 5.2 (finite expected regularization of a finite-relative-entropy posterior by a terminating dyadic search).
Lemma 12.1 (convexity and coercivity of the kernel potential Φ(ν)=D(ν∥σ)−∫logJνdν).
Proposition 12.6 (the potential grows by at most Cd per block).
Lemma 13.2 (inverse simplex-volume moment under a ball bound, with no support restriction).
Significance
The result. Theorem 3.2 is the first information estimate in the paper and the model for its later routes: it shows that revealing a nested dyadic cell after each block, which restores the spread condition needed by the projection estimate, costs only O(d) nats per block. Since the original message history is a function of Πt, the bound also controls the information in the messages alone. Combined with the paper's endpoint arguments this yields the lower bound T≥cdlog(1/ϵ) for learners with o(d2) bits.
Formalizing it. These results are proved only in an unrefereed preprint; no machine-checked proofs exist. The milestones are independent analytic statements (an entropy regularization, a convex potential and its drift, an inverse-volume moment) that are reusable in the companion missions on exact Gaussian observations.
Difficulty
The information a block reveals depends on how concentrated the current posterior is, and earlier messages can make it arbitrarily concentrated. Simply conditioning on messages gives no control. Revealing a localizing cell restores spread, but naming a cell itself costs information, and the count of candidate cells at depth j grows like 2nj/2; the argument must show that confinement to a depth-j cell (worth nj bits relative to the prior) pays for this, uniformly over all message rules.
Formalization scope
The prior is the image of cube volume under ϕ, not surface measure; coordinates are Fin n → ℝ, and d appears as n + 1.
Row counts and parameters are natural-number floors n / 16, n / 8. Gaussian entries are gaussianReal 0 1.
A disclosure Q : Disclosure n N t is valid when each cell map is measurable with finite range, contains Z, lies in Q0, and the cells are nested. The goal asserts existence of a valid disclosure with mutualInformation (augmentedLaw rules Q) ≤ C (n+1) t and expected final level at most Ct.
Mutual information is klDiv of the joint law against the product of marginals, valued in ℝ≥0∞.
The goal is not trivial: the trivial disclosure (always Q0) does not bound the information in arbitrary messages, and the quantifier order (absolute c, then C0, then C) matches the source.
Needed infrastructure: Gaussian projections of measures on cells, Lm density bounds, dyadic cell combinatorics, and relative-entropy chain rules. Contributions toward any milestone are welcome.
Posterior replicas and conditional information in Gaussian regressionResearch Paper
Motivation
Suppose an unknown unit vector s∈Sd−1 is observed through exact linear measurements Yj=⟨Xj,s⟩ with independent Gaussian rows Xj∼N(0,Id). If every pair is kept, d rows determine s. A learner that can keep only a bounded number of bits between measurements must compress each exact real label into a state update, and the question is how many measurements this costs for a prescribed angular accuracy ϵ. Exact labels make the question delicate: a real label has no built-in bit precision, so noise-based arguments do not apply.
This preprint attacks the question through a conditional information bound for a single block of observations: how much information about s can a finite message formed from k exact Gaussian measurements carry, beyond what an independent Gaussian projection of s (revealed only to the analyst) already reveals? Iterating such a block bound over a stream gives a memory–sample lower bound.
Timeline
1960. Watanabe introduces total correlation as a measure of multivariate dependence; Austin (2020) develops its chain rules on general probability spaces.
2015. Steinhardt and Duchi prove memory and communication lower bounds for noisy sparse linear regression.
2016–2017. Raz proves that learning parities requires quadratic memory or exponentially many samples, and extends the branching-program method to a large class of finite learning problems.
2019. Sharan, Sidford and Valiant prove an Ω(dlogr) sample lower bound for Gaussian regression with tiny uniform noise, at most d2/4 bits and Euclidean accuracy d−r, in a stated range of r. Dagan, Kur and Shamir prove quadratic-space lower bounds for two other linear-prediction tasks.
2026. Two companion OpenAI preprints treat exact observations: Memory and precision in noiseless Gaussian regression (memory Ad2, backward propagation of success bounds) and Replacing Gaussian observations in memory-constrained inference. The present OpenAI preprint, Posterior replicas and conditional information in Gaussian regression (dated September 27, 2026), gives multi-replica block bounds and derives the o(d2)-memory consequence. It has not been peer reviewed; the Lean goal is open on this platform.
Setting
Let σd be uniform probability on Sd−1. In a block experiment the signal S has law p=fσd with a Borel density 0≤f≤L. Independently draw a k×d standard Gaussian matrix A and observe (A,AS). A messageW with values in a finite set is drawn from a measurable Markov kernel of (A,AS). Finally an ℓ×d standard Gaussian matrix B is drawn independently of everything. The quantity of interest is the conditional mutual information
I(S;W∣B,BS),
in nats, and H(W) denotes the Shannon entropy of the message.
A finite-state learner with M bits reads pairs (Xj,Yj) once, in order, keeps a state in a set of size 2M, may stop at any index up to a deterministic horizon T, and outputs a unit vector from its terminal state, stopping index and fresh randomness only. Transitions and stopping may be arbitrary measurable randomized rules of the current state and current pair; shared randomness is independent of the signal and samples.
In Lean (OAI.PosteriorReplicas), sphereLaw d is normalized surface measure, gaussianRows d k is the product of stdGaussian, signalMessageLaw p κ is the law of (S,W), sideLaw ℓ appends (B,BS), conditionalInformation is the relative entropy of the joint law from the conditionally independent coupling, and messageEntropy is H(W). Learners are CompletedKernelLearner d M with Markov-kernel transitions on the completed observation space, wrapped in a JointKernelExperiment over a seed space (Ω,ρ).
Formalization targets
Goal: OAI.PosteriorReplicas.source_main
The goal is the conjunction of the paper's principal statements:
Theorem 1.1 (Gaussian replica block bound). For large d, with k=2⌊d/16⌋, t=k+1, ℓ=4k, there is an absolute C with
I(S;W∣B,BS)≤tH(W)+Cd+Clog(2+logL),
uniformly over the prior, L, and the message kernel.
Theorem 1.2 (Uniform-prior sample lower bound). There is an absolute c>0 such that for every M(d)=o(d2), eventually in d, every learner with uniform-prior success Pr{arccos⟨S^,S⟩≤ϵ}≥2/3, 0<ϵ≤1/10, has T≥cdlog(1/ϵ).
Theorem 3.3 (the finite equal-label measure identity) and the accompanying density-version statement for projected laws.
The alternative block comparisons: Theorem 5.1 (distance bins), Proposition 7.5 (Haar frames), Proposition 8.1 (synthetic Gaussian route) and Proposition 9.1 (Stiefel incidence).
Significance
The result. Theorem 1.2 shows that with o(d2) persistent bits, the dlog(1/ϵ) sample scale of real-valued Kaczmarz-type methods cannot be improved for exact Gaussian measurements, under the uniform prior and with an absolute constant. Theorem 1.1 is a reusable statement in its own right: the entropy of a message is divided by a factor proportional to d, and the dependence on the prior density bound L is only doubly logarithmic, which is what allows conditioning on rare learner states.
Formalizing it. These results appear only in an unrefereed preprint, and none has a machine-checked proof. The companion preprint Memory and precision in noiseless Gaussian regression proves a related statement for memory Ad2 by a different method; the two missions share the learner model but not the block estimates. Formalizing the goal requires conditional mutual information for general (non-discrete) random variables and the exact equal-label geometry, both of which would be reusable.
Difficulty
Conditioning on one exact observation confines the signal to a lower-dimensional section of the sphere, so posterior densities with respect to σd do not exist and density-based arguments fail. Bounding the information in the message by H(W) alone is far too weak: a message of d2 bits could then carry all relevant information. The block bound must instead account for what the analyst's independent projection already reveals, uniformly over priors with large density bounds L, since rare learner states produce such priors.
Formalization scope
Vectors are EuclideanSpace ℝ (Fin d); priors are measures on the ambient space given as (sphereLaw d).withDensity f with 0≤f≤L.
Messages are Markov kernels into Fin N with NeZero N; information quantities are ℝ≥0∞-valued relative entropies (klDiv), entropies use natural logarithms.
Row counts are natural-number floors such as 2 * (d / 16), d / 8, d / 2 as in the paper.
The streaming conjunct quantifies over all memory sequences with IsLittleO atTop M (d^2), all horizons T, all 0<ϵ≤1/10, all seed spaces and all JointKernelExperiments whose output kernel agrees almost surely with the run of the per-seed learner.
The goal cannot be met vacuously: block bounds are stated for every finite message kernel, and the streaming hypothesis (success at least 2/3) is satisfiable by learners with large T.
A complete development needs Gaussian matrices and their projections, coarea-type identities for equal labels, conditional kernels (condKernel), relative entropy chain rules, and spherical measure estimates. Contributions that isolate one conjunct (for example Theorem 3.3 or Theorem 1.1) are welcome.
It has polynomial-size arithmetic circuits when depth is unrestricted and is complete for algebraic branching programs, so it is the standard test case for the cost of restricting circuit depth. Depth-reduction theorems (Agrawal–Vinay, Koiran, Tavenas) show that any polynomial-size circuit for a degree-d polynomial can be flattened to homogeneous depth four with size NO(d); lower bounds of the form NΩ(d) at small depth are therefore exactly at the threshold that depth reduction permits, and improving them slightly would separate general circuits from formulas. Nisan and Wigderson asked for an explicit homogeneous polynomial requiring superpolynomial size at constant depth, even at depth five.
Timeline
1995. Nisan and Wigderson introduce partial-derivative measures and ask for superpolynomial homogeneous constant-depth lower bounds, even at depth five.
2014. Gupta, Kamath, Kayal and Saptharishi develop shifted partial derivatives (doi:10.1145/2629541); Kayal, Limaye, Saha and Srinivasan prove exponential bounds for homogeneous depth-four formulas.
2015. Fournier, Limaye, Malod and Srinivasan prove IMM lower bounds for restricted depth-four formulas (doi:10.1137/140990280); Bera and Chakrabarti prove a depth-five IMM lower bound with bounded bottom support (doi:10.4230/LIPIcs.CCC.2015.183).
2017. Kumar and Saraf prove dΩ(d) for homogeneous depth-four circuits computing IMMd5,d (doi:10.1137/140999335); Kumar and Saptharishi prove exponential homogeneous depth-five bounds over finite fields for a VNP family (doi:10.4230/LIPIcs.CCC.2017.31).
2021/2025. Limaye, Srinivasan and Tavenas prove superpolynomial lower bounds for all constant-depth circuits, including IMM in the low-degree regime (doi:10.1145/3734215).
These results either restrict the bottom linear forms, use a different width–degree regime, or concern a different polynomial. The source of this mission, an OpenAI preprint dated September 25, 2026, claims the sharp nΘ(n) bound in the balanced regime w=d=n with unrestricted bottom forms.
Setting
An arithmetic circuit over a field K is a finite DAG whose leaves are variables or field elements; sum gates take K-linear combinations of their inputs, product gates multiply their inputs (with multiplicity). A ΣΠΣΠΣ circuit has five layers of types +,×,+,×,+ from the output down, with a single output gate; edges join consecutive layers and bottom sums read leaves. Fan-in, fan-out and sharing are unrestricted, and bottom linear forms may involve any number of variables. The circuit is syntactically homogeneous if, with variables of degree 1, constants of degree 0 and product degrees adding, every sum gate has all inputs of the same formal degree. Size is the number of vertices, leaves included. The target is IMMn,n, of degree n in n3 variables.
Formalization targets
Goal: Theorem 1.1, Corollary 6.1 and Proposition 6.2
There is n0 such that for all n≥n0, every syntactically homogeneous ΣΠΣΠΣ circuit computing IMMn,n over C, and more generally over any field of characteristic zero, has
size≥nn/400.
Conversely, over every field and for every n≥2 there is such a circuit with
size≤2n3+rn2+rnt+1+nr−1+1≤nn+4,t=⌈n⌉,r=⌈n/t⌉.
The Lean statement OAI.Problem335.main bundles the three clauses and is open on the platform. The constant 1/400 is the paper's and is not optimized.
Significance
The theorem determines the size of homogeneous depth-five circuits for IMMn,n up to the constant in the exponent: nΘ(n). It removes the bottom-support restriction of Bera–Chakrabarti and works at the balanced width–degree point w=d=n, where the shifted-partials bounds of Amireddy et al. and the low-degree results of Limaye–Srinivasan–Tavenas do not apply directly. It answers the depth-five instance of the Nisan–Wigderson question for an explicit polynomial in VP. It does not give superpolynomial bounds for general circuits.
The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. The upper-bound clause is elementary and a natural first formal target; the lower bound requires a new rank measure and its estimates.
Difficulty
Depth-five circuits with unrestricted bottom linear forms can use linear forms involving all n3 variables, which defeats measures that rely on bottom forms having small support (the Bera–Chakrabarti approach) or on set-multilinearization with degree-dependent losses (which are too costly when d=w). Partial-derivative and shifted-partial measures applied directly give bounds that degrade with the bottom fan-in. One needs a measure that is small for every product of homogeneous low-degree polynomials of arbitrary support and large for IMMn,n.
Formalization scope
Depth5Circuit K n stores the leaves (D5Leaf: a scalar or a variable index in Fin n × Fin n × Fin n), bottom sums (lists of coefficient–leaf pairs), lower products (lists of bottom gates), middle sums, upper products, and one output sum, with explicit formal degrees and homogeneity constraints at every sum gate; empty sums have degree 0.
circuitSize counts leaves plus all gates plus the output gate; circuitValue evaluates to an MvPolynomial.
imm K n is the (0,0) entry of the ordered product of the n matrices Xij(t).
The lower bound is stated over ℂ and, with a threshold chosen before the field, over every Field with CharZero; the upper bound over every Field, with the explicit upperGateBound.
A complete development needs multivariate polynomial algebra, the derivative-multiplication operator g[k,m](∂V,U) and its rank, an integral (Bargmann–Fock type) moment estimate over C, and a transfer to characteristic zero via integer minors. Contributions formalizing Proposition 6.2 (the upper bound) and Proposition 3.1 (the circuit-side rank bound) are welcome.
N. Limaye, S. Srinivasan, S. Tavenas, Superpolynomial lower bounds against low-depth algebraic circuits, J. ACM, 2025. https://doi.org/10.1145/3734215
P. Amireddy, A. Garg, N. Kayal, C. Saha, B. Thankey, Low-depth arithmetic circuit lower bounds: bypassing set-multilinearization, ICALP 2023. https://doi.org/10.4230/LIPIcs.ICALP.2023.12
Generalized Star Height at Most ThreeResearch Paper
Motivation: how many nested stars does a regular language need?
A regular expression describes a set of words using letters, union, concatenation and the Kleene starP∗ (any finite repetition of words from P). The star height of an expression is the depth of nesting of its stars, and it measures how many layers of unbounded repetition a regular language genuinely needs. For ordinary expressions this hierarchy is infinite. Allowing complement as an additional operation changes the picture: Boolean conditions can replace some layers of repetition, and the generalized star-height problem asks how far this goes. Whether every regular language has generalized star height at most some fixed number — and in particular whether one star always suffices — has been one of the longest-standing questions in the algebraic theory of automata.
Timeline
1963 — Eggan connects ordinary star height with the cycle structure of transition graphs and raises the question of its unboundedness (Michigan Math. J. 1963).
1965 — Schützenberger characterizes the star-free languages (generalized height 0) as those recognized by finite aperiodic monoids (Inform. Control 1965).
1966 — Dejean and Schützenberger show that ordinary star height is unbounded already over a two-letter alphabet (Inform. Control 1966).
1992 — Pin, Straubing and Thérien prove generalized height at most one for languages recognized by finite nilpotent groups of class two and for further monoid classes (Inform. Comput. 1992, Theorems 7.3 and 7.8).
2002 — Straubing distinguishes the questions "is generalized star height bounded?" and "is it at most one?" in his account of the problem (LATIN 2002, p. 537).
2016–2017 — Bourne and Ruškuc prove height-one bounds for subword-counting languages with factors of length at most three (Theor. Comput. Sci. 2016); Bourne extends this to arbitrary fixed factors in his thesis (St Andrews, 2017, hdl:10023/12024).
2026 — Companion OpenAI preprints prove uniform bounds of thirteen (Finite Monoid Computations and a Uniform Generalized Star-Height Bound) and four (Generalized Star Height at Most Four).
2026 — The OpenAI preprint Generalized Star Height at Most Three (OpenAI Math Release, September 25, 2026) claims the bound three. It has not been peer reviewed and its theorem is not formally verified. Whether height one always suffices remains open; no language of generalized height greater than one is known.
Setting
Fix a finite alphabet Σ and let Σ∗ be the set of finite words. A generalized regular expression over Σ is built from the constants 0 (denoting ∅) and 1 (denoting {ε}), single letters a∈Σ, union P∪Q, concatenation PQ, complement ¬P (taken in Σ∗), and star P∗. Its height is defined by
For a regular language L⊆Σ∗, the generalized star heighthΣ(L) is the least height of an expression over Σ denoting L.
In Lean (namespace OAI.GeneralizedStarHeight), expressions are an inductive type Expression Alphabet with exactly these seven constructors, Expression.language interprets them in Mathlib's Language Alphabet (complement is Language complement, i.e. relative to all words), Expression.height is the recursion above, and HasHeightAtMost L n means some expression has language L and height at most n.
Formalization targets
Goal: generalized star height at most three (Theorem 1.1)
For every finite alphabet Σ and every regular language L⊆Σ∗,
hΣ(L)≤3.
The goal is published on the platform with status Open.
Significance
The result itself. Before 2026 it was not known whether generalized star height is bounded at all; all positive results covered restricted families of monoids or languages. Theorem 1.1 gives a uniform bound independent of the alphabet and of the recognizing automaton, settling the boundedness question. It leaves open the sharper question of whether height one always suffices: no language is known to require height two. A uniform bound also implies that the hierarchy of generalized heights has at most four nonempty levels, which narrows where any separating example must be sought.
Formalizing it. The statement is short and fully elementary, but the proof composes many constructions (finite-monoid recognition, prefix codes of episodes, split identities, marker scales) whose height accounting is error-prone. A formal proof would certify the boundedness theorem itself. Mathlib already has regular languages (Language.IsRegular) and ordinary regular expressions; this mission adds generalized expressions with complement and their height.
Difficulty
The classical lower bounds for ordinary star height do not transfer once complement is allowed, and complement can simulate many but not obviously all counting arguments. The natural approach — write each fiber of a morphism from Σ∗ to a finite monoid by an expression that simulates the monoid computation letter by letter — needs one star per level of the computation's dependence on earlier history, and the depth of this dependence grows with the monoid. Group components are the difficulty: aperiodic monoids give height zero, but counting modulo n and nonabelian group computations require stars, and a uniform bound must handle arbitrary finite groups nested inside arbitrary monoids without the number of stars growing with their size.
Formalization scope
The alphabet is any Type u with [Finite Alphabet]; regularity is Mathlib's Language.IsRegular (acceptance by a finite-state DFA).
Expressions must use letters of the same alphabet, so no auxiliary letters may be introduced; complement is relative to all words over that alphabet.
height charges 1 only for stars; complement, union and concatenation are free, exactly as in the source. Since HasHeightAtMost asks only for existence of an expression, no bound on expression size or computability is claimed, matching the source's remark that the construction bounds nesting only.
Needed infrastructure: recognition of regular languages by finite monoids, prefix codes and unique factorization, and closure of bounded-height expressions under Boolean operations. The generalized-expression layer is reusable for the companion bounds (four and thirteen) and for formal work on star-free languages.
T. Bourne and N. Ruškuc, On the star-height of subword counting languages and their relationship to Rees zero-matrix semigroups, Theor. Comput. Sci. 653 (2016). https://doi.org/10.1016/j.tcs.2016.09.024
T. Bourne, Counting subwords and other results related to the generalised star-height problem for regular languages, PhD thesis, University of St Andrews, 2017. https://hdl.handle.net/10023/12024
Variable-dimension Weisfeiler–Leman equivalence on general and subcubic graphsResearch Paper
Motivation
Weisfeiler–Leman (WL) refinement compares two graphs by repeatedly refining colors of ordered vertex k-tuples. For every fixed dimension k this is a polynomial-time procedure, with running time nO(k). When k is part of the input, that computation is no longer polynomial, and the complexity of deciding the outcome becomes a question in its own right. Seppelt (2024) proved coNP-hardness and recorded Berkholz's question whether the problem is EXPTIME-complete.
This preprint answers that question for the joint-update convention: deciding k-WL equivalence of two explicit graphs with k in binary is EXPTIME-complete, even on connected graphs of maximum degree three.
Background
1968. Weisfeiler and Leman introduce the refinement method.
1982. Luks shows isomorphism of graphs of bounded degree is decidable in polynomial time.
1992. Cai, Fürer and Immerman construct degree-three graphs with small color classes that remain indistinguishable with linearly many counting variables.
2019. Kiefer and Neuen record the joint-update convention and its bijective (k+1)-pebble game characterization.
2024–2025. Seppelt, and independently Lichter, Raßmann and Schweitzer, prove coNP-hardness of WL equivalence with the dimension as input. Grohe, Lichter, Neuen and Schweitzer compress CFI graphs to obtain long refinement sequences.
2026. The OpenAI preprint Variable-dimension Weisfeiler–Leman equivalence on general and subcubic graphs (dated September 25, 2026) proves EXPTIME-completeness; companion preprints treat identification and fixed-dimension time lower bounds. It has not been peer reviewed; the Lean goal is open on this platform.
Setting
Graphs are finite, simple, undirected and uncolored, given by adjacency matrices. In the joint-update convention a k-tuple's initial color records equalities and adjacencies among its entries; each round adjoins to the old color the multiset, over replacement vertices z, of the vector of k old colors obtained by replacing each coordinate in turn by z. Color names are common to both graphs, and G≡kH means their k-tuple color histograms agree at every round.
The language WL consists of encodings (G,H,k) with k≥2 in binary and G≡kH. The language SubWL additionally requires G and H to be connected, of the same positive order, and of maximum degree at most three. Malformed encodings are excluded.
In Lean (OAI.VariableWL), Graph is a SimpleGraph on Fin order, color and histogram implement the joint update by recursion on rounds, pairCode concatenates the two graph codes (order header plus row-major matrix) and the code of k, and complexity classes are defined from an explicit deterministic Turing machine model with OutputsWithin, InEXPTIME, PolytimeReduces and EXPTIMEComplete.
Formalization targets
Goal: Theorem 1.1
Both WL and SubWL are EXPTIME-complete under deterministic polynomial-time many-one reductions:
WL,SubWL∈EXPTIME,L≤pWL and L≤pSubWL for every L∈EXPTIME.
Significance
The result. Theorem 1.1 resolves the question recorded by Seppelt and strengthens the known coNP-hardness to EXPTIME-completeness. The subcubic case is notable because isomorphism of bounded-degree graphs is polynomial-time (Luks), yet equivalence under refinement at a supplied dimension remains EXPTIME-complete for degree three; nonisomorphic graphs can be equivalent. Corollary 8.3 shows hardness persists with k in unary.
Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. The uniform computation interface developed here is reused by the companion identification paper, so a formalization would serve both missions.
Difficulty
Membership requires showing that the dimension can be capped before allocating tuple tables (Lemma 2.2), since k may exceed the graph order. Hardness requires simulating an arbitrary exponential-time computation by a graph pair whose WL equivalence at a polynomially encoded dimension reflects acceptance. Because the number of address coordinates grows with the input, fixed-dimension constructions with dimension-dependent constants do not give a uniform polynomial-time reduction, and in the subcubic case colors must be realized by uncolored degree-three gadgets that a winning strategy still recognizes.
Formalization scope
Graphs: SimpleGraph (Fin order); Subcubic bounds every vertex degree by three; SubWL also demands positive equal orders and connectivity.
Equivalence quantifies over all rounds s; colors are nested Multiset types.
Dimension k≥2 is encoded in binary after a unary length header.
The Turing machine model is explicit; EXPTIME bounds are 2c(n+1)d and reductions run in c(n+1)d steps.
The statement is not trivial: both membership and hardness are required for both languages.
Needed infrastructure: the bijective game characterization (Lemma 2.4), product-circuit compilation (Proposition 3.2), the general and subcubic realizations (Propositions 5.1 and 7.1) and the uniform compiler (Proposition 8.2). Contributions toward any of these are welcome.
J.-Y. Cai, M. Fürer, N. Immerman, An Optimal Lower Bound on the Number of Variables for Graph Identification, Combinatorica 12 (1992). https://doi.org/10.1007/BF01305232
M. Grohe, M. Lichter, D. Neuen, P. Schweitzer, Compressing CFI Graphs and Lower Bounds for the Weisfeiler–Leman Refinements, J. ACM 72 (2025). https://doi.org/10.1145/3727978
Unconditional time lower bounds for Weisfeiler–Leman equivalenceResearch Paper
Motivation
The Weisfeiler–Leman (WL) method colors k-tuples of vertices by repeatedly recording their local extension patterns; two graphs are k-WL equivalent when the stable color histograms agree. For each fixed k the direct algorithm runs in time nO(k): there are nk tuples and polynomially many refinement rounds. The question is whether the growing exponent is necessary for any algorithm deciding the equivalence relation, not just for implementations of refinement.
This preprint proves that it is, unconditionally: for every sufficiently large fixed k, every deterministic sequential decider for k-WL equivalence needs time nck at every sufficiently large graph order, without assuming the Exponential Time Hypothesis.
Background
1966. Hennie and Stearns use padded machine indices and clocked self-simulation in their time-hierarchy proof.
1968. Weisfeiler and Leman introduce the refinement method.
1992. Cai, Fürer and Immerman's parity constructions establish limits of bounded-variable graph identification.
1996. Hella introduces the bijective pebble game characterizing counting-logic equivalence.
1999. Grohe proves equivalence in finite-variable logics is complete for polynomial time.
2013. Berkholz proves unconditional time lower bounds with exponent linear in the number of pebbles for existential pebble games.
2024–2025. Seppelt, and Lichter, Raßmann and Schweitzer, prove coNP-hardness of WL equivalence when the dimension is part of the input. Grohe, Lichter, Neuen and Schweitzer prove Ωk(nk/2) lower bounds on the number of refinement rounds via compressed CFI graphs; such bounds do not constrain other algorithms deciding the equivalence.
2026. The OpenAI preprint Unconditional time lower bounds for Weisfeiler–Leman equivalence (dated September 25, 2026) proves the bound stated below. It has not been peer reviewed; the Lean goal is open on this platform.
Setting
Graphs are finite, simple, undirected and uncolored, given as n×n adjacency matrices. For a k-tuple, the initial color records coordinate equalities and adjacencies. Each refinement step keeps the old color and adds, in the joint convention, the multiset over vertices z of the k-vectors of colors obtained by replacing each coordinate by z; in the separate convention, one such multiset per coordinate. Two n-vertex graphs are k-WL equivalent if their color histograms agree at every round.
A decider for a convention and dimension k is a deterministic machine that halts on every encoded pair of n-vertex graphs and accepts exactly the equivalent pairs. Its worst-case timeTA(n) is the maximum running time over pairs of n-vertex graphs (optionally restricted to connected graphs of diameter at most two).
In Lean (OAI.WLTime), Graph n is a symmetric loopless Boolean matrix on Fin n, tupleColor and histogram define both conventions by recursion on rounds, Equivalent compares all rounds, encodePair encodes n and both matrices, and machines are either multitape Turing machines (TM) or logarithmic-word RAMs (RAM) whose word operations are themselves implemented by Turing machines in time polynomial in the word length.
Formalization targets
Goal: Theorem 1.1
There are absolute constants c>0 and k0 such that for every fixed k≥k0, either convention, either input class (all graphs, or connected graphs of diameter at most two) and every correct deterministic decider A in either machine model, there is n0=n0(A,k) with
TA(n)≥nckfor every n≥n0.
The exponent constant c is independent of k and of the program; the threshold n0 may depend on both. The bound holds at every large order, not only infinitely often.
Significance
The result. Theorem 1.1 rules out any running time f(k)ng(k) with g(k)=o(k), unconditionally. Earlier lower bounds either concerned the number of refinement rounds, assumed ETH, or treated the dimension as part of the input (coNP- and EXPTIME-hardness), which does not give a fixed-dimension exponent. It covers both standard update conventions and the restricted class of diameter-two graphs.
Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. The Lean statement fixes explicit machine models, so a proof would include a verified padded diagonalization (Theorem 5.2), a verified computation-to-graph reduction (Theorem 4.3) and a verified compressed consistency construction (Theorem 3.2).
Difficulty
Unconditional time lower bounds in concrete models are rare; the only general technique is diagonalization, which yields hard languages but not hard natural problems. The proof must therefore transfer a diagonal language to WL equivalence through a reduction that is efficient enough to preserve an exponent linear in k. A polynomial-time computation with exponent proportional to k has too many addressed locations to list in a small reduction, and local consistency is symmetric whereas a computation must propagate information forward without forcing false predecessors to become true.
Formalization scope
Decides A c k p requires halting and correctness on every pair in the input class at every order n; worstTime is a Finset.sup over pairs in the class.
Diameter two includes n>0 and every pair of vertices equal, adjacent, or with a common neighbour (hence connected).
Turing machines have finitely many tapes, states and symbols; RAM words have O(log(n+2)) bits, and RAM instructions are fixed finite programs whose word operations carry a polynomial-time implementation.
Time is a natural number; the bound nck is compared in ℝ.
The statement is not vacuous: correct deciders exist (direct refinement), so the conclusion constrains real algorithms.
Needed infrastructure: bijective pebble games and their equivalence with refinement (Lemma 2.3), Turing machine simulation and clocking, and the graph constructions of Sections 3–4. Contributions toward any of these components are welcome.
J.-Y. Cai, M. Fürer, N. Immerman, An Optimal Lower Bound on the Number of Variables for Graph Identification, Combinatorica 12 (1992). https://doi.org/10.1007/BF01305232
M. Grohe, M. Lichter, D. Neuen, P. Schweitzer, Compressing CFI Graphs and Lower Bounds for the Weisfeiler–Leman Refinements, J. ACM 72 (2025). https://doi.org/10.1145/3727978
M. Lichter, S. Raßmann, P. Schweitzer, Computational Complexity of the Weisfeiler–Leman Dimension, arXiv:2402.11531, 2024. https://arxiv.org/abs/2402.11531
T. Seppelt, An Algorithmic Meta Theorem for Homomorphism Indistinguishability, MFCS 2024.
The complexity of identifying a graph by Weisfeiler–Leman refinementResearch Paper
Motivation
The Weisfeiler–Leman (WL) algorithm refines colors of vertex tuples to test graph isomorphism, and its dimension k controls how much tuple information is used. A graph's Weisfeiler–Leman dimensionWLdim(G) is the least k for which k-WL refinement identifiesG, i.e. distinguishes it from every non-isomorphic graph. This is a standard measure of the descriptive complexity of an individual graph, tied to counting logics and pebble games. The question here is how hard it is to compute: given G and k, decide whether WLdim(G)≤k.
Identification differs from testing whether a given pair of graphs is equivalent: it quantifies over every possible comparison graph. The preprint shows the problem is EXPTIME-complete when k is part of the input.
Background
1968. Weisfeiler and Leman introduce the refinement method.
1992. Cai, Fürer and Immerman relate WL to counting logic and pebble games and construct parity graphs needing linear dimension.
2017. Arvind, Köbler, Rattan and Verbitsky prove P-hardness of identification by color refinement (dimension one).
2019. Kiefer and Neuen give a game formulation used to analyze WL decompositions.
2024. Seppelt proves coNP-hardness of variable-dimension pair equivalence.
2025. Lichter, Raßmann and Schweitzer prove P-hardness of identification for each fixed k≥2 and NP-hardness when the dimension is part of the input, including on simple uncolored graphs; they also prove coNP-hardness of pair equivalence independently. Grohe, Lichter, Neuen and Schweitzer introduce compressed CFI graphs for round lower bounds.
2026. The OpenAI preprint The complexity of identifying a graph by Weisfeiler–Leman refinement (dated September 25, 2026) proves EXPTIME-completeness, building on the companion preprint on variable-dimension WL equivalence. It has not been peer reviewed; the Lean goal is open on this platform.
Setting
All graphs are finite, simple, undirected and uncolored. For k≥2 the joint-update convention is used: a k-tuple starts with its equality and adjacency type, and each round adjoins the multiset over vertices z of the vector of colors obtained by replacing each coordinate by z. For k=1 ordinary color refinement is used. Colors are shared between graphs. G≡kH means the tuple-color histograms agree at every round. k-WL identifiesG if G≡kH implies G≅H for every graph H, and WLdim(G) is the least positive such k.
The decision problem takes a nonempty graph G by its adjacency matrix and a positive integer k in binary, and asks whether WLdim(G)≤k; malformed inputs are rejected.
In Lean (OAI.WLIdentification), Graph is an order with a symmetric loopless Boolean adjacency on Fin order; Equivalent, Identifies and WLdim follow the definitions above; inputs are bit words consisting of a unary order header, the row-major matrix and the binary dimension; complexity classes are defined from an explicit deterministic single-tape Turing machine model (Machine, run, DecidesWithin, InEXPTIME, PolytimeManyOne, EXPTIMEComplete).
Formalization targets
Goal: Theorem 1.1
The language
{⟨G,k⟩:G nonempty,k≥1,WLdim(G)≤k}
is EXPTIME-complete under deterministic polynomial-time many-one reductions: it is decidable in time 2C(n+1)d, and every EXPTIME language reduces to it in polynomial time.
Significance
The result. Theorem 1.1 settles the complexity of the input-dimension identification problem, strengthening the NP-hardness of Lichter, Raßmann and Schweitzer to EXPTIME-completeness. By Corollary 7.3 hardness persists with k in unary, so it does not come from exponentially large numerical dimensions.
Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. A formal proof would include a verified reduction from arbitrary exponential-time Turing machine computations to graphs, and a verified upper bound for WL identification. The Turing-machine model and the WL definitions in the Lean statement are reusable for the companion missions on WL equivalence.
Difficulty
Hardness must handle the all-mates quantifier: an encoding of a computation into a graph must ensure that every graph H that is k-WL equivalent to it is isomorphic to it exactly when the computation accepts. Local recognition of gadgets, as in earlier NP-hardness proofs, shows each incidence piece of H has an allowed pattern, but the encoding here admits a whole family of shifted constraints, and one must show every shift arising from an equivalent mate lifts to a single global isomorphism on accepting instances. Membership in EXPTIME is also not immediate, since identification quantifies over infinitely many comparison graphs.
Formalization scope
Graphs are Fin n-indexed Boolean adjacency matrices; the problem language requires a nonempty graph, a binary word with leading bit true, and a positive value.
WLdim G is sInf of the positive identifying dimensions; this set is nonempty for finite graphs (dimension equal to the order identifies), so the infimum is not the default value.
Time is counted in steps of the explicit Turing machine on the input length; EXPTIME uses bounds 2C(n+1)d and reductions use bounds C(n+1)d.
The goal is not trivial: membership in EXPTIME and hardness under the explicit machine model are both required.
Needed infrastructure: WL refinement monotonicity, pebble games or an equivalent characterization, CFI-type gadget constructions, and Turing-machine simulation. Contributions toward the upper bound (Proposition 7.1) or the reconstruction results of Sections 3–5 are welcome.
J.-Y. Cai, M. Fürer, N. Immerman, An Optimal Lower Bound on the Number of Variables for Graph Identification, Combinatorica 12 (1992). https://doi.org/10.1007/BF01305232
V. Arvind, J. Köbler, G. Rattan, O. Verbitsky, Graph Isomorphism, Color Refinement, and Compactness, Computational Complexity 26 (2017).
T. Seppelt, An Algorithmic Meta Theorem for Homomorphism Indistinguishability, MFCS 2024.
M. Grohe, M. Lichter, D. Neuen, P. Schweitzer, Compressing CFI Graphs and Lower Bounds for the Weisfeiler–Leman Refinements, J. ACM 72 (2025). https://doi.org/10.1145/3727978
S. Kiefer, D. Neuen, The Power of the Weisfeiler–Leman Algorithm to Decompose Graphs, MFCS 2019.
Finite tensor savings and exact Fourier circuitsResearch Paper
Motivation
The discrete Fourier transform of length n is computed by the fast Fourier transform with O(nlogn) arithmetic operations, and this has been the benchmark since Cooley and Tukey (1965). Whether Ω(nlogn) operations are necessary is one of the basic open questions of algebraic complexity theory. Lower bounds of order nlogn are known only under restrictions on the algorithm: bounded coefficients, unitary 2×2 gates on exactly n registers, or bounded conditioning of intermediate maps. In the unrestricted model of linear circuits, where coefficients are arbitrary complex numbers and only arithmetic operations are counted, the question remained open. This mission concerns that unrestricted question.
1973. Morgenstern proves an Ω(nlogn) lower bound for linear circuits with bounded coefficients (doi:10.1145/321752.321761).
2013–2014. Ailon proves lower bounds for 2×2 unitary gate models and for well-conditioned computations (arXiv:1305.4745, arXiv:1403.1307).
2023. Alman and Rao improve the leading constants for power-of-two transforms via matrix non-rigidity (doi:10.1145/3564246.3585188).
2025. Alman and Li characterize asymptotic sizes of depth-two circuits for Kronecker powers (arXiv:2509.14489).
The source of this mission, an OpenAI preprint dated September 25, 2026, claims that the Ω(nlogn) lower bound fails in the unrestricted complex linear-circuit model.
Setting
For n≥2 let ζn=e2πi/n and Fn=(ζnjk)0≤j,k<n. A linear circuit of length n has inputs x0,…,xn−1 and the constant 0, followed by a finite sequence of gates. Each gate computes u+v, u−v or λu from previously available values u,v, where λ∈C is a fixed coefficient; each gate costs one. Values may be reused arbitrarily, and the n outputs are designated available values. The circuit computesFn if its outputs equal Fnx for every x∈Cn. Coefficients may depend on n and have no bound on size or description; depth, storage and conditioning are unrestricted. Let L(n) be the minimum number of gates.
Formalization targets
Goal: Theorem 1.1
n→∞liminfnlog2nL(n)=0,
equivalently: for every c>0 and every N0≥2 there are n≥N0 and an exact circuit for Fn with fewer than cnlog2n gates. The Lean statement OAI.ExactFourier.main_theorem is this second form and is open on the platform.
The statement does not assert an upper bound for every length, a uniform construction, or anything about numerical stability. A companion OpenAI preprint gives a quantitative all-length bound in a model that also charges coefficient preparation; that result is not part of this mission.
Significance
The theorem refutes the assertion that L(n)≥cnlog2n for some fixed c>0 and all large n in the unrestricted linear model. It shows that the known lower bounds necessarily depend on their restrictions (bounded coefficients, conditioning, unitary gates). The mechanism, a single finite tensor saving amplified through tensor powers, is a general tool: one strict improvement over the standard axis-by-axis algorithm for one tensor power of one nonmonomial matrix yields an exponent improvement for all tensor powers.
The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. The existence part of the argument is non-constructive (it proceeds by contradiction through price functions and compactness), so a formal proof is a meaningful check.
Difficulty
Leading-constant improvements of the FFT do not change the nlogn scale, and every classical structural algorithm (Cooley–Tukey, Good–Thomas, chirp) has that scale. A gain in the exponent of the logarithm needs a saving that compounds across many tensor factors; but a saving for one tensor power of a small matrix does not obviously transfer to Fourier matrices of growing length, because Fourier factorizations introduce diagonal twiddle factors and change the coordinate set. In addition, the existence of a single finite saving is itself not exhibited explicitly and must be proved.
Formalization scope
Gate w is add i j, sub i j or scale c i with c : ℂ, referencing the w values available so far.
Program n k is a list of k gates in topological order; values 0,…,n−1 are the inputs and value n is the constant 0 (via Fin.snoc x 0).
Circuit n has size, a program of that size, and outputs : Fin n → Fin (n+1+size); output selection is free.
fourierMatrix n j k = zeta n ^ (j*k) with zeta n = exp(2πi/n); Computes is equality with mulVec for every input.
MainStatement: for every real c>0 and N0≥2 there are n≥N0 and a computing circuit with size < c * n * logb 2 n.
A complete development needs tensor products of matrices and circuits, the Chinese Remainder (Good–Thomas) identification of Frs with Fr⊗Fs for coprime r,s, a Toeplitz/Vandermonde factorization of Fr on its own coordinates, and the price-function existence argument (separation, compactness, feedback). Contributions formalizing Lemma 2.3 (tensor amplification) and Proposition 3.4 (transfer of a finite win to Fourier circuits) are natural first steps.
N. Ailon, A lower bound for Fourier transform computation in a linear model over 2×2 unitary gates, preprint, 2013. https://arxiv.org/abs/1305.4745
N. Ailon, An Ω((nlogn)/R) lower bound for Fourier transform computation in the R-well conditioned model, preprint, 2014. https://arxiv.org/abs/1403.1307
A Polynomial-Time 2-Approximation for Shortest Common SuperstringResearch Paper
Motivation: approximating the shortest common superstring
Given a finite collection S of strings, the shortest common superstring (SCS) problem asks for a shortest string T that contains every member of S as a contiguous substring. It is a basic model of sequence assembly (reconstructing a long DNA sequence from overlapping fragments) and of data compression, and it is a standard test problem for approximation algorithms. Computing the optimum exactly is hard — Blum, Jiang, Li, Tromp and Yannakakis showed the problem is MAX SNP-hard, so it has no polynomial-time approximation scheme unless P = NP (Blum et al., J. ACM 1994) — so the natural question is the best constant factor achievable in polynomial time. For decades the target has been factor 2: the classical Greedy conjecture asserts that repeatedly merging the pair with maximum overlap achieves it.
Timeline
1988 — Tarhio and Ukkonen propose the factor-2 conjecture for the maximum-overlap Greedy procedure (Theor. Comput. Sci. 1988).
1994 — Blum, Jiang, Li, Tromp and Yannakakis give the first constant-factor algorithm a polynomial-time 3-approximation (J. ACM 1994).
1997 — Breslauer, Jiang and Jiang use rotations of periodic strings to control overlaps (J. Algorithms 1997).
2013 — Mucha obtains 2+11/23 via Lyndon words (SODA 2013).
2019/2020 — Golovnev, Kulikov, Logunov, Mihajlin and Nikolaev introduce the all-substrings hierarchical graph and the Collapsing conjecture (APPROX/RANDOM 2019; arXiv:1809.08669).
2023 — Englert, Matsakis and Veselý obtain (14+67)/9<2.466 (ISAAC 2023).
2026 — Chukhin, Kulikov, Mihajlin and Smal report a 7/3-approximation (ECCC TR26-157); Shibata reports a counterexample to the Greedy conjecture with ratio at least 9/4 (arXiv:2609.01365).
2026 — An OpenAI preprint, A Polynomial-Time 2-Approximation for Shortest Common Superstring (OpenAI Math Release, September 24, 2026), claims a deterministic polynomial-time algorithm with ratio 2. The preprint has not been peer reviewed and its theorem is not formally verified.
Setting
A string is a finite list of symbols; a string s is a substring of T if T=usv for some strings u,v (the empty string is a substring of everything). For a finite list S of strings, a common superstring is a string T having every s∈S as a substring, and
OPT(S)=min{∣T∣:T is a common superstring of S},
where ∣T∣ counts symbols. The alphabet is unbounded: each symbol is given by an explicit binary label, and the input is measured by its total encoded bit length N. An algorithm runs in polynomial time if its running time on a bit-level machine is bounded by a polynomial in N.
In Lean (namespace OAI.Superstring), a symbol is List Bool, a word is a list of symbols, and an instance is a list of words. Substring containment is Mathlib's infix relation <:+:, opt S is the infimum of lengths of common superstrings, and HasPolynomialImplementation f asks for a Mathlib Turing.TM2ComputableInPolyTime certificate for f with respect to an explicit self-delimiting binary encoding of instances and outputs, with every stack alphabet finite.
Formalization targets
Goal: a polynomial-time 2-approximation (Theorem 1.1)
There is a function f from instances to words, computable in polynomial time in the encoded input length, such that for every instance S
f(S)is a common superstring of Sand∣f(S)∣≤2OPT(S).
The goal is published on the platform with status Open.
Significance
The result itself. Factor 2 has been the conjectured benchmark for SCS since 1988, and the best proved polynomial-time ratio before this preprint was 7/3 (reported in 2026). Theorem 1.1 reaches factor 2 with a new algorithm rather than with Greedy, which a 2026 preprint reports does not achieve factor 2.
Formalizing it. The statement mixes three components that are each easy to get subtly wrong on paper: the correctness of the output (contiguous coverage of every input), the ratio against the unrestricted optimum, and a running-time bound measured in bits, with symbols of arbitrary label length. The formal statement pins down all three with an explicit machine model. A complete formalization requires both the combinatorial ratio proof and a verified polynomial-time implementation on Mathlib's stack-machine model, which is substantial reusable infrastructure for complexity statements in Lean.
Difficulty
The classical approach builds the overlap (distance) graph, takes a minimum-weight cycle cover as a lower bound, and then opens and concatenates the cycles; the cost of joining cycles is what has kept ratios above 2. Greedy, the natural candidate for factor 2, is reported to fail. Any factor-2 algorithm needs a lower bound on OPT that is tight enough that the cost of connecting all the pieces can be charged to the lower bound a second time without double-counting, uniformly over periodic and highly repetitive inputs. The polynomial running time must also be established at the bit level, with symbols of unbounded encoded length.
Formalization scope
Instances are List (List (List Bool)): duplicates and empty strings are allowed, and symbols are arbitrary bit lists, so the alphabet is unbounded.
Coverage is contiguous substring containment (List.IsInfix), not subsequence containment.
opt is a natural-number sInf; the set is nonempty because the concatenation of all inputs is a common superstring, so the junk value is never used. The ratio is measured in symbols.
Polynomial time uses Mathlib's Turing.TM2ComputableInPolyTime for the encodings encodeInstance and encodeWord (prefix markers for list structure), together with finiteness of every stack alphabet, so the time bound is in input bits on a finite-alphabet machine. A function that is merely computable, or polynomial only in the number of symbols, does not satisfy the goal.
Needed infrastructure: the all-substrings graph and Euler tours, periodicity lemmas (Fine–Wilf), and a verified implementation on Mathlib's TM2 model. Contributions of reusable TM2 programming libraries are welcome.
Selected references
J. Tarhio and E. Ukkonen, A greedy approximation algorithm for constructing shortest common superstrings, Theor. Comput. Sci. 57 (1988), 131–145. https://doi.org/10.1016/0304-3975(88)90167-3
A. Blum, T. Jiang, M. Li, J. Tromp and M. Yannakakis, Linear approximation of shortest superstrings, J. ACM 41 (1994), 630–647. https://doi.org/10.1145/179812.179818
D. Breslauer, T. Jiang and Z. Jiang, Rotations of periodic strings and short superstrings, J. Algorithms 24 (1997), 340–353. https://doi.org/10.1006/jagm.1997.0861
N. Chukhin, A. S. Kulikov, I. Mihajlin and A. Smal, A tight cycle-cover inequality for shortest common superstring, ECCC TR26-157, 2026. https://eccc.weizmann.ac.il/report/2026/157/
The approximation threshold for metric k-medianResearch Paper
Motivation
In metric k-median, a finite set J (or D) of clients and a finite set F of candidate facilities lie in a common finite metric with rational distances. Given an integer k≥1, one opens a nonempty set S⊆F with ∣S∣≤k and pays
Candidate facilities are part of the input and need not coincide with the clients. It is one of the basic clustering and facility-location objectives, and its approximability has been a testing ground for LP rounding, primal-dual methods and local search. A lower bound has long been known: if P=NP, no polynomial-time algorithm achieves a factor below 1+2/e≈1.736 in this candidate-facility model, by a reduction from Feige's coverage gap. The best polynomial-time algorithms had reached 2+ε, leaving a gap between 1.736 and 2.
This mission asks for a formal proof that the threshold is exactly 1+2/e, as stated in an OpenAI preprint dated September 24, 2026 (source): a deterministic polynomial-time (1+2/e+ε)-approximation for every fixed ε>0, and hence, under P=NP, an infimal approximation factor of exactly 1+2/e. The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
Background
2001–2002 — Jain and Vazirani connect k-median to facility location by Lagrangian relaxation and primal-dual methods (J. ACM 2001); Charikar, Guha, Tardos and Shmoys give the first constant-factor approximation by LP rounding (JCSS 2002); Jain, Mahdian and Saberi introduce greedy dual fitting (STOC 2002; J. ACM 2003).
2004 — Arya et al. show that bounded-swap local search achieves 3+ε (SICOMP 2004).
2016 — Li and Svensson show that constant-additive pseudo-approximations can be converted to true approximations at arbitrarily small loss, breaking the factor-3 barrier (SICOMP 2016).
2017–2023 — Bi-point rounding: 2.675+ε (Byrka et al., TALG 2017) and 2.613 (Gowda et al., SODA 2023).
2019 — Cohen-Addad, Gupta, Kumar, Lee and Li give a tight FPT (1+2/e+ε)-approximation in time kO(k)poly (ICALP 2019).
2025–2026 — Cohen-Addad, Grandoni, Lee, Schwiegelshohn and Svensson reach 2+ε (arXiv:2503.10972); Byrka et al. develop iterative randomized rounding with 2+ε (arXiv:2604.06046).
September 2026 — Two OpenAI preprints claim a deterministic (1+2/e+ε)-approximation, matching the known hardness threshold (source), and an independent randomized (2−σ)-approximation via anchor recovery and bounded-price strictness (source).
Hardness — Feige proves the lnn threshold for set cover and the perfect-completeness Max-k-Coverage gap (J. ACM 1998, Theorem 5.3); Anand and Lee record the resulting 1+2/e lower bound for k-median with specified facilities under P=NP (IPCO 2024).
Setting
An instance consists of n points with a rational distance table d that is a metric (nonnegative, zero exactly on the diagonal, symmetric, triangle inequality), a client set J, a facility set F (index sets that may overlap), and an integer 1≤k≤∣F∣, encoded in binary. A feasible solution is a nonempty S⊆F with ∣S∣≤k. An algorithm is an α-approximation if it always outputs a feasible S with cost(S)≤αOPTk, and it is polynomial-time if it runs on a deterministic multi-stack Turing machine with finite alphabets in time polynomial in the encoding length.
Formalization targets
Milestone: Theorem 1.1 (p. 1)
For every fixed ε>0 there is a deterministic polynomial-time algorithm which, on every instance, returns a feasible S with
The result itself. It closes the approximability of metric k-median with specified candidate facilities up to arbitrarily small additive error in the factor, ending a sequence of improvements from LP rounding through local search (3+ε), bi-point rounding (2.675, 2.613) to 2+ε. It shows that the FPT factor 1+2/e of Cohen-Addad et al. is achievable in polynomial time. The case F=J has a different and still separate lower-bound question.
Formalizing it. The goal combines an algorithmic theorem with a hardness reduction. A formal proof needs: the Li–Svensson reduction from constant-additive pseudo-approximations (Theorem 2.2, p. 4); the grid preparation and iterative rounding with a finite directed comparison inequality whose scalar estimates are proved by rational polynomial certificates (Sections 3–5, Appendix A); derandomization by moment-matching distributions of polynomial size (Section 6); and, for the lower bound, NP-hardness of Feige's coverage gap in the Lean computation model. All are reusable for other clustering and covering problems.
Difficulty
Two obstacles meet. The cardinality budget is hard: allowing a constant number of extra facilities makes good connection cost much easier, and earlier rounding analyses in the iterative graph framework only certify factors at least 2 (p. 2). The preprint's new ingredient is a potential that keeps track of surviving assignment copies after an opening and a finite directed comparison inequality (Theorem 4.1, p. 13) that pays for erasures. Then the randomized rounding must be made deterministic and polynomial-time while keeping the analysis valid, which requires preserving exactly the low-order moments the analysis uses (Lemma 6.1, p. 28; Theorem 6.2, p. 33), before Li–Svensson removes the additive surplus. The hardness side is classical but rests on the PCP-based Max-k-Coverage gap.
Formalization scope
Instance carries n, a Fin n → Fin n → ℚ metric (distance_eq_zero is an iff, so a true metric), client and facility Finsets, and 1 ≤ k ≤ facilities.card. cost sums nearest distances over clients; optimum is the minimum over nonempty facility subsets of size ≤k.
Outputs are membership bit masks of an actual feasible set; FactorCorrect α I out requires that mask to describe a nonempty S⊆F with ∣S∣≤k and cost(S)≤αOPTk.
Polynomial time is Turing.TM2ComputableInPolyTime with finite tape alphabets, on the fixed binary instance encoding.
approximationFactors is the set of α admitting such an algorithm, and the goal is sInf approximationFactors = 1 + 2/Real.exp 1 under the hypothesis Complexity.PNeNP, where P and NP are defined in the same machine model (NP via polynomial-length witnesses and a finite-alphabet polynomial-time verifier). The set is nonempty by the milestone and bounded below, so sInf is meaningful.
The hypothesis P=NP is not provable, so the goal is a conditional statement; deriving the lower bound requires a Cook–Levin-type NP-hardness of the coverage gap in this model.
K. Jain, M. Mahdian, E. Markakis, A. Saberi, V. V. Vazirani, Greedy facility location algorithms analyzed using dual fitting with factor-revealing LP, J. ACM 50 (2003). https://doi.org/10.1145/950620.950621
R. Gandhi, S. Khuller, S. Parthasarathy, A. Srinivasan, Dependent rounding and its applications to approximation algorithms, J. ACM 53 (2006). https://doi.org/10.1145/1147954.1147956
K. N. Gowda, T. Pensyl, A. Srinivasan, K. Trinh, Improved bi-point rounding algorithms and a golden barrier for k-median, SODA 2023. https://doi.org/10.1137/1.9781611977554.ch38
K. Jain, V. V. Vazirani, Approximation algorithms for metric facility location and k-median problems using the primal-dual schema and Lagrangian relaxation, J. ACM 48 (2001). https://doi.org/10.1145/375827.375845
M. Charikar, S. Guha, É. Tardos, D. B. Shmoys, A constant-factor approximation algorithm for the k-median problem, JCSS 65 (2002). https://doi.org/10.1006/jcss.2002.1882
V. Arya, N. Garg, R. Khandekar, A. Meyerson, K. Munagala, V. Pandit, Local search heuristics for k-median and facility location problems, SIAM J. Comput. 33 (2004). https://doi.org/10.1137/S0097539702416402
J. Byrka, T. Pensyl, B. Rybicki, A. Srinivasan, K. Trinh, An improved approximation for k-median and positive correlation in budgeted optimization, ACM TALG 13 (2017). https://doi.org/10.1145/2981561
V. Cohen-Addad, F. Grandoni, E. Lee, C. Schwiegelshohn, O. Svensson, A (2+ε)-approximation algorithm for metric k-median, arXiv:2503.10972 (2026 version). https://arxiv.org/abs/2503.10972v2
Single-exponential recovery and bounded-price strictness for metric k-medianResearch Paper
Motivation
In metric k-median, a finite set J (or D) of clients and a finite set F of candidate facilities lie in a common finite metric with rational distances. Given an integer k≥1, one opens a nonempty set S⊆F with ∣S∣≤k and pays
Candidate facilities are part of the input and need not coincide with the clients. It is one of the basic clustering and facility-location objectives, and its approximability has been a testing ground for LP rounding, primal-dual methods and local search. The hard part of the problem is the facility budget: a solution with small connection cost is much easier to find if a few extra facilities may be opened, and every approximation algorithm must eventually enforce ∣S∣≤k on its output.
This mission concerns two tools for enforcing that budget and their combination into a randomized approximation strictly below factor 2 on arbitrary finite rational metrics, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
Background
2001–2002 — Jain and Vazirani connect k-median to facility location by Lagrangian relaxation and primal-dual methods (J. ACM 2001); Charikar, Guha, Tardos and Shmoys give the first constant-factor approximation by LP rounding (JCSS 2002); Jain, Mahdian and Saberi introduce greedy dual fitting (STOC 2002; J. ACM 2003).
2004 — Arya et al. show that bounded-swap local search achieves 3+ε (SICOMP 2004).
2016 — Li and Svensson show that constant-additive pseudo-approximations can be converted to true approximations at arbitrarily small loss, breaking the factor-3 barrier (SICOMP 2016).
2017–2023 — Bi-point rounding: 2.675+ε (Byrka et al., TALG 2017) and 2.613 (Gowda et al., SODA 2023).
2019 — Cohen-Addad, Gupta, Kumar, Lee and Li give a tight FPT (1+2/e+ε)-approximation in time kO(k)poly (ICALP 2019).
2025–2026 — Cohen-Addad, Grandoni, Lee, Schwiegelshohn and Svensson reach 2+ε (arXiv:2503.10972); Byrka et al. develop iterative randomized rounding with 2+ε (arXiv:2604.06046).
September 2026 — Two OpenAI preprints claim a deterministic (1+2/e+ε)-approximation, matching the known hardness threshold (source), and an independent randomized (2−σ)-approximation via anchor recovery and bounded-price strictness (source).
Setting
Write n=∣D∣ and N=∣D∣+∣F∣. A comparison solutionO⊆F of size h assigns each client to a nearest member of O (ties broken by fixed priorities); Ci is the cluster of i∈O and Pi=∑p∈Cid(p,i), with P=cost(O). An anchor is a supplied feasible S⊆F with ∣S∣=h. A certificate partitions O into good and bad centres and gives distinct proxiesφi∈S for the good centres. A randomized polynomial-time algorithm is a polynomial-time multi-stack Turing machine that reads the encoded instance together with a string of fair random bits whose length is a fixed polynomial in the input length.
Formalization targets
Milestone: refined recovery (Theorem 1.1, p. 2)
Let D,F be disjoint, with distances between distinct indices positive integers bounded by a fixed polynomial in N. Fix ε>0, 0<L0<∞ and a rational 0<μ≤min{1/4,ε/12}. There is a randomized algorithm that, given an anchor S with ∣S∣=h≥1 and a failure parameter ζ∈(0,1), always returns S^⊆F with ∣S^∣≤h, runs in time polynomial in N and log(1/ζ), and, whenever some comparison solution O of size h and cost P>0 admits a certificate with
satisfies cost(S^)≤(1+2/e+ε)P with probability at least 1−ζ. The algorithm is not given O, P or the certificate.
Goal: global application (Theorem 1.2, p. 3)
There is an absolute constant σ>0 such that for every fixed a>0 some randomized polynomial-time algorithm for metric k-median always returns a feasible S (nonempty, S⊆F, ∣S∣≤k) and satisfies
The result itself. Theorem 1.1 makes the running time single-exponential in the number of clusters without accurate proxies, so logarithmically many exceptions are tractable; FPT methods with kO(k) dependence do not give this by setting k=O(logN). Combined with a new proof of bounded-price strictness for one compatible execution of the logarithmic-surplus construction of Cohen-Addad, Grandoni, Lee, Schwiegelshohn and Svensson (Lemma 8.1, p. 43), it yields Theorem 1.2: a randomized approximation strictly below 2, both with high probability and in expectation, that opens at most k facilities on every output. A companion preprint proves a stronger deterministic (1+2/e+ε) bound by an independent route; Theorem 1.2's interest is the way recovery and payment accounting together enforce the budget.
Formalizing it. The statements are fully explicit about the machine model, the random bits, and the input encoding. A formal proof would need local-search anchoring (Theorem 3.3), leader/ball sampling with amortized radius guesses (Section 4), a finite categorical continuous-greedy algorithm with explicit error (Lemma 5.1, p. 21), the surplus construction as an external interface (Theorem 7.1, p. 35), and metric rounding and transfer (Lemma 2.1, p. 6). The submodular-optimization and local-search components are reusable.
Difficulty
Every factor-2 dual-fitting argument charges λ+2PC to a client set C served by a comparison facility, which gives exactly 2; improving the constant requires saving on connection cost while still paying for all h regular openings with one final price, one set of copy lengths and the budgets of one actual replay of the construction (Section 1.2, p. 3). On the recovery side, guessing a good solution from an anchor naively costs kO(k); keeping the dependence single-exponential in the number of bad clusters requires interleaving leader sampling and removals and amortizing radius guesses over disjoint client sets (Section 4). Theorem 1.1 holds only for normalized integral metrics; the global application must construct its anchors after normalization and transfer the final cost bound back (Lemma 2.1, p. 6).
Formalization scope
RationalMetricInput: points Fin pointCount, a rational pseudometric table (zero on the diagonal, symmetric, triangle inequality), client and facility Finsets covering all points (they may overlap, so clients and facilities may share locations), a nonempty facility set and a positive budget k. Feasible S is S⊆F, ∣S∣≤k, and S nonempty when there are clients; optimum minimizes over nonempty subsets of size ≤k.
A BinaryRandomizedAlgorithm is a TM2ComputableInPolyTime function of (input bits, random bits) with finite alphabets, using randomBits.eval (input length) fair bits; probabilities and expectations are uniform averages over all seeds.
In the goal, feasibility holds for every seed; the success bound is 1−(N+2)−a with N=∣D∣+∣F∣ (Real.rpow); the same algorithm must also satisfy the expectation bound.
In the milestone, Input adds disjointness of D and F, integral distances, positivity between distinct indices, and an anchor with anchor.card = budget; Bounded bound caps distances by a fixed polynomial in N; ζ is passed in unary precision ⌈log2(1/ζ)⌉, and PolynomialWork bounds work by c(N+1)d(1+log(1/ζ))d. A Certificate encodes O with ∣O∣=h, P>0, the good set, injective proxies into the anchor, the proxy-cost promise with lexicographic tie-breaking, and at most L0logN bad centres.
V. Cohen-Addad, F. Grandoni, E. Lee, C. Schwiegelshohn, Breaching the 2 LMP approximation barrier for facility location with applications to k-median, arXiv:2207.05150 (2026 version). https://arxiv.org/abs/2207.05150v2
G. Călinescu, C. Chekuri, M. Pál, J. Vondrák, Maximizing a monotone submodular function subject to a matroid constraint, SIAM J. Comput. 40 (2011). https://doi.org/10.1137/080733991
K. Jain, M. Mahdian, E. Markakis, A. Saberi, V. V. Vazirani, Greedy facility location algorithms analyzed using dual fitting with factor-revealing LP, J. ACM 50 (2003). https://doi.org/10.1145/950620.950621
K. Jain, V. V. Vazirani, Approximation algorithms for metric facility location and k-median problems using the primal-dual schema and Lagrangian relaxation, J. ACM 48 (2001). https://doi.org/10.1145/375827.375845
M. Charikar, S. Guha, É. Tardos, D. B. Shmoys, A constant-factor approximation algorithm for the k-median problem, JCSS 65 (2002). https://doi.org/10.1006/jcss.2002.1882
V. Arya, N. Garg, R. Khandekar, A. Meyerson, K. Munagala, V. Pandit, Local search heuristics for k-median and facility location problems, SIAM J. Comput. 33 (2004). https://doi.org/10.1137/S0097539702416402
J. Byrka, T. Pensyl, B. Rybicki, A. Srinivasan, K. Trinh, An improved approximation for k-median and positive correlation in budgeted optimization, ACM TALG 13 (2017). https://doi.org/10.1145/2981561
V. Cohen-Addad, F. Grandoni, E. Lee, C. Schwiegelshohn, O. Svensson, A (2+ε)-approximation algorithm for metric k-median, arXiv:2503.10972 (2026 version). https://arxiv.org/abs/2503.10972v2