Theoretical Computer Science

Operations Research·Captain: Shuze Chen

The k-Server ConjectureOpen Problem

Motivation

The $k$ -server problem was introduced by Manasse, McGeoch, and Sleator (STOC 1988 / J. Algorithms 1990) as a common generalization of paging, weighted caching, and related sequential decision problems, and their $k$ -server conjecture has since become the central open question of competitive analysis. The conjecture asserts that a single ratio — exactly $k$ — governs deterministic online server management on every metric space.

Timeline

1985. Sleator and Tarjan introduce competitive analysis — an online algorithm judged against the offline optimum on every input — for list update and paging, and ask for a theory of such guarantees.
1988–1990. Manasse, McGeoch, and Sleator introduce the $k$ -server problem (STOC 1988; J. Algorithms 1990) and settle its extremes: no deterministic algorithm beats ratio $k$ on any space with more than $k$ points (Corollary 7), two servers admit a $2$ -competitive algorithm (Theorem 5, algorithm RES), and $k$ servers on $k+1$ points admit a $k$ -competitive one (Theorem 4, algorithm BAL). Section 8 poses the $k$ -server conjecture, in the symmetric finite setting of the paper.
1990. Fiat, Rabani, and Ravid (FOCS 1990) give the first competitive ratio depending on $k$ alone — exponential in $k$ , but finite on every metric space.
1991. Chrobak, Karloff, Payne, and Vishwanathan (SIAM J. Discrete Math.) prove the conjecture on the real line via Double Coverage; Chrobak and Larmore (SIAM J. Comput.) extend it to all tree metrics.
1995. Koutsoupias and Papadimitriou (J. ACM) prove the Work Function Algorithm is $(2k-1)$ -competitive on every metric space — the breakthrough, and still the best general bound. Their Conjecture 1.1 fixes the conjecture's modern form: for every metric space there is an online algorithm with competitive ratio $k$ .
1996. The same authors verify the conjecture on spaces of $k+2$ points via the dual 2-evader problem (Inf. Process. Lett. 57).
2004. Bartal and Koutsoupias prove the WFA itself is $k$ -competitive on the line, weighted stars, and all spaces of $k+2$ points.
2021. Coester and Koutsoupias (ICALP) give a unifying potential for all known WFA analyses and push the frontier to the circle.
2023. Bubeck, Coester, and Rabani (STOC) refute the randomized analogue: no $o(\log^2 k)$ -competitive randomized algorithm exists in general. The deterministic conjecture — this mission's goal — survives as the central open question, with the gap between $k$ and $2k-1$ unmoved since 1995.
2026. Coester, Koutsoupias, and Zbysiński post The $k$ -server conjecture is true (arXiv:2609.15979), a claimed proof of the full conjecture: the Work Function Algorithm itself is $k$ -competitive on every metric space, via a matrix representation of work functions and a potential function built on it. The preprint is not yet peer-reviewed; this mission's goal stays open until a machine-checked proof exists.

Setting

Fix a metric space $M$ with distance function $d$ , and a number of servers $k \ge 1$ . A configuration records where the $k$ servers stand: it is a function $C$ assigning to each server $i \in \{1, \dots, k\}$ a point $C(i) \in M$ . Moving the servers from configuration $C$ to configuration $C'$ means server $i$ travels from $C(i)$ to $C'(i)$ ; the movement cost is the total distance traveled,

\mathrm{moveCost}(C, C') \;=\; \sum_{i=1}^{k} d\bigl(C(i),\, C'(i)\bigr).

A request sequence is a finite list $\sigma = (r_1, \dots, r_n)$ of points of $M$ , presented one at a time; write $\sigma_{\le j} = (r_1, \dots, r_j)$ for the list of the first $j$ requests (so $\sigma_{\le 0}$ is the empty list).

A deterministic online algorithm $A$ is a rule that, for every finite request sequence $\ell$ , specifies a configuration $A(\ell)$ — where the servers stand after serving the requests of $\ell$ in order. In particular $A(\text{empty list})$ is the initial configuration, before any request arrives. Two points about this way of modeling an algorithm:

Online and deterministic, by construction. The configuration after $j$ requests is $A(\sigma_{\le j})$ , a function of those first $j$ requests only — the algorithm cannot see the future, and makes no random choices.
The service constraint. Whenever a request sequence ends with a request $r$ , some server must stand at $r$ immediately after: for every list $\ell$ and every point $r$ , the configuration reached after serving $\ell$ followed by $r$ places at least one server at the point $r$ .

Running $A$ on $\sigma = (r_1, \dots, r_n)$ produces the configurations $A(\sigma_{\le 0}),\, A(\sigma_{\le 1}),\, \dots,\, A(\sigma_{\le n})$ , and its cost is the total movement along this trajectory:

\mathrm{cost}_A(\sigma) \;=\; \sum_{j=1}^{n} \mathrm{moveCost}\bigl(A(\sigma_{\le j-1}),\, A(\sigma_{\le j})\bigr).

For comparison, an offline schedule for $\sigma$ starting at a configuration $C_0$ is any sequence of configurations $S_0 = C_0, S_1, \dots, S_n$ in which $S_j$ places a server at the request $r_j$ , for each $j$ — chosen with the whole of $\sigma$ known in advance. The optimal offline cost $\mathrm{OPT}(C_0, \sigma)$ is the infimum, over all such schedules, of the total movement $\sum_{j=1}^{n} \mathrm{moveCost}(S_{j-1}, S_j)$ .

Finally, $A$ is $c$ -competitive if there is a constant $a$ — depending on the algorithm, hence possibly on the metric space and the initial configuration, but never on the request sequence — with

\mathrm{cost}_A(\sigma) \;\le\; c \cdot \mathrm{OPT}\bigl(A(\text{empty list}),\, \sigma\bigr) + a \qquad \text{for every request sequence } \sigma.

Formalization targets

Goal — the $k$ -server conjecture

\text{For every } k \ge 1,\ \text{every metric space } M,\ \text{and every initial configuration } C_0:\ \exists\, A \text{ starting at } C_0 \text{ that is } k\text{-competitive.}

The goal fixes no algorithm: any $k$ -competitive construction settles it. This is the weakest stable form of the conjecture — it survives every improvement in constants or techniques short of a disproof.

Milestones — the known ladder

The milestones are the classical results between the trivial and the conjectured, each an existence or impossibility statement over the same definitions: the lower bound $c \ge k$ on any space with at least $k+1$ points; the conjecture for $k = 2$ ; for spaces of exactly $k+1$ points; for the real line; the $(2k-1)$ upper bound of the Work Function Algorithm on every space; the conjecture for spaces of exactly $k+2$ points; the conjecture for three servers in the Manhattan plane $(\mathbb{R}^2, \ell^1)$ — the one settled case over a genuinely two-dimensional continuum (Bein–Chrobak–Larmore 2002; reproved by the unifying potential of Coester–Koutsoupias 2021); Coester–Koutsoupias's 2021 result that the Work Function Algorithm itself — not just some algorithm — is $3$ -competitive for three servers on trees, stated over an explicit formalization of the WFA; and the 2023 Bubeck–Coester–Rabani refutation of the randomized analogue: there are $(k+1)$ -point spaces on which every randomized algorithm is $\Omega(\log^2 k)$ -competitive, stated over a mixed-strategy model of randomized online algorithms.

Significance

A proof of the conjecture would close the founding problem of competitive analysis and pin down the exact power of determinism in online optimization over arbitrary metrics; a disproof would separate general metric spaces from every special class where the ratio $k$ is known tight. Either outcome recalibrates the field's standard model of adversarial request sequences.

None of these results — not even the lower bound — has a machine-checked proof, and online algorithms as a subject are absent from Mathlib. This mission builds the base layer: a faithful model of online service systems (configurations, online algorithms as prefix functions, offline schedules, competitiveness), the classical possibility and impossibility results over it, and, at the top, the Koutsoupias–Papadimitriou bound, whose potential-function argument is self-contained but delicate. The model is reusable for paging, weighted caching, metrical task systems, and the randomized $k$ -server problem.

Difficulty

The obvious first idea — the greedy algorithm, moving the nearest server to each request — is not competitive for any constant, already on three points of the line: two nearby points can ping-pong one server forever while a server parked slightly farther away never moves. Every known competitive algorithm must sometimes move a server other than the nearest one, and the whole difficulty of the conjecture is quantifying exactly how much such foresight-free hedging can achieve. The Work Function Algorithm's analysis via a potential over offline work functions loses a factor of two for reasons nobody has been able to remove; on the lower-bound side, no metric space is known where the deterministic ratio exceeds $k$ .

Formalization scope

The Lean model commits to: configurations as functions Fin k → M (labeled servers — equivalent in cost to the unlabeled multiset model, since offline can permute labels for free); algorithms as total functions List M → (Fin k → M) with the service constraint, so a step may move several servers (the standard laziness reduction makes this equivalent to one-move-per-request); costs in ℝ via Metric.dist; the offline optimum as an sInf over schedules, which agrees with the attained minimum on finite spaces; and the additive-constant form of competitiveness, quantified as ∃ a, ∀ σ.

Two conventions guard against trivialization. The additive constant is quantified before the request sequence — allowing it to depend on $\sigma$ would make every algorithm $1$ -competitive. And the lower-bound milestone requires $k+1$ distinct points (Finset.card = k + 1); on spaces with at most $k$ points the conjecture is trivially true and the lower bound false.

Three further definitional layers extend the model. The work function workFunction C₀ σ C is the sInf of (schedule cost + final move to C) over schedules serving σ from C₀, and the Work Function Algorithm WFA is defined on finite spaces with k ≥ 1 servers: after each request it moves to a configuration containing the request minimizing (movement cost) + (work function of the history including the request), a minimizer existing by finiteness and ties broken by a fixed arbitrary choice — matching the standard definition with its "ties broken arbitrarily" (our fixed choice is one admissible instance). A tree is a finite metric space carrying a tree graph whose weighted path lengths realize the metric — exactly "the set of vertices of a tree" of the sources. A randomized algorithm is a mixed strategy: a probability measure over an index type together with a deterministic algorithm per outcome and measurable per-sequence cost; its expected cost is a lower Lebesgue integral in $[0,\infty]$ , and $c$ -competitiveness from $C_0$ demands every outcome start at $C_0$ and one additive constant work for all request sequences.

Welcome contributions: proofs of any milestone in any order (the lower bound and the $(k+1)$ -point case are the natural entry points); alternative algorithms for milestones already closed; and infrastructure lemmas about moveCost, schedules, and work functions published as reusable platform theorems.

Selected references

M. Manasse, L. McGeoch, D. Sleator, Competitive algorithms for server problems, J. Algorithms 11 (1990). doi:10.1016/0196-6774(90)90003-W
A. Fiat, Y. Rabani, Y. Ravid, Competitive k-server algorithms, FOCS 1990. doi:10.1109/FSCS.1990.89566
M. Chrobak, H. Karloff, T. Payne, S. Vishwanathan, New results on server problems, SIAM J. Discrete Math. 4 (1991). doi:10.1137/0404017
M. Chrobak, L. Larmore, An optimal on-line algorithm for k servers on trees, SIAM J. Comput. 20 (1991). doi:10.1137/0220008
E. Koutsoupias, C. Papadimitriou, On the k-server conjecture, J. ACM 42 (1995). doi:10.1145/210118.210128
E. Koutsoupias, C. Papadimitriou, The 2-evader problem, Inf. Process. Lett. 57(5) (1996), 249–252.
C. Coester, E. Koutsoupias, Towards the k-server conjecture: a unifying potential, pushing the frontier to the circle, ICALP 2021. arXiv:2102.10474
S. Bubeck, C. Coester, Y. Rabani, The randomized k-server conjecture is false!, STOC 2023. arXiv:2211.05753
E. Koutsoupias, The k-server problem (survey), Computer Science Review 3 (2009). doi:10.1016/j.cosrev.2009.04.002

122 thms11 active usersReviewed

Completed

Captain: marwahaha

More Asymmetry Bound: omega < 2.37134Research Paper

Motivation

The matrix-multiplication exponent measures how the arithmetic complexity of multiplying square matrices grows with the ir dimension. Known upper bounds come from constructing large independent matrix products inside tensor powers whose asymptotic rank is controlled. Improving the extraction, rather than finding a lower-rank starting tensor, has driven several recent advances.

Alman, Duan, Vassilevska Williams, Xu, Xu, and Zhou improve the combination-loss analysis by allowing all three variable directions to be treated differently. Their original fourth-power computation gives the bound $\omega<2.371339$ . The mission targets the slightly weaker rational endpoint $2.37134$ , keeping the historical result distinct from the later AlphaEvolve numerical improvement incorporated into the latest manuscript. More Asymmetry Yields Faster Matrix Multiplication, version 2, SODA 2025.

Setting

Fix an arbitrary field $K$ . The matrix-multiplication tensor $\langle a,b,c\rangle_K$ represents multiplication of an $a\times b$ matrix by a $b\times c$ matrix. A tensor's rank is the least number of pure tensors summing to it. The existing Lean definition matMulExp K is the infimum of $\log R(\langle n,n,n\rangle_K)/\log n$ for integer dimensions $n\ge2$ , with value $3$ at the excluded dimensions $0$ and $1$ . This definition, and the existing equivalence with the Strassen-preorder exponent, remain unchanged.

The source tensor is the literal fourth power $T=CW_5^{\otimes4}$ of the Coppersmith–Winograd tensor. The public parenthesization is $(CW_5\otimes CW_5)\otimes(CW_5\otimes CW_5)$ . Its asymptotic rank is at most $7^4=2401$ . Its canonical coarse components are indexed by triples $(i,j,k)$ with $i+j+k=8$ . This is the fourth-power, recursion-level-three specialization described in Section 7, not the eighth-power specialization used by the later optimization note. More Asymmetry, Section 7.

A complete split distribution records frequencies of entire fine-grade words, rather than only the marginal split at the next recursion step. At level $\ell\ge1$ , these words have length $2^{\ell-1}$ over the alphabet $\{0,1,2\}$ . Three such distributions describe the X-, Y-, and Z-variable blocks. A restricted constituent power keeps only blocks approximately consistent with those distributions, in maximum-coordinate distance at most a specified $\varepsilon\ge0$ . An interface tensor is a tensor product of these restricted constituent powers. The approximation tolerance and all three distributions are part of the interface. More Asymmetry, Definitions 3.4–3.6 and 4.1.

Formalization targets

The goal is the unconditional field-uniform statement

\forall K\;[\mathrm{Field}(K)],\qquad \operatorname{matMulExp}(K)<\frac{237134}{100000}.

Its binders and exponent definition match the existing Schönhage and Stothers goals; only the declaration name and endpoint differ. No optimizer result, characteristic condition, distribution, or assumed value surplus is a hypothesis of the root.

The compact proposal has four milestones and the root, totaling five review items. The milestones concern literal fine-to-coarse source restrictions; the fourth-power rank budget; an actual strict six-symmetrized value surplus at the chosen parameter; and the conditional implication from that surplus to the exponent bound. Existing proved source and rank theorems are reused. The open surplus target contains the new complete-split extraction and exact numerical obligations, which are described separately in the proof outline rather than hidden in an opaque certificate definition.

The chosen internal parameter is $\tau_0=3952233/5000000$ , so

2.371339<3\tau_0=2.3713398<2.37134.

The substantive value target is the existence of a real $V>2401$ such that the actual source has six-symmetrized $\tau_0$ -value at least $V$ in the existing finite-witness semantics. The strict slack leaves room to translate limiting extraction rates into strict lower bases. Neither the existence of that surplus nor a completed exact numerical certificate is claimed at proposal time.

Significance

This formalization would capture a new structural improvement, not a re-optimization of the same DWZ square data. Its distinguishing feature is sequentially obtaining the necessary ownership properties for X, then Y, then Z, while preserving more useful fine blocks. The resulting complete-split and interface-tensor theory is also the mathematical foundation for the later AlphaEvolve optimization. More Asymmetry, Sections 2, 4–6; Dupont et al., Section 2.

The known mathematical result is not an open conjecture. The open work is its machine-checked reconstruction. The earlier square and Stothers roots are marked Proved. The newer DWZ fourth-power root has an accepted reduction but remains Open. Its literal fourth source, rank budget, sixfold-symmetry bridge and entropy-certificate infrastructure can be reused independently of that unfinished endpoint. A proof of the numerical DWZ bound alone would not imply the smaller bound targeted here.

Difficulty

The old hashing interface guarantees both coarse X- and Y-block uniqueness. The new method initially requires only coarse X-block uniqueness. Fine Y-block compatibility and usefulness must then establish the ownership needed for the subsequent Z-stage. Applying a theorem whose hypotheses already demand coarse Y uniqueness would discard the new method's essential advantage. Six coordinate permutations create six regions whose parameters and output interfaces must remain consistent. More Asymmetry, Section 4.1 and Figure 1.

Removing incompatible fine blocks creates holes. The relevant repair theorem concerns holes in all three modes and a quantitative supply of broken interface copies. It cannot be replaced without proof by the older square-specific Z-only repair interface. The global and recursive stages also carry subexponential losses and approximation tolerances; their limiting order must be explicit. Numerical feasibility is a separate obligation: floating-point parameters and optimization success are not exact normalization, marginal, entropy, or logarithm proofs. More Asymmetry, Theorem 4.2, Theorems 5.3 and 6.4, and Section 7.

Formalization scope

The environment is pinned to Mathlib 777aaa61dcd2a1258d2b4962dbe983ede4d23b2e and Lean v4.29.0-rc3. The development reuses TensorObj, MMObj, restrictions, degenerations, tensor powers, existing tau-value predicates, and matMulExp. The root is uniform over arbitrary fields. Source relations remain target-first: a restriction of A from B is written Restrict A B. A collection of overlapping constituent restrictions must not be relabeled as an external direct sum.

Complete split distributions, simultaneous three-mode projections, interface tensors, region permutations, and explicit finite extraction maps form reusable infrastructure. Exact rational profiles require compatible lengths; approximate profiles require their stated tolerance and limiting argument. No constant-valued replacement for tensor value, vacuous witness hypothesis, or certificate that merely assumes the desired extraction is admissible.

The authors' released code and parameter archive is the provenance source for the original computation. Versioned archive and witness hashes belong to the companion source audit. The optimization program need not be formalized: an exact certificate checker must establish its own normalization, support, marginal and interval conditions. Contributions to complete-split interfaces, sequential ownership, three-mode repair, recursive extraction, entropy certificates, and finite source-to-exponent bridges all advance this mission.

Selected references

Josh Alman, Ran Duan, Virginia Vassilevska Williams, Yinzhan Xu, Zixuan Xu, and Renfei Zhou, More Asymmetry Yields Faster Matrix Multiplication, SODA 2025. Pinned version 2.
Authors' code and parameters for the original fourth-power bounds. OSF release.
Ran Duan, Hongxun Wu, and Renfei Zhou, Faster Matrix Multiplication via Asymmetric Hashing, FOCS 2023. Version 5.
Emilien Dupont et al., Improving the matrix multiplication exponent with modern optimization and AlphaEvolve, 2026 preprint. Version 1.

149 thms10 active usersReviewed

Completed

Captain: marwahaha

Duan–Wu–Zhou Fourth-Power Bound: omega < 2.37193Research Paper

Motivation

The matrix-multiplication exponent measures how the arithmetic cost of multiplying square matrices grows with their dimension. An improvement in this exponent is relevant both to algebraic complexity and to algorithms whose running times depend on matrix multiplication. This mission formalizes a known improvement using the fourth power of the Coppersmith–Winograd tensor; it does not claim a new mathematical record.

Duan, Wu, and Zhou identify a loss that arises when constituent tensors are analyzed independently although some of their finer components can coexist inside a shared variable block. Their asymmetric-hashing method recovers part of this combination loss. The paper's headline result concerns the eighth power. Its separate fourth-power computation reports $2.371919$ in Table 3, printed page 78. The present target is the slightly weaker exact rational endpoint $2.37193$ . Duan–Wu–Zhou, Faster Matrix Multiplication via Asymmetric Hashing.

Setting

Fix an arbitrary field $K$ . The matrix-multiplication tensor $\langle a,b,c\rangle_K$ encodes multiplication of an $a\times b$ matrix by a $b\times c$ matrix. Its tensor rank is the smallest number of pure tensors whose sum is that tensor. The existing Lean definition matMulExp K takes the infimum of $\log R(\langle n,n,n\rangle_K)/\log n$ over integers $n\ge2$ , with the value $3$ at the two excluded small dimensions. This definition is reused without alteration.

A restriction applies a linear map separately to each of a tensor's three variable spaces. A degeneration allows polynomial families of such maps and takes an appropriate leading coefficient. The order of the Lean relation is target first: Restrict A B means that $A$ is obtained from $B$ . A direct sum uses disjoint variable spaces; a collection of overlapping restrictions does not constitute a direct sum.

The Coppersmith–Winograd tensor $CW_q$ has border rank at most $q+2$ . This mission fixes $q=5$ and uses the literal tensor $T=(CW_5\otimes CW_5)\otimes(CW_5\otimes CW_5)$ , whose asymptotic-rank budget is $7^4=2401$ . Its standard coordinate partition has 45 coarse components $T_{ijk}$ indexed by nonnegative integers $i+j+k=8$ . Each coarse component consists of ordered products of square components, whose grades sum to $(i,j,k)$ . Duan–Wu–Zhou, Sections 3 and 6–8.

A restricted-splitting value pair consists of a lower value bound and a prescribed distribution on finer Z-variable blocks. In a tensor power, Z-blocks with the wrong empirical split distribution are removed before measuring value. Sixfold symmetrization, using all permutations of the three modes, is part of this definition. Keeping the scalar and discarding the prescribed distribution loses information required by the recursion. Duan–Wu–Zhou, Definition 3.9, Equation (3), and Definition 8.1.

Formalization targets

The goal is precisely

\forall K\;[\mathrm{Field}(K)],\qquad \operatorname{matMulExp}(K)<\frac{237193}{100000}.

It has the same field quantification and exponent definition as the completed Schönhage and Stothers goals. Only the name and rational endpoint change. No distribution, optimizer, characteristic restriction, or unproved value bound is a hypothesis of this goal.

The supporting targets concern the literal fourth-power source; prescribed-splitting component values; the recursive and global extraction inequalities of Equations (34) and (25); an exact certificate for the released fourth-power computation; and the value-to-exponent implication of Theorem 3.2. The proof outline distinguishes stable formal statements from source-level tasks whose complete Lean interfaces still require development. It does not turn an unspecified certificate into an assumption that the desired extraction exists.

The compact milestone list contains four precise statements: the literal fine-to-coarse product restriction; the fourth-power asymptotic-rank bound; existence of a strict six-symmetrized value surplus; and the conditional implication from that surplus to the goal. Together with the root, these are five review items. The first, second, and fourth milestones are marked Proved. The surplus remains Open. An accepted root reduction links the surplus to the proved capstone; it is a proof sketch, not a proof of the exponent bound. Recursive component extraction and exact numerical certification remain substantial work inside that open target.

The planned internal parameter is $\tau=790643/1000000$ . Thus $3\tau=2.371929<2.37193$ . The substantive value obligation is a strict surplus over $2401$ for the actual fourth-power source, with asymptotic losses absorbed by choosing strict lower rates. The exact certificate must establish this surplus; neither its existence nor its numerical slack is presently claimed as proved.

Significance

The result would extend the formalized Stothers endpoint $2.3737$ to an asymmetric fourth-power bound. More importantly, it would provide restricted-splitting interfaces that can support subsequent higher-power and more-asymmetric analyses. The mathematical improvement is already established in the cited paper. The task here is to reconstruct its argument with machine-checked statements, concrete tensor maps, and exact numerical bounds.

The earlier square and Stothers mission roots are marked Proved. Reusable infrastructure includes polynomial degenerations, tensor powers, direct-sum value witnesses, hashing and hole-repair lemmas, the literal fourth-power grading, and the final exponent bridge. Two additional literal fourth-power support/restriction bridges and an additive entropy certificate with directed-log inputs are also marked Proved. These statuses do not imply that the new restricted-value recursion or numerical witness is already formalized.

Difficulty

The central difficulty is retaining the correct dependence between each value bound and its prescribed split distribution. The released fourth-power data contains consumer-specific copies of square value pairs. Equal coarse grades do not justify identifying their chosen distributions. The 21 positive fourth-power components use the six-region recursion, whereas the 24 components with a zero coordinate require the boundary merging argument. Duan–Wu–Zhou, Equation (34), Section 7.3, and released implementation.

Global hashing must additionally control competitors with the same marginals, shared Z-blocks, missing fine blocks, and subexponential losses. An isolated restriction into each constituent is insufficient to establish a simultaneous extraction. Numerical optimization presents a separate issue: floating-point normalization and approximate maximum-entropy computations are not exact feasibility or entropy proofs. Exact marginal constraints, positivity domains, and directed error bounds must all be checked.

Formalization scope

The environment is pinned to Mathlib 777aaa61dcd2a1258d2b4962dbe983ede4d23b2e and Lean v4.29.0-rc3. The development reuses TensorObj, MMObj, Degenerates, HasTauValueAtLeast, the six-symmetrized value infrastructure, and matMulExp. All endpoint theorems remain uniform over arbitrary fields. Finite profiles use exact integer counts; rational distributions must have compatible unbounded lengths before an asymptotic statement is invoked. Real limiting rates are represented with explicit strict slack where the existing finite-witness predicate does not guarantee endpoint attainment.

No constant-valued replacement for tensor value, opaque witness carrying its desired conclusion, or external direct sum substituted for overlapping source blocks is admissible. New definitions must specify the actual coordinate projections and restrictions they represent. The authors' optimizer is used to find candidate data, not trusted as a proof oracle. Contributions to restricted-power semantics, consumer-specific square pairs, boundary merging, recursive extraction, exact entropy bounds, and source-to-exponent bridges are all directly relevant to the goal.

Selected references

Ran Duan, Hongxun Wu, and Renfei Zhou, Faster Matrix Multiplication via Asymmetric Hashing, FOCS 2023. Full paper, version 5.
Duan–Wu–Zhou, accompanying optimization and verification code, including power4_dup_2.371919.mat. Authors' release.
A. M. Davie and A. J. Stothers, Improved Bound for Complexity of Matrix Multiplication, Proceedings of the Royal Society of Edinburgh Section A 143(2), 2013. DOI.
Arnold Schönhage, Partial and Total Matrix Multiplication, SIAM Journal on Computing 10(3), 1981. DOI.

125 thms10 active usersReviewed

Completed

Formal Verification Mathematical Logic·Captain: Rizwan G Mir

The Cook-Levin Theorem: NP-Completeness of Boolean Satisfiability in Lean 4Research Paper

Introduction

The Cook-Levin theorem states that CNF SAT is NP-complete. This mission formalizes the theorem over a multi-tape Turing machine model in Lean 4.

Main Goal

Prove CookLevin.cook_levin_theorem:

NPComplete SAT

under the decider and reduction hypotheses.

175 thms9 active usersReviewed

Algebra Analysis Combinatorics+3·Captain: Lucas

Formal Conjectures Portfolio: Bateman-Horn and CompanionsOpen Problem

1. Motivation

Wikipedia's pages on open problems are, for many mathematicians, the first contact with a conjecture: a one-paragraph statement, a short history, a list of partial results. The Formal Conjectures library (Google DeepMind, Apache-2.0) turned a large part of that material into Lean 4 statements, so that the conjectures can be attacked — and, just as importantly, stated unambiguously — by machine.

This mission ports a coherent slice of that material to Prove2Me. It is deliberately a portfolio mission: the goal theorem is the Bateman–Horn conjecture, the strongest single statement in the collection, and the milestone list gathers the other conjectures and the landmark theorems that surround them. Some milestones are genuine steps toward the goal (the Bunyakovsky conjecture is literally the one-polynomial case); most are independent open problems from other fields, grouped here because they share a source, a level of difficulty, and a need for faithful formal statements. A reader should not assume that proving a milestone advances the goal theorem. The mission's value is that every statement in it has been written against the same Mathlib revision, checked to compile, and documented well enough to be attacked.

A rough timeline of the collection's landmarks:

1947 — Mills: a real $A>1$ with $\lfloor A^{3^n}\rfloor$ always prime.
1962 — Radó: the busy beaver function outgrows every computable function.
1971 — Davies: planar Kakeya sets have Hausdorff dimension $2$ .
1978 — Apéry: $\zeta(3)$ is irrational.
1985 — Read (after Enflo, 1981): an operator on $\ell^1$ with no nontrivial closed invariant subspace.
2001 — Zudilin: one of $\zeta(5),\zeta(7),\zeta(9),\zeta(11)$ is irrational.
2002 — Mihăilescu: $8$ and $9$ are the only consecutive perfect powers (Catalan's conjecture).
2009 / 2021 — Dvir; Bukh–Chao: the finite-field Kakeya bound and its sharp density constant.
2021 — Gardam: Kaplansky's unit conjecture is false (its zero-divisor and idempotent companions remain open).
2024 — Saito: Mills' constant is irrational; bbchallenge: $\mathrm{BB}(5)=47\,176\,870$ .
2025 — Wang–Zahl: the Kakeya set conjecture in $\mathbb{R}^3$ .

2. Setting

The goal theorem concerns prime values of polynomials. Fix a finite set $S=\{f_1,\dots,f_k\}\subseteq\mathbb{Z}[X]$ of distinct polynomials. Say that $f$ satisfies the Bunyakovsky condition if its leading coefficient is positive, $\deg f\ge 1$ , and $f$ is irreducible over $\mathbb{Z}$ ; say that $S$ satisfies the Schinzel condition if for every prime $p$ there is an integer $n$ with $p\nmid f_1(n)\cdots f_k(n)$ — i.e. no fixed prime divides the product at every argument.

For a prime $p$ let $\omega_p(S)$ be the number of residue classes $n \bmod p$ at which some $f_i$ vanishes, let $D=\prod_i \deg f_i$ , and let

\pi_S(x)=\#\{\,n\le x : |f_i(n)| \text{ is prime for every } i\,\}.

The Bateman–Horn constant is the (conditionally convergent) Euler product

C=\lim_{N\to\infty}\ \prod_{p<N}\Big(1-\tfrac1p\Big)^{-k}\Big(1-\tfrac{\omega_p(S)}{p}\Big).

The other groups use their own vocabulary, each fixed in a definition item of this mission: Kakeya sets in $\mathbb{R}^n$ and over $\mathbb{F}_q$ ; Mills' property $\lfloor A^{3^n}\rfloor \in \mathbb{P}$ ; Wagstaff primes and Catalan–Mersenne numbers; polynomial self-maps and their Jacobian matrix; nontrivial closed invariant subspaces; linear extensions of a finite poset; Catalan's constant; and an explicit two-symbol Turing machine model with its maximum-shifts function $\mathrm{BB}$ .

3. Target

The goal theorem is the Bateman–Horn asymptotic: under the Bunyakovsky and Schinzel hypotheses, $C$ exists and is positive and

\pi_S(x)\ \sim\ \frac{C}{D}\,\frac{x}{(\log x)^{k}}\qquad (x\to\infty).

Weaker statements in the same direction appear as milestones, first of all Bunyakovsky's conjecture: under the same hypotheses with $k=1$ , $f$ takes prime values infinitely often. The remaining milestones are listed in the milestone panel and are grouped by subject: Diophantine equations (Brocard, Pillai, Lebesgue–Nagell, Catalan/Mihăilescu), Mersenne-type primality (New Mersenne, infinitude of Mersenne primes, Catalan–Mersenne), prime-representing constants (Mills), geometric measure theory (Kakeya in $\mathbb{R}^n$ , Kakeya over $\mathbb{F}_q$ , Falconer), operator theory (invariant subspace problem and Read's $\ell^1$ counterexample), group algebras (Kaplansky's zero-divisor and idempotent conjectures), affine algebraic geometry (the two-variable Jacobian conjecture), irrationality and transcendence ( $\zeta(5)$ , all odd zeta values, Zudilin's theorem, $e+\pi$ , $e\pi$ , $\gamma$ , Catalan's constant), order theory (the $1/3$ – $2/3$ conjecture), and computability (Radó's theorem).

4. Significance

The results themselves. Bateman–Horn is the quantitative form of Schinzel's hypothesis H: it contains the twin prime conjecture, the infinitude of primes of the form $n^2+1$ , and Bunyakovsky as special cases, and it is the standard heuristic behind prime-counting predictions. The other targets are each the headline question of their area: whether every bounded Hilbert-space operator has an invariant subspace; whether group algebras of torsion-free groups are domains; whether Kakeya sets must have full dimension. The solved milestones (Mihăilescu, Davies, Dvir, Zudilin, Read, Saito, Radó) are landmarks whose formal proofs would be significant library contributions in their own right.

Formalizing them. None of the open statements is expected to fall here; the concrete deliverable is a set of faithful, compiling, reusable statements plus formal proofs of the solved milestones, most of which are not in Mathlib today. Several are realistically in reach: the finite-field Kakeya bound (Dvir's polynomial method is short), the elementary fact that $\pi+e$ and $\pi e$ cannot both be algebraic, and Radó's diagonal argument.

5. Difficulty

For Bateman–Horn, the obstruction is visible already for $k=1$ , $\deg f = 2$ : sieve methods bound $\pi_S(x)$ from above by a constant times the conjectured main term and produce almost-primes, but the parity problem blocks every known sieve from producing a single prime value of an irreducible quadratic. The conditional convergence of the Euler product is a second, smaller trap: the product over $p<N$ must be taken in order, so any reformulation as an unordered infinite product changes the statement.

Each other group has its own obstruction, and they do not transfer: the parity problem says nothing about Kakeya, where the difficulty is that dimension is not stable under the natural compactness arguments, nor about the invariant subspace problem, where the known counterexamples on $\ell^1$ show that no soft argument can work.

6. Formalization scope

Conventions this mission commits to, all fixed in the definition items:

Polynomials are elements of ℤ[X]; primality of a polynomial value is primality of its absolute value, and the counting function ranges over natural numbers $n \le \lfloor x\rfloor$ .
The Bateman–Horn constant is the limit of the ordered partial products over $p<N$ , not an unordered infinite product.
Kakeya sets carry no compactness or measurability hypothesis, matching the source; the conjecture is stated as an equality of Hausdorff dimensions in $[0,\infty]$ .
Falconer's hypothesis is written $d < 2\dim_H E$ to avoid division in $[0,\infty]$ .
Torsion-freeness of a group is spelled out as "every element of finite order is the identity", which is the hypothesis the source intends (it is weaker than Mathlib's IsMulTorsionFree).
Linear extensions are order-preserving bijections onto $\{0,\dots,|P|-1\}$ , and probabilities are quotients of set cardinalities in $\mathbb{Q}$ .
The busy beaver model is an explicit $n$ -state, $2$ -symbol machine with a bi-infinite Boolean tape; $\mathrm{BB}$ counts transitions performed (maximum shifts), the halting transition included, and $\mathrm{BB}(0)=0$ .
Several source statements are phrased as "is $X$ true?" with an unknown answer. Prove2Me statements must be definite, so each such question is recorded in its affirmative form (e.g. " $e+\pi$ is irrational"); a solver who can refute one should submit a disproof. The one question with no statable answer, "what is $\mathrm{BB}(6)$ ?", is replaced by Radó's growth theorem rather than guessed at.
Nothing here is vacuous: each hypothesis set is satisfiable (e.g. closed unit balls are Kakeya sets, and $X^2+1$ satisfies the Bunyakovsky and Schinzel conditions).

Contributions welcome: proofs of the solved milestones; sharper variants; and additional faithful statements from the same source library, which contains far more than fits in one mission.

7. Selected references

P. T. Bateman and R. A. Horn, A heuristic asymptotic formula concerning the distribution of prime numbers, Math. Comp. 16 (1962), 363–367. DOI
T. Radó, On non-computable functions, Bell System Tech. J. 41 (1962), 877–884. DOI
R. O. Davies, Some remarks on the Kakeya problem, Math. Proc. Cambridge Philos. Soc. 69 (1971), 417–421. DOI
C. J. Read, A solution to the invariant subspace problem on the space $\ell_1$ , Bull. London Math. Soc. 17 (1985), 305–317. DOI
K. Falconer, On the Hausdorff dimensions of distance sets, Mathematika 32 (1985), 206–212. DOI
W. Zudilin, One of the numbers $\zeta(5),\zeta(7),\zeta(9),\zeta(11)$ is irrational, Russian Math. Surveys 56 (2001), 774–776. DOI
P. Mihăilescu, Primary cyclotomic units and a proof of Catalan's conjecture, J. reine angew. Math. 572 (2004), 167–195. DOI
Z. Dvir, On the size of Kakeya sets in finite fields, J. Amer. Math. Soc. 22 (2009), 1093–1097. DOI
B. Bukh and T.-W. Chao, Sharp density bounds on the finite field Kakeya problem, Discrete Analysis 26 (2021). DOI
G. Gardam, A counterexample to the unit conjecture for group rings, Ann. of Math. 194 (2021), 967–979. DOI
K. Saito, Mills' constant is irrational, Mathematika 71 (2025), e70027. arXiv:2404.19461
H. Wang and J. Zahl, Volume estimates for unions of convex sets, and the Kakeya set conjecture in three dimensions, arXiv:2502.17655
Google DeepMind, Formal Conjectures, Apache-2.0, github.com/google-deepmind/formal-conjectures

Provenance note. The Lean statements in this mission are adaptations of the Formal Conjectures library (Apache-2.0), rewritten to depend only on Mathlib and on this mission's own definition items, and checked to compile against the platform's Mathlib revision. Each draft item carries a read-back; those read-backs are non-blind — they were written by the same agent that drafted the statements, and each says so in its first line. They are documentation, not independent testimony.

81 thms8 active usersReviewed

Completed

Captain: marwahaha

Davie–Stothers Fourth-Power Bound: omega < 2.3737Research Paper

Motivation

The matrix-multiplication exponent $\omega$ measures the asymptotic arithmetic cost of multiplying square matrices. An upper bound $\omega<c$ means that, over the field under consideration, two $n\times n$ matrices can be multiplied using $O(n^{c+\varepsilon})$ field operations for every $\varepsilon>0$ . It is a central benchmark in algebraic complexity and controls the exponent of many algorithms that use matrix multiplication as a subroutine.

Coppersmith and Winograd's 1990 analysis of the square of their tensor established $\omega<2.375477$ . That number remained the record for roughly two decades. Stothers' 2010 thesis first obtained a smaller exponent by analyzing the fourth tensor power, and Davie and Stothers later supplied a self-contained journal treatment. Their Theorem 5.3 and numerical parameters give $\omega<2.373689703$ ; see Davie--Stothers, printed pp. 367--368. The result is the first historical step below the classical tensor-square barrier and is the natural next capstone after a formal proof of the $2.375477$ bound.

This mission formalizes the Davie--Stothers fourth-power argument at the exact rational endpoint $2.3737$ . It concentrates on the new mathematical layer introduced by the fourth power: five non-matrix constituents, their recursive value estimates, and the two-dimensional same-marginal ambiguity in the final distribution count.

Setting

For a field $K$ , an order-three tensor represents a bilinear map. The matrix-multiplication tensor

\langle a,b,c\rangle_K =\sum_{i<a}\sum_{j<b}\sum_{k<c} x_{ij}\otimes y_{jk}\otimes z_{ki}

encodes multiplication of an $a\times b$ matrix by a $b\times c$ matrix. Restrictions apply linear maps to the three tensor legs; degenerations permit polynomial families of maps. A direct sum of matrix-multiplication tensors has disjoint variable blocks and can be converted into an exponent inequality by Schönhage's asymptotic sum inequality.

The Coppersmith--Winograd tensor $CW_q$ has border rank at most $q+2$ and a three-class coordinate partition. Its square decomposes into fifteen coarse constituents $\varphi_{ijk}$ with $i+j+k=4$ . Davie--Stothers square this decomposition again. The fourth power has forty-five constituents with indices summing to eight, grouped into ten symmetry classes represented by

\varphi_{008},\ \varphi_{017},\ \varphi_{026},\ \varphi_{035},\ \varphi_{044}, \ \varphi_{116},\ \varphi_{125},\ \varphi_{134},\ \varphi_{224},\ \varphi_{233}.

The first five classes are rectangular matrix-multiplication tensors. The last five require recursive value bounds. With $\rho\in[2,3]$ , the paper writes

E=(2q)^\rho,\qquad H=(q^2+2)^\rho,\qquad L=4q^\rho(q^\rho+2),

and states the five lower bounds in Lemma 5.1. The final fourth-power extraction assigns frequencies to the ten symmetry classes. Their coordinate marginals are encoded by the $9\times10$ matrix $Q$ in Equation (5.2); its kernel is the two-dimensional space $Y$ displayed immediately after that equation.

The paper's bounds are limiting exponential rates and may carry subexponential losses in their finite Salem--Spencer extractions. Prove2Me's HasTauValueAtLeast predicate instead records a constant-relative finite witness. The source-faithful formal statements therefore assert attainment of every fixed nonnegative base strictly below each displayed limiting rate, rather than unjustified attainment of the limiting endpoint itself. This downward-closed form retains the complete asymptotic conclusion and is exactly what the final strict numerical surplus needs.

Formalization targets

Goal: the Davie--Stothers fourth-power bound

For every field $K$ ,

\operatorname{matMulExp}(K)<\frac{23737}{10000}=2.3737.

The source's computed endpoint $2.373689703$ is strictly smaller, giving slack for an exact rational certificate. The Lean goal has exactly the same field quantification and matMulExp definition as the existing Coppersmith--Winograd mission; only the theorem identifier and endpoint change.

Source-level milestones

The mission records the canonical nine-grading of $CW_6^{\otimes4}$ and the ten symmetry classes of Table 1. It formalizes all five clauses of Lemma 5.1 for $\varphi_{116}$ , $\varphi_{125}$ , $\varphi_{134}$ , $\varphi_{224}$ , and $\varphi_{233}$ in every-strict-lower-base form; Equation (5.2) and the stated basis of $\ker Q$ ; Lemma 5.2's entropy minimization along that kernel; Theorem 5.3's downward-closed fourth-power value inequality; and the Table 2 numerical specialization. The final milestones connect the resulting tau-value surplus to the border-rank budget and transfer the Strassen-preorder exponent bound to matMulExp.

Significance

Mathematically, this theorem is the first improvement obtained by passing from the square to the fourth power of the Coppersmith--Winograd tensor. It establishes the recursive constituent pattern used by the later eighth-, sixteenth-, and higher-power analyses. In particular, the five formulas in Lemma 5.1 are the first complete catalogue of genuinely recursive fourth-power constituents.

For formalization, the mission creates a reusable representation of higher-power CW gradings and their symmetry orbits. It also forces a distinction between a locally chosen joint type and all other types with the same marginals. Lemma 5.2 is the exact finite-dimensional entropy correction needed when the marginal map has nontrivial kernel. That infrastructure can be reused by later refined-laser and complete-split missions.

The result is known mathematically. The open task is a machine-checked reconstruction. Prove2Me already contains the CW tensor, its characteristic-free border-rank degeneration, its canonical square grading and constituent restrictions, the Salem--Spencer layer, direct-sum tau-value witnesses, the asymptotic sum inequality, and the exponent bridge. The exact optimizer identity for the $\varphi_{116}$ profile is also proved. The remaining frontier is to connect the literal fourth-power constituents to finite direct-sum extractions, then assemble all five value estimates and the final kernel-corrected distribution count.

Difficulty

The fourth power contains 225 ordered products before symmetry grouping. A formal proof must show that each claimed constituent is the literal block of $CW_q^{\otimes4}$ and that its recursive decomposition uses the correct variable spaces. Replacing a sum of overlapping blocks by an external direct sum would make the value bound artificially strong.

The five non-matrix classes have different feasible frequency polytopes. Their optimizer formulas are valid only after the corresponding nonnegativity and normalization conditions are checked. The $\varphi_{233}$ class already has a nontrivial same-marginal family. At the global level the map $Q$ has a two-dimensional kernel, so marginal counts alone do not determine a unique joint distribution. Ignoring that kernel removes the entropy penalty and invalidates Theorem 5.3.

Finally, Table 2 contains decimal witnesses obtained numerically. A formal proof must replace floating-point evaluation by exact rational parameters and certified bounds for logarithms and real powers, while retaining strict slack at $23737/10000$ .

Formalization scope

The development uses environment 777aaa61dcd2a1258d2b4962dbe983ede4d23b2e and the existing TensorObj, MMObj, restriction, degeneration, HasTauValueAtLeast, tensorAsymptoticRank, matMulExp_strassen, and matMulExp declarations. Top-level theorems quantify over an arbitrary field. Finite block indices and symmetry classes use finite types; frequency vectors and entropy inequalities use real numbers; exact finite profiles use natural numbers before passing to cofinal asymptotics.

The capstone specializes to $q=6$ and the fourth tensor power. Generic grading, orbit, multinomial, entropy, and optimizer lemmas are welcome when they shorten later missions. Every value theorem must ultimately be backed by restrictions or degenerations to direct sums of concrete matrix-multiplication tensors. An opaque value functional, a constituent definition that is an external sum rather than the source block, or a numerical hypothesis that assumes the desired endpoint is outside scope.

Contributions are welcome for the literal nine-grading, symmetry-orbit classification, the five constituent extractions, exact address factorizations, optimizer feasibility, the kernel calculation and Lemma 5.2, exact Table 2 arithmetic, and the final exponent assembly.

Selected references

A. M. Davie and A. J. Stothers, Improved Bound for Complexity of Matrix Multiplication, Proceedings of the Royal Society of Edinburgh Section A: Mathematics 143(2), 2013, pp. 351--369. Author PDF and DOI 10.1017/S0308210511001646.
A. J. Stothers, On the Complexity of Matrix Multiplication, PhD thesis, University of Edinburgh, 2010. Edinburgh Research Archive.
Don Coppersmith and Shmuel Winograd, Matrix Multiplication via Arithmetic Progressions, Journal of Symbolic Computation 9, 1990, pp. 251--280. DOI 10.1016/S0747-7171(08)80013-2.
Arnold Schönhage, Partial and Total Matrix Multiplication, SIAM Journal on Computing 10(3), 1981, pp. 434--455. DOI 10.1137/0210032.

171 thms8 active usersReviewed

Completed

Combinatorics Complexity Theory Graph Theory+1·Captain: mikedeng1

Scheduling Subject to Resource Constraints: Classification and Complexity II: Unit-Time Jobs on Two Uniform Machines with Unit Resources Are Strongly NP-hardResearch Paper

Motivation

Machine scheduling asks how to assign jobs to machines over time. In many applications a job also needs additional scarce resources while it runs: a tool, a skilled operator, a memory bank, a channel. Adding such resources can turn a problem with a polynomial algorithm into an NP-hard one. Błażewicz, Lenstra and Rinnooy Kan (DAM 1983) extended the standard three-field classification $\alpha\,|\,\beta\,|\,\gamma$ of scheduling problems (Graham, Lawler, Lenstra and Rinnooy Kan 1979) with a resource field $res\lambda\sigma\rho$ . They then drew the complete borderline between easy and hard problems for unit-time jobs, identical or uniform machines and the makespan criterion. Their Fig. 2 marks each problem type as polynomially solvable or NP-hard.

This mission formalizes the two hardness results of that classification that come from graph partition problems (Theorems 2 and 3, p. 15). Two identical machines are easy under any resource constraints (Theorem 1, after Garey and Johnson 1975). Theorems 2 and 3 show that a third identical machine, or two machines of different speeds, already makes the problem strongly NP-hard, once the number of unit resources is part of the input.

Setting

There are $n$ jobs $J_1,\dots,J_n$ and $m$ machines $M_1,\dots,M_m$ . Each machine processes at most one job at a time, and each job runs on one machine without interruption. Machine $M_i$ has a speed $q_i>0$ , and every job has unit execution requirement $p_j=1$ , so it takes time $1/q_i$ on $M_i$ . Identical machines ( $P$ ) are the case $q_i=1$ ; uniform machines ( $Q$ ) allow arbitrary speeds.

There are $l$ resources $R_1,\dots,R_l$ . Resource $R_h$ has a positive integer size $s_h$ , the amount available at any time. Job $J_j$ needs a nonnegative integer amount $r_{hj}$ of $R_h$ throughout its execution. A schedule assigns each job a machine $\mu(j)$ and a start time $S_j\ge 0$ . Its completion time is $C_j=S_j+1/q_{\mu(j)}$ , and it is being executed at every time $t$ with $S_j\le t<C_j$ . A schedule is feasible when:

jobs on the same machine do not overlap in time;
at every time $t$ , the set $S_t$ of jobs being executed satisfies

\sum_{j\in S_t} r_{hj}\le s_h\qquad(h=1,\dots,l).

The makespan is $C_{\max}=\max_j C_j$ .

The resource type $res{\cdot}11$ means three things: the number $l$ of resources is part of the input, every size is $s_h=1$ , and every requirement satisfies $r_{hj}\le1$ . A unit resource is therefore a conflict: two jobs that both need it can never run at the same time. The problems here have no precedence constraints. $Pm\,|\,res{\cdot}11,\,p_j=1\,|\,C_{\max}$ and $Qm\,|\,res{\cdot}11,\,p_j=1\,|\,C_{\max}$ ask for a feasible schedule of minimum makespan. Their decision versions ask, for a threshold $y$ , whether a feasible schedule with $C_{\max}\le y$ exists.

The source problems are two graph problems on a graph $G=(V,E)$ with $|V|=3t$ :

PARTITION INTO TRIANGLES: can $V$ be partitioned into $t$ triples of pairwise adjacent vertices?
PARTITION INTO PATHS OF LENGTH 2: can $V$ be partitioned into $t$ triples, each with at most one nonadjacent pair, that is, each spanning a path of length 2?

Both are NP-complete (Garey and Johnson 1979, problems GT11 and GT13).

The construction of p. 15 introduces one job per vertex and one unit resource $R_{\{j,k\}}$ per nonadjacent pair $\{j,k\}$ , required by $J_j$ and $J_k$ only.

Formalization targets

Goal: Theorem 3

Q2\,|\,res{\cdot}11,\,p_j=1\,|\,C_{\max}\ \text{is NP-hard in the strong sense.}

Formally: if the language of PARTITION INTO PATHS OF LENGTH 2 is NP-hard, then the language of unary codes of yes-instances of the decision version of $Q2\,|\,res{\cdot}11,\,p_j=1\,|\,C_{\max}$ is NP-hard. The two speeds are arbitrary positive integers.

Milestones

The construction's key property (p. 15). In the constructed instance, two distinct jobs can be executed simultaneously if and only if their vertices are adjacent.
The triangle equivalence (proof of Theorem 2). $G$ has a partition into triangles if and only if the constructed instance on three identical machines has a feasible schedule with $C_{\max}\le t$ .
Theorem 2. $P3\,|\,res{\cdot}11,\,p_j=1\,|\,C_{\max}$ is NP-hard in the strong sense, given the NP-hardness of PARTITION INTO TRIANGLES.
The paths equivalence (proof of Theorem 3). $G$ has a partition into paths of length 2 if and only if the constructed instance on two uniform machines with speeds $q_1=2$ , $q_2=1$ has a feasible schedule with $C_{\max}\le t$ .

Significance

The results. Theorems 2 and 3 are two of the minimal NP-hard problems in the paper's classification. Together with Theorem 1 they place the borderline exactly: with unit resources whose number is part of the input, two identical machines are polynomial, while three identical machines, or two machines of different speeds, are strongly NP-hard. Strong NP-hardness rules out pseudo-polynomial algorithms unless P = NP, and it carries over to every more general resource type and machine environment in Fig. 1 and Fig. 2. Section 4.1 of the paper also derives hardness for $\sum C_j$ and $L_{\max}$ from these instances.

Formalizing it. The results are classical and proved on paper, but the paper's proofs are one sentence each ("Clearly", "It is easily seen"). No machine-checked proof exists, and the platform has no model of resource-constrained scheduling with real-valued time. This mission produces that model. It also produces a precise statement of strong NP-hardness on top of Cook's Turing-machine definitions, and the first formal NP-hardness reductions from graph partition problems to scheduling.

Difficulty

The scheduling half of each equivalence depends on the real-time model. On two uniform machines of speeds 2 and 1, jobs take time $\tfrac12$ and $1$ , so jobs on the fast machine start at half-integers or anywhere else. The resource constraint must hold at every real time, not at a finite set of checkpoints. An argument that treats time as integer slots applies to the triangle case but does not transfer to the paths case.

The complexity half needs polynomial-time computability of the construction on Cook's one-tape Turing machines, on encoded strings that include malformed inputs. It also needs closure of polynomial-time reductions under composition, which the imported complexity layer states but does not prove.

Formalization scope

Time and schedules. Start times are nonnegative reals, execution intervals are half-open $[S_j,C_j)$ , and the resource constraints are imposed at every real time. Schedules are nonpreemptive.
Indices. Jobs, machines and resources are 0-based (Fin n, Fin m, Fin l), so $q_1,q_2$ are q 0, q 1.
Decision versions. "NP-hard" refers to the decision version with a threshold $y$ . Thresholds are natural numbers and the $Q2$ speeds are positive integers. This restricted problem is a subproblem of the one with rational data, so its hardness is the stronger statement.
Encodings and strong NP-hardness. Instances are strings over a two-letter alphabet with every number in unary. Graphs are $t$ in unary followed by the $3t\times 3t$ adjacency matrix, so $|V|=3t$ is part of the instance. Languages contain only codes of yes-instances. Strong NP-hardness is NP-hardness of the unary code language. With unary numbers, $\mathrm{Max}(I)\le\mathrm{Length}(I)$ , so this is equivalent to Garey and Johnson's definition. The complexity layer is the published module CookPvsNP_defs.
Cited hypothesis. Each hardness theorem takes as its only hypothesis the NP-hardness of its source problem, which the paper cites from Garey and Johnson rather than proves. The hypothesis is a true statement about a nonempty, non-universal language. The statements are not weakened to a reduction between languages, and they assume nothing about P versus NP.
Source problems. The paper's phrase "three vertices, at most two of which are nonadjacent" is read as "at most one nonadjacent pair", which is Garey and Johnson's GT13. Reading it as "at most two nonadjacent pairs" would admit triples with a single edge and change the problem. PARTITION INTO PATHS OF LENGTH 2 reuses the published definition CubicP3Partition.P3Factor, a spanning non-induced $P_3$ -factor.
Construction. Resources are indexed by the nonadjacent pairs $j<k$ in lexicographic order, one per unordered pair and none for a pair $\{j,j\}$ . A diagonal resource would make every job infeasible.
Not trivial. A model that checks resources only at integer times, or only at start times, would make the paths equivalence false. A hypothesis on the target problem would make the goal circular. The definitions rule out both.

Welcome contributions: proofs of the two equivalences, polynomial-time computability of the construction on Cook's machines, and a general composition lemma for polynomial-time reductions. The composition lemma is reusable for every hardness mission built on CookPvsNP_defs.

Selected references

J. Błażewicz, J. K. Lenstra, A. H. G. Rinnooy Kan, Scheduling subject to resource constraints: classification and complexity, Discrete Applied Mathematics 5 (1983) 11–24. https://doi.org/10.1016/0166-218X(83)90012-4
M. R. Garey, D. S. Johnson, Complexity results for multiprocessor scheduling under resource constraints, SIAM Journal on Computing 4 (1975) 397–411. https://doi.org/10.1137/0204035
M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, Freeman, San Francisco, 1979, ISBN 0-7167-1045-5.
R. L. Graham, E. L. Lawler, J. K. Lenstra, A. H. G. Rinnooy Kan, Optimization and approximation in deterministic sequencing and scheduling: a survey, Annals of Discrete Mathematics 5 (1979) 287–326. https://doi.org/10.1016/S0167-5060(08)70356-X
S. Cook, The P versus NP problem, Clay Mathematics Institute Millennium Problems. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf

41 thms7 active usersReviewed

Completed

Combinatorics Graph Theory·Captain: hao jia

Immune High-Girth Bipartite Graphs (Feghali-Lucke-Paulusma-Ries 2025)Research Paper

Motivation

A matching cut is a vertex bipartition whose crossing edges form a matching. The property was introduced under the name decomposability and has links to graph algorithms, stable cutsets in line graphs, and several graph-labeling problems. An Open Problem Garden question asked whether sufficiently large girth forces a matching cut once average degree is bounded.

Feghali, Lucke, Paulusma, and Ries answered that question negatively. Their conference paper appeared at ISAAC 2023, and the version of record was published in Algorithmica in 2025. The paper proves NP-completeness for bipartite graphs of arbitrarily prescribed girth and bounded maximum degree. A central input, Lemma 5, is a stronger structural existence statement: for every girth threshold there is an immune $14$ -regular bipartite graph of at least that girth, and it has a perfect matching.

This is therefore a ResearchPaper mission, not a new open-problem mission. Its goal is to formalize the published theorem and its graph-theoretic consequence. Repository candidate constructions and finite arithmetic audits remain separate and are not credited as solving the problem.

Setting

For a finite simple graph $G$ and a vertex set $A\subseteq V(G)$ , the associated cut consists of all edges with one endpoint in $A$ and one in $V(G)\setminus A$ . The cut is nontrivial when both shores are nonempty. It is a matching cut when each vertex is incident with at most one crossing edge. A graph is called immune in the cited paper when it has no matching cut.

The girth is the length of a shortest simple cycle; forests have infinite girth. A graph is $14$ -regular when every vertex has exactly fourteen neighbors. Bipartiteness is witnessed by a partition into two independent sides. A perfect matching pairs every vertex with one adjacent partner.

The original OPG wording has a literal one-vertex boundary ambiguity: with nonempty shores required, $K_1$ has no matching cut, average degree zero, and infinite girth. The research-paper target avoids that vacuity by constructing connected graphs with at least two vertices, exact degree fourteen, and arbitrarily large finite girth.

Formalization targets

Lemma 5 — immune high-girth graphs

The main theorem follows the paper's structural lemma:

\forall g\ge3\ \exists G, \quad G\text{ is finite, connected, bipartite, and $14$-regular},

\operatorname{girth}(G)\ge g, \qquad G\text{ has no matching cut}, \qquad G\text{ has a perfect matching}.

The graph may depend on $g$ . The existence quantifier does not request an efficient algorithm or a numerical order bound.

Negative OPG consequence

A supporting theorem removes the perfect-matching and bipartite fields and records the direct substantive counterexample family:

\forall g\ge3\ \exists G, \qquad \overline d(G)=14<15, \quad \operatorname{girth}(G)\ge g, \quad G\text{ has no matching cut}.

Thus choosing $d=15$ refutes the intended universal assertion that some girth threshold works for every graph of average degree below $d$ .

Significance

The theorem shows that large girth and bounded degree do not force matching cuts. The examples are highly nontrivial: they are connected, regular, bipartite, and can have arbitrarily large girth. This separates local tree-like structure from the global expansion that prevents a matching cut.

Within the paper, the immune graphs serve as gadgets for hardness reductions. The journal theorem states that, for every $g\ge3$ , Matching Cut is NP-complete even for bipartite graphs of girth at least $g$ and maximum degree at most $60$ . Formalizing Lemma 5 supplies the graph-theoretic core needed to reconstruct that result without forcing this mission to formalize an entire complexity-theory reduction in its first stage.

Difficulty

Large girth alone makes bounded neighborhoods look like trees, and trees have many matching cuts. Immunity must therefore come from global expansion rather than short local cycles. The paper obtains the required family from Lubotzky–Phillips–Sarnak Ramanujan graphs and combines spectral and isoperimetric bounds to show that every nontrivial cut has too many crossing incidences to be a matching.

A formal proof must bridge several exact interfaces: existence of suitable primes, the finite Cayley-graph construction, bipartiteness and regularity, the girth lower bound, the spectral-to-isoperimetric inequality, and Hall's theorem for the perfect matching. None of these can be replaced by a finite sample or an asymptotic slogan.

Formalization scope

Graphs are finite and simple. Connectedness is nonempty mutual graph reachability. A simple cycle is a cyclic list of at least three distinct vertices; girth at least $g$ means every such cycle has length at least $g$ , so forests satisfy every threshold. A matching cut requires both shores nonempty and is encoded by the condition that every vertex has at most one crossing neighbor. A perfect matching is represented by an adjacent involution.

The main theorem explicitly requires at least two vertices, although exact 14-regularity already forces nontrivial order; the redundant bound documents exclusion of the $K_1$ ambiguity. The mission does not claim that the frozen OPG contract was well-posed at order one. It formalizes the paper's substantive counterexample family and the consequence for the intended question.

Candidate files in the associated repository explore alternative bounded-degree constructions and integer counts. They are candidate_only and are not proof dependencies. Contributions should follow the published Lemma 5 and its cited inputs, or provide a separately sourced proof of the same declaration. The later maximum-degree-60 NP-completeness theorem is welcome as a future extension after the finite complexity framework is fixed.

Selected references

C. Feghali, F. Lucke, D. Paulusma, and B. Ries, Matching Cuts in Graphs of High Girth and H-Free Graphs, Algorithmica 87 (2025), 1199–1221. https://doi.org/10.1007/s00453-025-01318-8
C. Feghali, F. Lucke, D. Paulusma, and B. Ries, ISAAC 2023 version. https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ISAAC.2023.31
A. Lubotzky, R. Phillips, and P. Sarnak, Ramanujan graphs, Combinatorica 8 (1988), 261–277. https://doi.org/10.1007/BF02126799
Open Problem Garden, Matching cut and girth. https://www.openproblemgarden.org/op/matching_cut_and_girth

20 thms6 active usersReviewed

Linear Optimization Operations Research Optimization·Captain: ORdos

Smale's Ninth Problem: Strongly Polynomial Linear ProgrammingOpen Problem

The problem of solving linear inequalities

The linear feasibility problem takes a matrix $A \in \mathbb{R}^{m\times n}$ and a vector $b \in \mathbb{R}^m$ and asks whether the system of $m$ linear inequalities in $n$ real unknowns

\{\,x \in \mathbb{R}^n \mid Ax \ge b\,\} \;\ne\; \emptyset

has a solution. By linear programming duality, optimizing a linear objective over such a set reduces to feasibility, so this decision problem carries the whole complexity of linear programming.

What "polynomial time" means here depends on the machine. In the bit model the input is a list of rational numbers, its size $L$ counts the bits of all numerators and denominators, and an algorithm is polynomial if it runs in time $\mathrm{poly}(m, n, L)$ . In the real-number model the input is a list of $mn + m$ exact real numbers, each arithmetic operation ( $+, -, \times, \div$ ), comparison, or memory move costs one unit, and a running time may only depend on $m$ and $n$ . An algorithm polynomial in this second sense is what Smale asks for; the closely related bit-model notion — $\mathrm{poly}(m,n)$ arithmetic operations and polynomially bounded intermediate bit sizes — is called strongly polynomial. This mission fixes the real-number model precisely as a Blum–Shub–Smale (BSS) machine (Blum–Shub–Smale 1989): a finite program of instructions acting on a bi-infinite tape $\mathbb{Z} \to \mathbb{R}$ of real registers — loads of arbitrary real machine constants, exact field arithmetic at fixed addresses, two-sided tape shifts, a sign-test branch, and accept/reject — with cost equal to the number of executed instructions. The convention that costs something: the program must be uniform, one finite instruction list serving every $m$ , $n$ , and every real instance. Uniformity is exactly what separates the question from point-location tricks available to non-uniform families of decision trees.

Why it matters

For optimization, the question is the last gap in the complexity of its central problem. Linear programs with combinatorial structure already admit strongly polynomial algorithms — Tardos (1986) solved every LP whose running time may depend on the entries of $A$ but not on $b$ or $c$ , covering network flows and all $\{0,\pm1\}$ -constraint problems — and a positive answer for general LP would extend that unification to the whole class, while explaining why simplex-type methods behave so well in practice (Spielman–Teng 2004).

For the theory of computation over the reals, the problem is a benchmark for what unit-cost exact arithmetic can do: it is Problem 9 on Smale's list of mathematical problems for the twenty-first century (Smale 1998), posed in the BSS model as the real-number analogue of the P-versus-NP style questions of that program, and it interacts with polyhedral combinatorics through the polynomial Hirsch conjecture: a polynomial bound on polytope diameters is a necessary condition for any polynomial pivot rule. A problem that calibrates both the practice of optimization and the foundations of real computation is a subject, not a special case.

The question and what is known

\textbf{Question (Smale's 9th).}\quad \text{Is there a uniform BSS program deciding } \{x \mid Ax \ge b\} \ne \emptyset \text{ in } \mathrm{poly}(m,n) \text{ steps?}

The timeline splits into a negative branch (lower bounds against algorithm classes) and a positive branch (polynomial algorithms in weaker senses).

Lower bounds. Klee–Minty (1972) constructed a deformed cube on which Dantzig's largest-coefficient simplex rule visits all $2^n$ vertices; analogous exponential examples were later found for essentially every deterministic pivot rule, and randomized rules were driven to subexponential lower bounds by Friedmann–Hansen–Zwick (2011) — against upper bounds of $\exp(O(\sqrt{n \log n}))$ from Kalai (1992) and Matoušek–Sharir–Welzl (1996). On the interior-point side, Allamigeon–Benchimol–Gaubert–Joswig (2018) showed by tropical methods that log-barrier path following is not strongly polynomial, and Allamigeon–Gaubert–Vandame (2022) extended this to every self-concordant barrier: no interior-point method of that class can settle the question positively.

Polynomial algorithms in weaker senses. Khachiyan (1979/80) proved LP feasibility is polynomial in the bit model via the ellipsoid method; Karmarkar (1984) and then Renegar (1988) brought interior-point methods to $O(\sqrt{n}\,L)$ iterations. Megiddo (1984) solved LP in linear time for every fixed dimension; Tardos (1986) gave the combinatorial strongly polynomial class; Vavasis–Ye (1996) and Dadush–Huiberts–Natura–Végh (2020) replaced the bit size by condition measures of $A$ alone; Ye (2011) proved policy iteration strongly polynomial for fixed-discount Markov decision processes.

The central difficulty is visible in every positive result: each known iteration count is controlled by a scale-dependent quantity — bit length, condition number, barrier curvature — that is unbounded over the real instances with $m, n$ fixed. The naive plan, "run the ellipsoid method and round", fails at its first step in the real model: the number of iterations needed to separate a feasible system from an infeasible one grows with the thinness of the feasible set, which is not a function of $(m, n)$ ; no data-independent perturbation $\varepsilon$ exists when the data are arbitrary reals. All results above are proved on paper only; none has a machine-checked proof in the literature. What is already formalized, on this platform, is the substrate this mission builds on: the simplex iteration (mission Introduction to Linear Optimization IV), the ellipsoid method with its volume-halving correctness theorem (XI), interior-point path following (XII), and self-concordance with the barrier method (Convex Optimization VI).

A hierarchy of formalization targets

The mission's milestone list realizes this hierarchy in order; each level states what it deliberately leaves open.

Level 0 — the model works. A uniform BSS program decides one-variable feasibility in linear time:

\exists\,P,\,C\ \ \forall m,\ \forall (a,b) \in \mathbb{R}^m \times \mathbb{R}^m:\ P \text{ decides } \{x \in \mathbb{R} \mid a_i x \ge b_i\ \forall i\} \ne \emptyset \text{ within } C(m{+}1) \text{ steps}.

It fixes nothing about $n \ge 2$ ; its role is to certify that the machine model and cost semantics of the goal are non-vacuous.

Level 1 — the classical method is exponential. On the Klee–Minty cube, Dantzig's rule admits a run of

2^n - 1 \text{ pivots}

from the all-slack basis to the optimum. It leaves open all other pivot rules — extensions to further rules are welcome as strengthenings.

Level 2 — the bit model succeeds. Through the Cramer–Hadamard solution bound $|x_j| \le n!\,U^n$ and the perturbation estimates, Khachiyan's theorem: for integer data bounded by $U$ , every admissible ellipsoid run decides feasibility within

t^* \le 10^6\,(n{+}2)^4(\log_2 U + n + 2) \text{ iterations}.

The generous constants are deliberate — only the polynomial order is load-bearing. This level leaves open exactly the dependence on $\log U$ .

Level 3 — the goal (open). A uniform program with data-independent polynomial cost:

\exists\,P,\,C,\,d\ \ \forall m, n, A, b:\ P \text{ decides } \{x \mid Ax \ge b\} \ne \emptyset \text{ within } C\,(mn + m + 2)^d \text{ steps}.

The statement asserts only the shape of the truth — no hard-coded degree or constant — so it is stable under every future quantitative improvement. These levels do not exhaust the project: Tardos' combinatorial LP theorem, Ye's fixed-discount MDP result, and impossibility statements for restricted program classes in the style of Allamigeon–Gaubert–Vandame are natural later milestones.

Formalization scope

Polyhedra, simplex states, pivots, and ellipsoid runs are the platform's existing LinearOptimization development over Matrix (Fin m) (Fin n) ℝ, with $\{x \mid Ax \ge b\}$ as polyhedron A b; algorithms with data-dependent iteration counts are formalized as run predicates, as in the parent missions. The new SmaleNinth definitions supply what the goal genuinely needs and the run-predicate style cannot express: a concrete inductive type of BSS programs with operational semantics and unit-cost accounting, the Klee–Minty data with Dantzig's rule, and the explicit Khachiyan constants. One convention closes the degenerate escape hatch: the goal quantifies over finite BSSProgram terms under the fixed encodeLP input convention — formalizing "algorithm" as an arbitrary function $\mathbb{R}^{mn+m} \to \mathrm{Bool}$ would make the statement trivially true and is not the theorem. Division is totalized as $x/0 = 0$ and the branch test is $x_i \le 0$ ; both are benign for the class of programs quantified over.

The machine module is infrastructure beyond this mission — any real-number complexity statement (other Smale problems, sums-of-square-roots, BSS-completeness) can reuse it, as can any pivot-rule lower bound reuse the Klee–Minty module. Formalization forces distinctions the literature leaves informal: which machine variant carries the unit-cost claim, how ties in Dantzig's rule are resolved, and which of the interchangeable Khachiyan constants each estimate actually needs. Welcome contributions include proofs of any milestone, alternative exponential instances for other pivot rules, sharper constants in the Khachiyan module, and ports of the known strongly polynomial special cases.

Selected references

L. Blum, M. Shub, S. Smale, On a theory of computation and complexity over the real numbers, Bull. AMS 21(1):1–46, 1989. DOI
S. Smale, Mathematical problems for the next century, Math. Intelligencer 20(2):7–15, 1998. DOI
V. Klee, G. J. Minty, How good is the simplex algorithm?, in Inequalities III, Academic Press, 1972, pp. 159–175.
L. G. Khachiyan, Polynomial algorithms in linear programming, USSR Comput. Math. Math. Phys. 20:53–72, 1980. DOI
N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4:373–395, 1984. DOI
J. Renegar, A polynomial-time algorithm, based on Newton's method, for linear programming, Math. Programming 40:59–93, 1988. DOI
É. Tardos, A strongly polynomial algorithm to solve combinatorial linear programs, Oper. Res. 34(2):250–256, 1986. DOI
N. Megiddo, Linear programming in linear time when the dimension is fixed, J. ACM 31(1):114–127, 1984. DOI
G. Kalai, A subexponential randomized simplex algorithm, STOC 1992. DOI
O. Friedmann, T. D. Hansen, U. Zwick, Subexponential lower bounds for randomized pivoting rules for the simplex algorithm, STOC 2011. DOI
D. A. Spielman, S.-H. Teng, Smoothed analysis of algorithms: why the simplex algorithm usually takes polynomial time, J. ACM 51(3):385–463, 2004. DOI
S. A. Vavasis, Y. Ye, A primal-dual interior point method whose running time depends only on the constraint matrix, Math. Programming 74:79–120, 1996. DOI
Y. Ye, The simplex and policy-iteration methods are strongly polynomial for the Markov decision problem with a fixed discount rate, Math. Oper. Res. 36(4):593–603, 2011. DOI
X. Allamigeon, P. Benchimol, S. Gaubert, M. Joswig, Log-barrier interior point methods are not strongly polynomial, SIAM J. Appl. Algebra Geom. 2(1):140–178, 2018. DOI
X. Allamigeon, S. Gaubert, N. Vandame, No self-concordant barrier interior point method is strongly polynomial, STOC 2022. arXiv
D. Dadush, S. Huiberts, B. Natura, L. A. Végh, A scaling-invariant algorithm for linear programming whose running time depends only on the constraint matrix, STOC 2020. arXiv
D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997 (Chapters 3, 8, 9 — formalized in the Introduction to Linear Optimization mission series).
B. Korte, J. Vygen, Combinatorial Optimization: Theory and Algorithms, 6th ed., Springer, 2018, §4.1–4.5.

29 thms6 active usersReviewed

Completed

Captain: joe

The Sipser–Gács–Lautemann TheoremResearch Paper

Randomness appears to enlarge efficient computation, but the Sipser–Gács–Lautemann theorem places every bounded-error probabilistic polynomial-time language at the second level of the polynomial hierarchy, giving one of complexity theory’s foundational limits on the power of randomization.

66 thms6 active usersReviewed

Captain: xuanji

AlphaEvolve Eighth-Power Bound: omega < 2.371177Research Paper

Formalize $\omega < 2.371177$ , the current record from Dupont, Eisenberger, Kozlovskii, Mehrabian, Ruiz, See, Zhou, Alman, Vassilevska Williams and Balog (arXiv:2608.16884, August 2026).

The paper applies the combination-loss laser method of Alman et al. (arXiv:2404.16349), formalized here as the $\omega < 2.37134$ entry, to $CW_5^{\otimes 8}$ . That is level $\ell^* = 4$ instead of 3, with an exact rational certificate of about $7\cdot 10^6$ parameters found by gradient-based optimization and AlphaEvolve. The authors state that the solution and verification code are being prepared for release.

6 thms5 active usersReviewed

Completed

Combinatorics Operations Research·Captain: mikedeng1

Competitive Paging Algorithms IV: An Algorithm Competitive against Several Others Exists iff the Reciprocal Ratios Sum to at Most 1Research Paper

Motivation

Paging is the problem of managing a fast memory that holds $k$ pages out of $n$ : when a requested page is not in fast memory (a page fault), some resident page must be evicted, and the cost of an algorithm is its number of faults. Practitioners have many eviction rules. Least-recently-used (LRU) performs well on real workloads but can be $k$ times worse than the optimal off-line schedule; the randomized marking algorithm of the same paper is $2H_k$ -competitive and so has better worst-case guarantees. Fiat, Karp, Luby, McGeoch, Sleator and Young asked in 1991 whether one on-line algorithm can combine the advantages of several given ones, and answered the question exactly: the attainable combinations of ratios are characterized by one inequality (arXiv:cs/0205038, §6).

The question of combining on-line algorithms has since become a theme of its own: combining heuristics with worst-case-safe algorithms, and, more recently, combining machine-learned predictions with robust fallbacks, both ask for the same kind of guarantee against several reference algorithms at once.

Setting

A type $(k,n)$ consists of $k$ servers and a finite set $M$ of $n$ vertices with the uniform metric: two distinct vertices are at distance $1$ . This is paging: vertices are pages, the vertices covered by servers are the pages in fast memory, and a server move is a page fault.

A deterministic on-line algorithm $A$ of type $(k,n)$ has an initial configuration of its $k$ servers and, after each request $r\in M$ , moves servers so that some server covers $r$ ; its configuration after a request sequence depends only on that sequence. Its cost $C_A(\sigma)$ on a request sequence $\sigma$ is the total distance its servers travel, i.e. the number of server moves.

For algorithms $A$ and $B$ of the same type and a constant $c$ , $A$ is $c$ -competitive against $B$ if there is a constant $a$ such that for every request sequence $\sigma$

C_A(\sigma)\le c\cdot C_B(\sigma)+a .

A sequence $c^*=(c(1),\dots,c(m))$ of positive reals is realizable if for every type $(k,n)$ and every $m$ deterministic on-line algorithms $B(1),\dots,B(m)$ of that type there is a deterministic on-line algorithm $A$ of the same type that is $c(i)$ -competitive against $B(i)$ for every $i$ .

Formalization targets

Goal: Theorem 6

For $m\ge1$ and positive reals $c(1),\dots,c(m)$ ,

c^*\ \text{is realizable}\iff \sum_{1\le i\le m}\frac1{c(i)}\le 1 .

Milestones

In the order of the paper's proof:

Punishments are paid for. If $A$ punishes $B$ at a time step (an $A$ -interval on a vertex $v$ ends at that step and contains the end of a $B$ -interval on $v$ that began no later), then $B$ has moved a server; the number of such steps is at most $C_B(\sigma)$ .
A fault leaves room to punish. If $|S_A|=k$ , $|S_B|\le k$ , $x\in S_B$ and $x\notin S_A$ , then some $u\in S_A$ is not in $S_B$ .
The greedy quota claim. If $\sum_i 1/c(i)\le 1$ and each unit of cost punishes the $B(i)$ minimizing $c(i)(\mathrm{PUN}(i)+1)$ (other algorithms may be punished incidentally), then after cost $r$ every $B(i)$ has been punished at least $\lfloor r/c(i)\rfloor$ times.
Shuttle algorithms. With $2m-1$ servers on $2m$ vertices there are $m$ algorithms, each keeping all vertices outside its own pair covered, no two of which move at the same step; in particular their total cost on any $\sigma$ is at most $|\sigma|$ .
A forcing adversary. With $2m-1$ servers on $2m$ vertices every algorithm can be forced to move at each of $N$ steps, so $C_A(\tau(N))\ge N$ .

Significance

The result. Theorem 6 is an exact characterization, not a bound: the region of simultaneously attainable ratios against arbitrary deterministic paging algorithms is $\{c:\sum 1/c(i)\le 1\}$ . For example, any two paging algorithms can be combined into one that is $2$ -competitive against each, and no better symmetric pair is possible in general. Combined with Theorem 7 of the same paper (not part of this mission), the same region is attainable against randomized algorithms, which is how LRU's practical behaviour and the marking algorithm's $2H_k$ worst-case guarantee can be obtained within constant factors by one algorithm.

Formalizing it. The theorem has been proved since 1991; no machine-checked proof is known. A formal proof produces a reusable notion of competitiveness of one on-line algorithm against another, built on the published KServer_model definitions, and a formal account of the scheduling fact at the core of the sufficiency proof.

Difficulty

Sufficiency looks like an averaging argument, but the combined algorithm cannot simulate the $B(i)$ and follow one of them: switching between their configurations costs up to $k$ per switch, which no additive constant absorbs. The accounting has to charge each of $A$ 's faults to a specific move of a specific $B(i)$ , and the charge must be injective; the paper's claim that $C_B(\sigma)$ is at least the number of punishments is where this happens, and it depends on how server intervals are matched. The allocation of faults to algorithms is then a deadline-scheduling problem whose feasibility is exactly $\sum 1/c(i)\le 1$ , and the floor functions make the counting delicate at the boundary. The paper's own definition of punishment only counts intervals that start with a move, so the first $k$ faults of $A$ (servers on their initial vertices) need separate treatment; they are absorbed by the additive constant.

Necessity needs the right family of hard instances: the $m$ algorithms must never move at the same step, which pins the type to $(2m-1,2m)$ .

Formalization scope

The Lean development works in the namespace CompetitivePaging.Combining and imports the published KServer_model definitions: KServer.OnlineAlgorithm k M (a configuration map from request prefixes to Fin k → M with a serving condition) and OnlineAlgorithm.cost. Committed conventions:

a type $(k,n)$ is any k : ℕ and any finite M : Type with a metric in which distinct points are at distance $1$ ; realizability quantifies over all of them, never over one fixed type;
servers are labelled; each algorithm has its own initial configuration, and the additive constant $a$ is chosen before the request sequence;
$c(i)>0$ and $m\ge1$ are hypotheses of the goal, as in the paper; without positivity, $1/0=0$ in Lean would make a zero ratio free;
time $t$ is the step processing the $t$ -th request; the paper's $\mathrm{PUN}$ counts time steps.

Trivializing encodings are ruled out: realizability is not stated for a single fixed type, the metric is not the metric of Fin n, and the competitive constant is not allowed to depend on the request sequence.

A complete proof needs the construction of the punishing algorithm as a KServer.OnlineAlgorithm (a lazy, injective algorithm whose moves depend on the prefix and on the $B(i)$ 's configurations), the injective charging argument, the scheduling lemma, and the explicit shuttle algorithms. The scheduling lemma and the charging lemma are independent of paging and reusable. Proofs of any milestone are welcome, as are alternative statements of the sufficiency construction.

Selected references

A. Fiat, R. M. Karp, M. Luby, L. A. McGeoch, D. D. Sleator, N. E. Young, Competitive Paging Algorithms, J. Algorithms 12(4):685–699, 1991. doi:10.1016/0196-6774(91)90041-V; preprint arXiv:cs/0205038.
D. D. Sleator, R. E. Tarjan, Amortized efficiency of list update and paging rules, Comm. ACM 28(2):202–208, 1985. doi:10.1145/2786.2793
M. S. Manasse, L. A. McGeoch, D. D. Sleator, Competitive algorithms for server problems, J. Algorithms 11(2):208–230, 1990. doi:10.1016/0196-6774(90)90003-W

9 thms5 active usersReviewed

Computational Geometry Linear Optimization Operations Research·Captain: mikedeng1

Linear Programming in Linear Time When the Dimension Is Fixed: Fixed-Dimension LP Feasibility Decided in Linear Time on the Real RAMResearch Paper

Motivation

A linear program asks for a point $x\in\mathbb{R}^d$ minimizing $c^Tx$ subject to $n$ linear inequalities $\sum_{j=1}^d a_{ij}x_j\ge b_i$ . Many problems in computational geometry and statistics are linear programs with few variables and very many constraints: separating two point sets by a line or plane, fitting a line in the Chebyshev ( $L_\infty$ ) norm, finding the smallest disk or ball containing a point set (a related convex problem). For these problems the number of variables $d$ is a small constant, and what matters is how the running time grows with $n$ .

Nimrod Megiddo showed that for every fixed $d$ the problem can be solved in time $C(d)\cdot n$ (J. ACM 31(1), 1984).

Timeline.

1983. Megiddo (SIAM J. Comput. 12) and, independently, Dyer (SIAM J. Comput. 13 (1984)) give linear-time algorithms for $d=2$ and $d=3$ .
1984. Megiddo extends the method to every fixed $d$ , with $C(d)<2^{2^{d+2}}$ (the paper formalized here).
1988–1991. Clarkson (J. ACM 42 (1995), conference version 1988) gives a randomized algorithm with expected time $O(d^2n)+d^{O(\sqrt d)}\log n$ . Seidel (Discrete Comput. Geom. 6 (1991)) gives a simple randomized $O(d!\,n)$ algorithm.
1992–1996. Matoušek, Sharir and Welzl and, independently, Kalai give subexponential randomized bounds. Chazelle and Matoušek derandomize the linear dependence with $C(d)=d^{O(d)}$ (J. Algorithms 21 (1996)).

Setting

Fix $d$ . An instance is a matrix $A\in\mathbb{R}^{n\times d}$ and a vector $b\in\mathbb{R}^n$ , and its feasible region is the polyhedron $P(A,b)=\{x\in\mathbb{R}^d: Ax\ge b\}$ . Here $n$ is the number of constraints and $d$ the number of variables.

The model of computation is the real RAM. A program is a finite list of instructions acting on real registers, integer pointer registers and a memory $\mathbb{Z}\to\mathbb{R}$ . It performs exact $+,-,\times,/$ on reals at unit cost, tests the sign of a real, sets, copies, increments, decrements and compares pointers, and loads and stores through pointers. The input is the standard encoding of $(A,b)$ in memory: the numbers $n$ and $d$ , then $A$ row by row, then $b$ . A program decides an instance within $T$ steps with output $\beta\in\{\text{accept},\text{reject}\}$ if it halts on that output after at most $T$ steps.

Megiddo's method rests on multidimensional search. There is an unknown point $x^*\in\mathbb{R}^d$ and an oracle that, for any hyperplane $\{x: a^Tx=b\}$ , answers whether $a^Tx^*<b$ , $=b$ or $>b$ . Given hyperplanes $H_i=\{a_i^Tx=b_i\}$ with $a_i\ne0$ , the question is how many oracle calls determine the position of $x^*$ relative to all of them. A search strategy is a ternary decision tree: inner nodes are hyperplane queries, leaves carry outputs, and the tree is built from the data alone. For linear programming, $x^*$ is an optimal solution, or a minimizer of the infeasibility function $f(x)=\max_i(b_i-a_i^Tx)$ when the system is infeasible. The oracle is implemented by solving problems in $d-1$ variables.

Formalization targets

Goal: linear-time feasibility on the real RAM

\forall d\ \exists R\ \exists C\ \forall n\ \forall A\in\mathbb{R}^{n\times d},\,b\in\mathbb{R}^n:\quad R\text{ decides within }C\,(n+1)\text{ steps whether } \{x: Ax\ge b\}\neq\emptyset.

The program and the constant depend on $d$ only. No explicit form of $C(d)$ is fixed.

Milestones

One query settles half of $n$ hyperplanes on the line ( $A(1)=1$ , $B(1)=\tfrac12$ ).
$v(\epsilon)=(1,\epsilon,\dots,\epsilon^{d-1})$ is orthogonal to some $a_i$ for at most $n(d-1)$ values of $\epsilon$ , so there is a basis in which all $a_{ij}\ne0$ .
For hyperplanes of opposite slopes in the $(x_1,x_2)$ plane, the answers for $H^{(1)}_{ik}$ and $H^{(2)}_{ik}$ settle one of $H_i$ , $H_k$ .
A linearly dependent pair of opposite slopes has $a_{i1}=a_{k1}=0$ , and the middle hyperplane settles one of them.
Approach I: $2^{d-1}$ queries settle at least $\lfloor 2^{1-2^d}n\rfloor$ hyperplanes.
$C(d)\log n$ queries settle all $n$ hyperplanes.
If a hyperplane contains no optimal point, all optimal points lie on one side of it.
The oracle, Case I: at an optimum relative to $\{x_d=0\}$ , two auxiliary systems decide the side or certify global optimality.
The oracle, Case II: at a minimizer of $f$ on $\{x_d=0\}$ , systems (1) and (2) decide the side or certify infeasibility.

Significance

The result. For every fixed dimension, linear programming is solvable in time linear in the number of constraints. The algorithm is also strongly polynomial in fixed dimension: its operation count does not depend on the bit size of the data. Deciding whether the optimum is at most $t$ is feasibility of $Ax\ge b$ together with $-c^Tx\ge-t$ , so the goal also covers the decision form of optimization. The prune-and-search technique of the paper, which discards a constant fraction of the constraints per round, became a standard tool of computational geometry.

Formalizing it. The result is proved and classical. The platform already has the cases $d=1$ (linear time) and $d=2$ (quadratic time, by Fourier–Motzkin elimination) on the same machine and input encoding (SmaleNinth.real_ram_decides_one_variable_lp_linear, SmaleNinth.real_ram_decides_two_variable_lp_quadratic). No machine-checked proof of the general statement is known. The work consists of the query-complexity layer (milestones 1–6), the convex-analytic correctness of the oracle (milestones 7–9), and a real-RAM implementation with a step count linear in $n$ , including linear-time median selection. Alternative proofs, for example through Clarkson's or Seidel's algorithms made deterministic, are welcome for the goal.

Difficulty

The obvious approach is to find the optimum by testing constraints one by one or by eliminating variables. Fourier–Motzkin elimination produces $\Theta(n^2)$ constraints after one step. Pivoting methods have no known bound linear in $n$ . The key difficulty is to discard a constant fraction of the constraints using only a constant number of recursive calls in dimension $d-1$ , when no single hyperplane test gives information about more than one constraint. The multidimensional search layer gives this, and it is where the pairing of hyperplanes by slope and the degenerate cases (dependent pairs, zero coefficients) have to be handled exactly. At the machine level, the step count must stay linear in $n$ for a fixed program, so every median selection and every recursive call must be implemented within the budget, with the recursion depth depending on $d$ only.

Formalization scope

Machine and input. The machine is the platform's real RAM SmaleNinth.RAMProgram with RAMDecidesInTime, and the input convention is SmaleNinth.encodeLP (published definitions, reused unchanged). No instruction is added: there is no LP, median, floor or sort primitive. Time is the number of machine steps.
Quantifier order. $\forall d\ \exists R\ \exists C\ \forall n, A, b$ . The bound is $C(n+1)$ in the number $n$ of constraints, so that the machine can halt at $n=0$ . The paper's $C(d)<2^{2^{d+2}}$ counts unspecified units of "effort" with an unquantified $\theta(nd)$ term, and it is not transferred to machine steps. Where a milestone's proof fixes a constant exactly, the constant is stated: $2^{d-1}$ queries and $\lfloor n/2^{2^d-1}\rfloor$ settled hyperplanes in milestone 5.
Feasibility only. The machine outputs accept or reject. Returning an optimizer, "unbounded", or a minimizer of $f$ is not part of the goal. The case $d=0$ is included.
Query trees. Nodes are queries compare (a ⬝ᵥ x) b and nothing else, leaves hold fixed values, and correctness is required for every $x$ . A tree over arbitrary tests of $x$ would make milestones 5 and 6 empty, and it is excluded by the definition.
Indices. The paper's $x_1,x_2$ are indices 0, 1 of Fin (d + 2), and its $x_d$ is Fin.last d of Fin (d + 1).
Corrections. Two passages of §4 are stated in corrected form. The Case I auxiliary objective includes the $\pm c_d$ term of the direction. In Case II, feasibility of (1) puts improvement in $\{x_d>0\}$ , where the page's last sentence says $\{x_d<0\}$ . The pairing claim carries $a_{k1}a_{i2}-a_{k2}a_{i1}\ne0$ , the hypothesis its argument uses, since linear independence alone does not give it.
Not included. Approach II and its bound $O(n(\log n)^{d^2})$ , the remarks on slowly growing $d$ , the randomized variants, and the applications of §1.
Reusable parts. The query-tree definition and milestones 1–6 apply to any prune-and-search problem with a hyperplane oracle. The oracle lemmas (7–9) are statements about convex piecewise-linear functions and polyhedra.

Selected references

N. Megiddo, Linear programming in linear time when the dimension is fixed, J. ACM 31(1):114–127, 1984. https://doi.org/10.1145/2422.322418
N. Megiddo, Linear-time algorithms for linear programming in $R^3$ and related problems, SIAM J. Comput. 12(4):759–776, 1983. https://doi.org/10.1137/0212052
M. E. Dyer, Linear time algorithms for two- and three-variable linear programs, SIAM J. Comput. 13(1):31–45, 1984. https://doi.org/10.1137/0213003
K. L. Clarkson, Las Vegas algorithms for linear and integer programming when the dimension is small, J. ACM 42(2):488–499, 1995. https://doi.org/10.1145/201019.201036
R. Seidel, Small-dimensional linear programming and convex hulls made easy, Discrete Comput. Geom. 6:423–434, 1991. https://doi.org/10.1007/BF02574699
B. Chazelle, J. Matoušek, On linear-time deterministic algorithms for optimization problems in fixed dimension, J. Algorithms 21(3):579–597, 1996. https://doi.org/10.1006/jagm.1996.0046

16 thms5 active usersReviewed

Completed

Captain: marwahaha

Coppersmith–Winograd Bound: omega < 2.376Research Paper

AI generated but i think correct. I think the milestones make it really annoying but the central theorem looks correct.

Motivation

The matrix-multiplication exponent measures the asymptotic number of field operations needed to multiply two square matrices. A bound $\omega<c$ means that, for every $\varepsilon>0$ , two $n\times n$ matrices can be multiplied using $O(n^{c+\varepsilon})$ arithmetic operations. Matrix multiplication is a central benchmark in algebraic complexity and a primitive for many algorithms in linear algebra, graph theory, and symbolic computation.

After Strassen showed that $\omega<3$ , a sequence of tensor constructions reduced the exponent further. Schönhage's asymptotic sum inequality made it possible to exploit simultaneous matrix products rather than a single square product. In 1990, Don Coppersmith and Shmuel Winograd combined an explicit low-border-rank tensor with a block extraction argument based on Salem--Spencer sets. Their basic analysis gave $\omega<2.38719$ ; coupling the random weights in the tensor square sharpened this to $\omega<2.375477$ , hence the exact rational consequence $\omega<2.376$ .

This mission formalizes that historical Coppersmith--Winograd result. It follows the source tensor and its actual block restrictions, while excluding placeholder “laser values” that are not backed by extracted direct sums of matrix-multiplication tensors.

Setting

For a field $K$ , an order-three tensor is represented by three finite-dimensional $K$ -vector spaces and an element of their tensor product. The matrix-multiplication tensor

\langle a,b,c\rangle_K =\sum_{i<a}\sum_{j<b}\sum_{k<c} x_{ij}\otimes y_{jk}\otimes z_{ki}

encodes multiplication of an $a\times b$ matrix by a $b\times c$ matrix. A restriction applies one linear map to each tensor leg. A degeneration permits those maps to depend polynomially on a formal parameter and selects their first nonzero coefficient. Thus a degeneration from the diagonal tensor $I_r$ is a border-rank certificate $\underline R(T)\le r$ .

The Coppersmith--Winograd tensor with parameter $q$ is

T_q= \sum_{i=1}^{q} (x_0y_i z_i+x_i y_0z_i+x_i y_i z_0) +x_0y_0z_{q+1}+x_0y_{q+1}z_0+x_{q+1}y_0z_0.

It has border rank at most $q+2$ . Its coordinates carry three classes, indexed by $0,1,2$ , and its six nonzero block types are

(0,1,1),\ (1,0,1),\ (1,1,0),\ (0,0,2),\ (0,2,0),\ (2,0,0).

The first three blocks are matrix-multiplication tensors with dimensions $(1,1,q)$ , $(q,1,1)$ , and $(1,q,1)$ ; the other three are scalar products. Tensor powers therefore contain many typed rectangular matrix products. The laser method selects a large family with disjoint coordinate blocks and applies Schönhage's asymptotic sum inequality to all surviving products simultaneously.

Formalization targets

Goal: the 1990 Coppersmith--Winograd bound

For every field $K$ ,

\operatorname{matMulExp}(K)<\frac{297}{125}=2.376.

The Lean goal has the same quantified proposition and the same matMulExp definition as the existing Schönhage-bound mission; only the theorem identifier and rational endpoint change.

Tensor and block foundations

The development records the characteristic-free order-three degeneration

T_q\unlhd I_{q+2}

and the exact matrix-product dimensions associated with every supported type sequence in $T_q^{\otimes N}$ . These statements identify the algebraic input before any asymptotic counting is used.

Coupled-weight extraction

For $q=6$ , the tensor-square grading and the coupled-weight pruning must produce the direct sums and asymptotic inequality stated in Section 8 and in the coupled-constituent lemma on journal pp. 270--272. The final numerical milestone certifies the rational endpoint $297/125$ from exact inequalities, rather than treating the decimal $2.375477$ as a proof object.

Significance

The result was the strongest matrix-multiplication bound for roughly two decades and introduced the tensor family that underlies the classical laser-method line of work. A formal proof supplies a checked bridge from an explicit border-rank identity to an exponent bound whose combinatorial extraction is substantially more delicate than the earlier Schönhage examples.

The formalization also produces reusable infrastructure. The order-three CW degeneration is an explicit polynomial-family test case over arbitrary fields. The six block identifications and type-count formulas can be reused in analyses of tensor powers. A faithful extraction predicate, stated through actual restrictions to direct sums of MMObj tensors, separates sound laser arguments from formulas that count incompatible or coordinate-sharing blocks as independent.

The mathematical bound is known. The open work is its machine-checked reconstruction in Lean. The border-rank theorem, per-type matrix-product restriction layer, tensor-square support invariant, balanced block calculation, Salem--Spencer set theorem, and exact $q=6$ numerical endpoint are already proved. The unrestricted value/rank bridge, the coupled-constituent extraction, and the full Section 8 auxiliary inequality remain the substantive frontier.

Difficulty

The main difficulty is not expanding $T_q$ or evaluating a decimal logarithm. A tensor power contains exponentially many typed terms, but most share variables. They cannot all be placed in a direct sum, and counting all joint type sequences overestimates the usable matrix products. The source hashes coordinate blocks into a large progression-free set and prunes collisions so that the surviving blocks are genuinely independent.

The $2.376$ improvement adds a second layer. It begins with $T_q^{\otimes2}$ , regroups variables into five classes, couples weights that were independent in the simpler analysis, and estimates a nontrivial central block by a further extraction. A formal proof must track the direction of every restriction, the exact multiplicities of all block types, and the loss introduced by pruning. Replacing exponential surviving-block counts by a polynomial number of blocks, or using joint entropy without the marginal compatibility constraints, changes the mathematical claim and is outside the mission.

Formalization scope

The mission uses the existing TensorObj, MMObj, TensorObj.Restrict, Degenerates, tensorAsymptoticRank, matMulExp, and matMulExp_strassen declarations in the Mathlib environment pinned by the earlier matrix-multiplication mission. Tensor dimensions and type counts are natural numbers; exponent and optimization inequalities are real-valued. All top-level bounds quantify over an arbitrary field, matching the integral polynomial identities used by the construction.

Laser statements must exhibit, directly or through a faithful reusable predicate, restrictions from a tensor power to a finite direct sum of concrete matrix-multiplication tensors. The number and dimensions of the summands remain part of the witness. A constant-valued “laser functional,” a vacuous witness hypothesis, or a capacity definition that discards the exponential number of surviving blocks does not satisfy the mission.

Welcome contributions include restriction composition lemmas, tensor-power block equivalences, multinomial and entropy estimates with all marginal constraints, formal Salem--Spencer pruning, exact real-inequality certificates, and the coupled central-block value lemma. Every milestone should cite the corresponding equation, table, or lemma in the primary paper.

Selected references

Don Coppersmith and Shmuel Winograd, Matrix Multiplication via Arithmetic Progressions, Journal of Symbolic Computation 9, 1990, pp. 251--280. ScienceDirect.
Arnold Schönhage, Partial and Total Matrix Multiplication, SIAM Journal on Computing 10(3), 1981, pp. 434--455. DOI 10.1137/0210032.
Avi Wigderson and Jeroen Zuiddam, Asymptotic Spectra: Theory, Applications and Extensions, 2023, for the tensor restriction and asymptotic-rank framework used by the Lean development. Author manuscript.

72 thms5 active usersReviewed

Completed

Combinatorics·Captain: mikedeng1

Three Partition Refinement Algorithms 2: Refining by the Smaller HalfResearch Paper

Motivation

Many equivalence problems on finite structures reduce to computing the coarsest partition of a finite set that is compatible with a relation. Deciding whether two states of a finite labelled transition system are bisimilar, testing congruence of finite-state processes in Milner's calculus of communicating systems (CCS), and minimizing a deterministic finite automaton are all instances. Kanellakis and Smolka studied the relational version in connection with CCS equivalence and gave an $O(mn)$ -time algorithm, conjecturing that $O(m \log n)$ was possible. Paige and Tarjan's 1987 paper answers that conjecture with an algorithm that has since become the standard method for bisimulation minimization in model checkers and process-algebra tools.

Timeline:

1971 — Hopcroft gives an $O(n \log n)$ algorithm for minimizing deterministic finite automata, i.e. for the coarsest partition stable with respect to one or more functions, using the rule "process the smaller half".
1983/1990 — Kanellakis and Smolka give an $O(mn)$ -time, $O(m + n)$ -space algorithm for the relational problem, and $O(c^2 n \log n)$ when every element has at most $c$ successors; they conjecture an $O(m \log n)$ algorithm.
1987 — Paige and Tarjan combine Hopcroft's smaller-half strategy with refinement by unions of blocks and obtain $O(m \log n)$ time and $O(m + n)$ space for the relational problem.

Setting

Let $U$ be a finite set with $n = |U|$ elements and let $E \subseteq U \times U$ be a binary relation on $U$ ; write $xEy$ for $(x, y) \in E$ and $m = |E|$ . For $S \subseteq U$ the preimage of $S$ is

E^{-1}(S) = \{x \in U \mid \exists y \in S,\ xEy\}.

A partition of $U$ is a family of nonempty, pairwise disjoint subsets of $U$ , its blocks, whose union is $U$ . A partition $R$ is a refinement of a partition $P$ if every block of $R$ lies inside a block of $P$ .

A set $B \subseteq U$ is stable with respect to $S \subseteq U$ if $B \subseteq E^{-1}(S)$ or $B \cap E^{-1}(S) = \emptyset$ : either every element of $B$ has an $E$ -successor in $S$ , or none does. A partition is stable with respect to $S$ if all its blocks are, and a partition is stable if it is stable with respect to each of its own blocks.

Given $E$ and an initial partition $P$ , the coarsest stable refinement of $P$ is a stable partition $Q$ refining $P$ such that every stable partition refining $P$ is a refinement of $Q$ . The relational coarsest partition problem asks for it.

The algorithms refine by the operation $\mathrm{split}(S, Q)$ , which replaces each block $B$ of $Q$ that meets both $E^{-1}(S)$ and its complement by the two blocks $B \cap E^{-1}(S)$ and $B - E^{-1}(S)$ . The set $S$ is a splitter of $Q$ if $\mathrm{split}(S, Q) \neq Q$ .

The naïve algorithm starts from $Q = P$ and, while possible, picks a splitter $S$ of $Q$ that is a union of blocks of $Q$ and replaces $Q$ by $\mathrm{split}(S, Q)$ .
The improved algorithm also maintains a partition $X$ , initially $\{U\}$ , of which $Q$ is a refinement. While $Q \neq X$ , it picks a block $S \in X$ that is not a block of $Q$ and a block $B \in Q$ with $B \subseteq S$ and $|B| \le |S|/2$ , replaces $S$ in $X$ by $B$ and $S - B$ , and replaces $Q$ by $\mathrm{split}(S - B, \mathrm{split}(B, Q))$ .

The improved algorithm is analysed under the standing assumption $|E(\{x\})| \ge 1$ for all $x \in U$ : every element has at least one successor. (The paper reduces the general case to this one by a preprocessing step.)

Formalization targets

Goal: the improved algorithm

For every run $(Q_0, X_0) = (P, \{U\}), \dots, (Q_K, X_K)$ of the improved algorithm with refining blocks $B_0, \dots, B_{K-1}$ :

at every stage $Q_j$ and $X_j$ are partitions, $Q_j$ refines $X_j$ , and $Q_j$ is stable with respect to every block of $X_j$ ;
if $Q_K = X_K$ , then $Q_K$ is the coarsest stable refinement of $P$ ;
if $Q_K \neq X_K$ , another step applies;
$K \le n - 1$ ;
every $x \in U$ satisfies

\#\{\, j < K \mid x \in B_j \,\} \le \log_2 n + 1.

Items 1–4 are the correctness of the improved algorithm, which the paper deduces from that of the naïve one. Item 5 is the counting fact on which the $O(m \log n)$ bound rests.

Milestones

§3, p. 978: $S$ is a splitter of $Q$ if and only if $Q$ is unstable with respect to $S$ .
Properties (1)–(3), p. 978: stability is inherited under refinement and under union; $\mathrm{split}$ is monotone in its second argument.
§3, p. 979: a stable partition is stable with respect to every union of its blocks.
Lemma 2, p. 979: every stable refinement of $P$ refines each partition produced by the naïve algorithm.
Theorem 2, p. 979: the naïve algorithm stops after at most $n - 1$ steps at the unique coarsest stable refinement.
Property (4), p. 978: $\mathrm{split}$ is commutative, and $\mathrm{split}(S, \mathrm{split}(Q, P))$ is the coarsest refinement of $P$ stable with respect to both $S$ and $Q$ .
Lemma 3, p. 980: the three-way split of a block $D$ into $D_{11}$ , $D_{12}$ and $D_2$ , including $D_{12} = D_1 \cap (E^{-1}(B) - E^{-1}(S - B))$ .

Significance

The coarsest stable refinement of the partition of states by their labels is the bisimilarity relation of a finite transition system, so the goal certifies, for any sequence of choices, the correctness of the refinement loop at the core of bisimulation minimization. The halving count is the combinatorial half of the $O(m \log n)$ bound: once the implementation charges $O(|B| + \sum_{y \in B} |E^{-1}(\{y\})|)$ per refining block $B$ , the count bounds the total work.

The results are proved in the paper, some by one-line arguments and the elementary properties (1)–(4) not at all ("stated without proof"). No machine-checked proof of the Paige–Tarjan algorithm's correctness or of its halving count is known to be available in Lean or Mathlib. The mission produces a checked account of the invariant, the final correctness and the counting argument for every run, not only for a particular implementation.

Difficulty

The correctness of the improved algorithm is not a special case of the naïve one read off directly. An improved step refines by $B$ and by $S - B$ , and $S - B$ is a union of blocks of $Q$ only because $Q$ refines $X$ . The invariant that $Q$ is stable with respect to every block of $X$ is what makes $Q = X$ a stopping condition, and it holds initially only under the standing assumption. The naive idea of reusing Hopcroft's argument fails: for relations, stability with respect to $S$ and $B$ does not imply stability with respect to $S - B$ , which is why both refinements are performed. For the halving count, the refining blocks that contain a fixed element must be shown to be nested across steps, which requires tracking how blocks of $X$ are replaced.

Formalization scope

$U$ is a Fintype with decidable equality, $E$ a decidable relation U → U → Prop. Partitions are Finset (Finset U) with an explicit predicate IsPartition (nonempty, pairwise disjoint blocks covering $U$ ); blocks are required to be nonempty, which the paper leaves implicit.
"Coarsest" means: every stable partition refining $P$ refines it. The paper's "every other stable partition" is read this way, since a stable partition that does not refine $P$ need not refine the answer.
Algorithms are step relations; a run is a finite sequence of states indexed by Fin (K + 1), with the choices $S_j, B_j$ recorded. Every statement holds for every run, so no choice rule is fixed.
Added hypotheses: $U$ nonempty (so $\{U\}$ is a partition and "at most $n - 1$ steps" is meaningful); the standing assumption $\forall x\, \exists y,\ xEy$ for the goal only. Lemma 2 is stated for every stable refinement of $P$ , which is what its proof gives and what Theorem 2 uses; it implies the printed form.
Explicit forms: $|B| \le |S|/2$ is 2 * B.card ≤ S.card, $K \le n - 1$ is K + 1 ≤ n, $\log_2$ is Real.logb 2 of $n$ cast to $\mathbb{R}$ . The termination bound for the improved algorithm is not printed in the paper and is derived as in the proof of Theorem 2. Running times ( $O(mn)$ , $O(m \log n)$ ) and the data structures of the implementation are out of scope.
A trivializing reading is ruled out: the goal quantifies over all runs from $(P, \{U\})$ with every side condition of the step (in particular $S \notin Q$ and the half-size condition), and the conclusion is a full correctness statement, not the existence of some stable partition; the discrete partition is stable but is not the answer in general.
Reusable beyond this mission: preimage, stability, $\mathrm{split}$ and its algebra (properties (1)–(4)), which apply to Hopcroft's algorithm and to bisimulation minimization in general. Contributions proving the elementary properties first, then Lemma 2 and Theorem 2, are the natural attack order.

Selected references

R. Paige, R. E. Tarjan, Three Partition Refinement Algorithms, SIAM Journal on Computing 16(6):973–989, 1987. https://doi.org/10.1137/0216062
P. C. Kanellakis, S. A. Smolka, CCS expressions, finite state processes, and three problems of equivalence, Information and Computation 86(1):43–68, 1990. https://doi.org/10.1016/0890-5401(90)90025-D
J. E. Hopcroft, An n log n algorithm for minimizing states in a finite automaton, in Theory of Machines and Computations, Academic Press, 1971, pp. 189–196. https://doi.org/10.1016/B978-0-12-417750-5.50022-1
A. V. Aho, J. E. Hopcroft, J. D. Ullman, The Design and Analysis of Computer Algorithms, Addison-Wesley, 1974.

12 thms4 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

Competitive Paging Algorithms I: The Marking Algorithm Is 2H_k-CompetitiveResearch Paper

Motivation

Paging is the problem of managing a two-level memory: a fast cache holds $k$ pages out of an address space of $n$ pages, requests to pages arrive one at a time, and a request to a page outside the cache (a page fault) forces the algorithm to bring that page in and, when the cache is full, to evict another. The cost is the number of faults. An on-line algorithm decides which page to evict without knowing future requests. The comparison of paging policies with the optimal off-line policy is where competitive analysis began.

Sleator and Tarjan showed that LRU and FIFO are within a factor $k$ of the off-line optimum and that no deterministic on-line algorithm does better than $k$ (Sleator–Tarjan 1985). Randomization changes the picture: Fiat, Karp, Luby, McGeoch, Sleator and Young introduced the marking algorithm and proved that its expected cost is within a factor $2H_k$ of the optimum, where $H_k = 1 + \frac12 + \dots + \frac1k \approx \ln k$ (arXiv:cs/0205038).

Timeline.

1985: Sleator and Tarjan: LRU and FIFO are $k$ -competitive; no deterministic algorithm beats $k$ .
1988: Karlin, Manasse, Rudolph and Sleator coin "competitive" and analyse flush-when-full (Algorithmica 3).
1990: Manasse, McGeoch and Sleator introduce the $k$ -server problem and define competitiveness for randomized algorithms (J. Algorithms 11).
1991: Fiat et al.: the marking algorithm is $2H_k$ -competitive, and $H_{n-1}$ -competitive when $k = n-1$ ; no randomized paging algorithm beats $H_k$ .
1991: McGeoch and Sleator give an $H_k$ -competitive randomized paging algorithm (Algorithmica 6).
2000: Achlioptas, Chrobak and Noga determine the exact competitive ratio of the marking algorithm, $2H_k - 1$ (Theoret. Comput. Sci. 234).

Setting

The paper works in the uniform $k$ -server problem, which is isomorphic to paging. There is a set $M$ of $n$ vertices, enumerated $e(0), \dots, e(n-1)$ , and moving a server between two distinct vertices costs $1$ . There are $k$ servers, $1 \le k \le n$ . A request is a vertex, and after each request some server must be on it. Cached pages are covered vertices; a fault is a server move.

The marking algorithm starts with its servers on $e(0), \dots, e(k-1)$ and keeps a set of marked vertices, initially the covered ones. On a request to $r$ :

Marking. $r$ is marked; the moment $k+1$ vertices are marked, all marks except the one on $r$ are erased.
Serving. If $r$ is covered, nothing moves. Otherwise a server is chosen uniformly at random among the covered unmarked vertices and moved to $r$ .

The marks are updated before the server is chosen. For a finite request sequence $\sigma$ , $C_M(\sigma)$ is the algorithm's expected number of server moves. $\mathrm{OPT}(\sigma)$ is the least number of moves with which $k$ servers, starting from the same configuration $C_0$ and knowing $\sigma$ in advance, can serve $\sigma$ .

A randomized algorithm is $c$ -competitive if there is a constant $a$ such that $C_M(\sigma) \le c \cdot C_B(\sigma) + a$ for every request sequence $\sigma$ and every algorithm $B$ .

The marks divide $\sigma$ into phases. A new phase begins at the request that would make $k+1$ vertices marked. A vertex is clean in a phase if it was not requested in the previous phase and not yet in this one, and stale if it was requested in the previous phase but not yet in this one.

Formalization targets

Goal: Theorem 1

\exists\, a \in \mathbb R\ \ \forall \sigma:\qquad C_M(\sigma) \;\le\; 2H_k \cdot \mathrm{OPT}(\sigma) + a .

The constant $a$ may depend on $n$ , $k$ and the enumeration, never on $\sigma$ .

Milestones (proof of Theorem 1, pp. 4–5)

Without loss of generality the adversary is lazy: no move on a covered request, exactly one move otherwise (reference item, already proved on the platform).
At the start of every phase the marked vertices are exactly the covered ones, and the first request of a phase is unmarked.
In a phase with $l$ clean requests, a lazy adversary pays $C_A \ge l - d$ , where $d$ counts its servers off the marking algorithm's servers at the start of the phase.
It also pays $C_A \ge d'$ , where $d'$ counts its servers off the final marked set at the end of the phase.
Hence $C_A \ge \max(l-d, d') \ge \tfrac12(l - d + d')$ .
A request to a stale vertex is a fault with probability $c/s$ ( $c$ clean vertices requested so far, $s$ stale vertices left).
The marking algorithm's expected cost in a phase is at most $l(H_k - H_l + 1) \le lH_k$ .

Companions

Theorem 2: for $k = n-1$ , $C_M(\sigma) \le H_{n-1} \cdot \mathrm{OPT}(\sigma) + a$ .
Tightness remark (pp. 5–6): for $k = 2$ , $n = 4$ there is no $a$ with $C_M(\sigma) \le H_2 \cdot \mathrm{OPT}(\sigma) + a$ for all $\sigma$ .

Significance

The result. Theorem 1 was the first proof that randomization beats the deterministic barrier $k$ for paging, bringing the ratio down to $O(\log k)$ . Together with the paper's lower bound $H_k$ for every randomized algorithm, it determines the randomized competitive ratio of paging up to a factor $2$ . Its phase and clean/stale accounting is reused throughout the analysis of randomized caching.

Formalizing it. The theorem is proved (1991). As far as is known it has no machine-checked proof. Formalizing it requires a probabilistic model of a randomized on-line algorithm, an off-line optimum, and a phase decomposition with an exchangeability argument, and these are the first such objects in this library. Theorem 2 and the $k = 2$ , $n = 4$ example use the same definitions and also check that the formal algorithm is the paper's. The sharp ratio $2H_k - 1$ is a natural follow-up.

Difficulty

The comparison is between a random process and a deterministic adversary, and each side has its own obstacle.

On the algorithm's side, the configuration inside a phase is random, and the fault probability of a stale request depends on the whole history of the phase. The claim that the $c$ uncovered stale vertices form a uniformly random subset of the $s$ stale ones is an exchangeability property of the process, and must be established from the step-by-step uniform choice. The worst-case ordering of the requests within a phase then has to be justified as a bound, not assumed.

On the adversary's side, the per-phase bound $\max(l-d, d')$ does not sum directly. The $d$ and $d'$ terms telescope across phases only because the configuration of the marking algorithm at each phase boundary is deterministic. The first phase, which begins after an initial run of requests to $e(0), \dots, e(k-1)$ , and the last, incomplete phase have to be absorbed into the additive constant.

Formalization scope

The vertex set is an abstract metric space $M$ with $e : \mathrm{Fin}\,n \simeq M$ and $\mathrm{dist}(x,y) = 1$ for $x \ne y$ . The natural metric $|i - j|$ on $\mathrm{Fin}\,n$ is deliberately not used. The configurations and the off-line optimum $\mathrm{OPT}$ are the published KServer definitions (KServer.Config, KServer.offlineCost), with $\mathrm{OPT}$ taken from the marking algorithm's initial configuration. An off-line algorithm starting elsewhere changes the cost by at most $k$ , which is absorbed into $a$ .

The marking algorithm is a Markov chain on pairs (covered set, marked set). Each step is a PMF, with the eviction drawn by PMF.uniformOfFinset from the covered unmarked vertices. The expected cost is the sum over requests of the probability that the request is not covered, which is exact because the algorithm moves exactly one server per fault. Harmonic numbers are Mathlib's harmonic, cast to $\mathbb R$ . Phases, clean counts and lazy off-line schedules are defined once, in the mission's definition file, and all milestones use them.

A trivializing formalization is ruled out as follows. The additive constant is quantified before $\sigma$ , so a per-sequence constant cannot be used. The comparison is with the optimum over all off-line schedules, not a particular one. The random choice is among the covered unmarked vertices, with marks updated first. The hypothesis $1 \le k \le n$ excludes the degenerate case $k = 0$ , where $H_0 = 0$ .

Proofs of individual milestones are welcome. The laziness reduction for off-line schedules, the exchangeability lemma for the uniform eviction process, and the harmonic-sum identity $\sum_{j=l+1}^{k} l/j = l(H_k - H_l)$ are reusable beyond this mission.

Selected references

A. Fiat, R. M. Karp, M. Luby, L. A. McGeoch, D. D. Sleator, N. E. Young, Competitive Paging Algorithms, J. Algorithms 12(4):685–699, 1991; arXiv:cs/0205038v1. https://arxiv.org/abs/cs/0205038
D. D. Sleator, R. E. Tarjan, Amortized Efficiency of List Update and Paging Rules, Comm. ACM 28(2):202–208, 1985. https://doi.org/10.1145/2786.2793
A. R. Karlin, M. S. Manasse, L. Rudolph, D. D. Sleator, Competitive Snoopy Caching, Algorithmica 3:79–119, 1988. https://doi.org/10.1007/BF01762111
M. S. Manasse, L. A. McGeoch, D. D. Sleator, Competitive Algorithms for Server Problems, J. Algorithms 11(2):208–230, 1990. https://doi.org/10.1016/0196-6774(90)90003-W
L. A. McGeoch, D. D. Sleator, A Strongly Competitive Randomized Paging Algorithm, Algorithmica 6:816–825, 1991. https://doi.org/10.1007/BF01759073
D. Achlioptas, M. Chrobak, J. Noga, Competitive Analysis of Randomized Paging Algorithms, Theoret. Comput. Sci. 234:203–218, 2000. https://doi.org/10.1016/S0304-3975(98)00116-9

10 thms4 active usersReviewed

Completed

Combinatorics Graph Theory Operations Research+1·Captain: mikedeng1

An Analysis of Several Heuristics for the Traveling Salesman Problem I: Nearest Neighbor Tours Can Be Far from OptimalResearch Paper

Motivation

The traveling salesman problem with the triangle inequality asks for a shortest closed tour through $n$ points whose distances form a metric. It is NP-hard, so in practice tours are built by fast construction heuristics, and the natural question is how far such a tour can be from optimal in the worst case. Rosenkrantz, Stearns and Lewis (SIAM J. Comput. 6(3), 1977) gave the first systematic worst-case analysis of the standard heuristics. Their results are reproduced in textbooks on approximation algorithms and combinatorial optimization, and they are the reference point against which later guarantees (Christofides' $3/2$ algorithm, the double-tree $2$ -approximation) are compared.

The simplest heuristic studied is the nearest neighbor algorithm (Bellmore and Nemhauser, 1968; the "next best method" of Gavett, 1965): from the current node, always move to the closest node not yet visited, and return to the start at the end. The paper shows that this greedy rule is never worse than logarithmic (Theorem 1) and that the logarithm cannot be removed (Theorem 2). This mission is about Theorem 2, the lower bound.

Setting

A traveling salesman graph on $n$ nodes is a complete graph with a distance $d(a,b)\in\mathbb R$ that is symmetric, $d(a,b)=d(b,a)$ , nonnegative, $d(a,b)\ge 0$ , and satisfies the triangle inequality $d(a,c)\le d(a,b)+d(b,c)$ . A tour lists the nodes in a visiting order $\tau(0),\dots,\tau(n-1)$ and returns to $\tau(0)$ ; its length is the sum of the $n$ distances along it. OPTIMAL is the least length of a tour.

The nearest neighbor algorithm starts at an arbitrary node $\tau(0)$ ; having reached $\tau(k)$ , it moves to a node $\tau(k+1)$ that minimizes $d(\tau(k),\cdot)$ over the nodes not yet visited, breaking ties arbitrarily; after the last node it returns to $\tau(0)$ . The length of the resulting tour is written NEARNEIBER. Because the start node and the ties are free, one instance has in general several nearest-neighbor tours. A lower bound needs only one of them; an upper bound must hold for all.

The instances of the proof are built from a recursive family of weighted graphs. With $l_i=\frac16(4\cdot 2^i-(-1)^i+3)$ (so $l_1,l_2,l_3,l_4=2,3,6,11$ ), the graph $F_1$ is a triangle with unit weights, and $F_{i+1}$ consists of two copies of $F_i$ joined through one new node by two edges of length $1$ and two edges of length $l_i$ . Each $F_i$ has $2^{i+1}-1$ nodes and a path $P_i$ from its start node to its middle node through every node, of length $L_i$ with $L_1=2$ , $L_{i+1}=2L_i+2l_i$ . The graph $G_i$ adds two closing edges to $F_i$ , and $\bar G_i$ is the complete graph on the same nodes whose distance is the shortest-path distance of $G_i$ .

Formalization targets

Goal: Theorem 2 (p. 566)

For each $m>3$ there is a traveling salesman graph with $n=2^m-1$ nodes and a nearest-neighbor tour on it such that

\frac{\mathrm{NEARNEIBER}}{\mathrm{OPTIMAL}}>\frac13\lg(n+1)+\frac49 .

The statement is existential in both the instance and the run of the algorithm, exactly as in the paper.

Milestones, in the order the proof uses them

(2.12): the difference equation $L_{i+1}=2L_i+2l_i$ , $L_1=2$ , has the solution $L_i=\frac19(6\,i\,2^i+8\cdot2^i+(-1)^i-9)$ .
$\bar G_i$ is a traveling salesman graph: the shortest-path distance of $G_i$ is symmetric, nonnegative and satisfies the triangle inequality.
(2.13)–(2.17): the shortest-path distances in $F_{i+1}$ between the seven named nodes $A,\dots,G$ of Fig. 1, e.g. $\overline{AG}=l_{i+2}-2$ .
Property a): every edge of $G_i$ is a shortest path between its endpoints.
Property b): the nearest neighbor algorithm started at the start node of $\bar G_i$ can follow $P_i$ and return along the edge of length $l_i-1$ .
The optimal tour: $\mathrm{OPTIMAL}(\bar G_i)=2^{i+1}-1$ .
The exact ratio: the tour along $P_i$ has length $L_i+l_i-1$ , so its ratio is $(L_i+l_i-1)/n$ .
The inequality: $(L_i+l_i-1)/n>\frac13\lg(n+1)+\frac49$ for $i\ge3$ .

The instance for $m$ is $\bar G_{m-1}$ .

Significance

Theorem 1 of the same paper shows $\mathrm{NEARNEIBER}/\mathrm{OPTIMAL}\le\frac12\lceil\lg n\rceil+\frac12$ for every nearest-neighbor tour on every traveling salesman graph. Theorem 2 shows that this bound has the right order: no constant-factor guarantee holds for the nearest neighbor rule, and the gap between the two constants ( $\frac13$ against $\frac12$ ) is all that remains. This separates the nearest neighbor rule from the insertion rules analysed later in the same paper, of which nearest and cheapest insertion are within a factor $2$ of optimal. It is the standard example of a natural greedy heuristic whose approximation ratio grows with $n$ .

The upper bound, Theorem 1, is already on Prove2Me with a machine-checked proof (SupplyChainTheory.nearest_neighbor_bound); its statement notes that the lower-bound instances are not formalized there. This mission supplies them: an explicit recursive family of metric instances, the shortest-path computations that certify it, and the arithmetic of its ratio. The result is proved in the paper; to our knowledge it has not been formalized in any proof assistant. The construction (a recursively defined weighted graph with a closed-form shortest-path table) is also a reusable pattern for other worst-case lower bounds of greedy heuristics.

Difficulty

The arithmetic ((2.12) and the final inequality) is routine. The content is in properties a) and b). A shortest-path distance is an infimum over all walks, and property a) asks that no detour through the recursive structure is shorter than the direct edge, at every level of the recursion. The paper handles this by an induction on (2.13)–(2.17) that tracks only seven nodes per level, and argues that distances inside a copy of $F_i$ are not shortened by embedding it into $F_{i+1}$ . Property b) then needs that at each step of $P_i$ the chosen node is at least as close as every unvisited node, including nodes in the other copy and nodes reached through the start or right nodes; ties occur, and the claim is only that some resolution of them follows $P_i$ . Checking small cases by computer does not give either property for all $i$ .

Formalization scope

Nodes of an instance are Fin n, a tour is a permutation of Fin n, the tour length is the sum over consecutive pairs including the closing edge, and OPTIMAL is a minimum over the finite set of permutations. The model is the paper's: symmetric, nonnegative distances with the triangle inequality. The distance structure also carries $d(a,a)=0$ , a normalization not in the paper; the diagonal never enters a tour length. A nearest-neighbor tour is a permutation in which each step goes to a node at least as close as every unvisited node, from an arbitrary start with arbitrary ties.

Ratios are multiplied out: the goal is $(\frac13\log_2(n+1)+\frac49)\cdot\mathrm{OPTIMAL}<\mathrm{NEARNEIBER}$ together with $\mathrm{OPTIMAL}>0$ , the paper's standing assumption (1.1). $\lg(n+1)$ is Real.logb 2 of $n+1$ , as printed. Because of the strict inequality and the conjunct $\mathrm{OPTIMAL}>0$ , the all-zero distance does not satisfy the goal, so the statement cannot be met by a degenerate instance.

In the construction the nodes of $F_i$ , $G_i$ , $\bar G_i$ are numbered $0,\dots,2^{i+1}-2$ from left to right (start node $0$ , middle node $2^i-1$ , right node $2^{i+1}-2$ ); in $F_{i+1}$ the left copy comes first, then the new node, then the right copy. Graphs are edge lists with real weights and $l_i$ is defined in $\mathbb R$ exactly as in (2.11). The shortest-path distance is the infimum of walk weights over an inductive walk predicate; it would be $0$ for two nodes with no connecting walk, a case that does not arise because every $G_i$ and $F_i$ is connected. $L_i$ is defined by its difference equation; its identification with the length of the tour along $P_i$ is milestone 7. All construction statements assume $i\ge1$ .

A complete development needs a small library for shortest-path distances of finite weighted edge lists (symmetry, triangle inequality, attainment, behaviour under relabelling and under gluing two graphs at a few nodes); this part is reusable beyond the mission. Contributions welcome: proofs of any milestone, and such general shortest-path lemmas as separate theorems. Theorem 1 is not part of this mission.

Selected references

D. J. Rosenkrantz, R. E. Stearns, P. M. Lewis II, An Analysis of Several Heuristics for the Traveling Salesman Problem, SIAM J. Comput. 6(3):563–581, 1977. https://doi.org/10.1137/0206041
M. Bellmore, G. L. Nemhauser, The Traveling Salesman Problem: A Survey, Operations Research 16(3):538–558, 1968. https://doi.org/10.1287/opre.16.3.538
J. W. Gavett, Three Heuristic Rules for Sequencing Jobs to a Single Production Facility, Management Science 11(8):B166–B176, 1965. https://doi.org/10.1287/mnsc.11.8.B166
N. Christofides, Worst-Case Analysis of a New Heuristic for the Travelling Salesman Problem, Report 388, Graduate School of Industrial Administration, Carnegie Mellon University, 1976.

12 thms4 active usersReviewed

Completed

Combinatorics Operations Research Optimization·Captain: mikedeng1

Worst-Case Performance Bounds for Simple One-Dimensional Packing Algorithms 2: First-Fit and Best-Fit with Bounded Item SizesResearch Paper

Motivation

Bin packing asks for the fewest unit-capacity bins that hold a given list of item sizes. It models cutting stock, memory allocation, file placement and the loading of trucks, and it is NP-hard, so in practice lists are packed by simple rules that look at one item at a time. The two most widely used rules are First-Fit and Best-Fit, and the question that Johnson, Demers, Ullman, Garey and Graham answered in 1974 is how far from optimal they can be in the worst case.

Their headline answer is that both rules use at most about $\tfrac{17}{10}$ times the optimal number of bins, and that $\tfrac{17}{10}$ is asymptotically attained. The lists that force this ratio use items larger than $\tfrac12$ . When all items are known to be small, which is typical of memory and storage applications, the guarantee is much better, and this mission is about that refinement: the paper's Theorem 2.3 and its corollary, which determine the asymptotic worst-case ratio of First-Fit and Best-Fit exactly as a function of the largest allowed item size $\alpha\le\tfrac12$ .

Timeline. Ullman (1971) introduced the worst-case analysis of First-Fit with a $\tfrac{17}{10}L^*+3$ bound. Garey, Graham and Ullman (1972) and Johnson's thesis (MIT, 1973) extended it to Best-Fit and to the decreasing variants. The 1974 SIAM paper collects these results; Theorem 2.3 there is the parametric bound for items of size at most $\alpha$ . The additive constants in the unrestricted $\tfrac{17}{10}$ bound were sharpened over the following four decades, culminating in Dósa and Sgall's proof (2013) that $FF(L)\le\lfloor\tfrac{17}{10}L^*\rfloor$ .

Setting

A list is a finite sequence $L=(a_1,\dots,a_n)$ of real numbers in $(0,1]$ . Its optimum $L^*$ is the least number of bins into which the elements of $L$ can be placed so that no bin contains numbers whose sum exceeds $1$ . The level of a bin is the sum of the numbers in it. For a real $\alpha>0$ , write $L\subseteq(0,\alpha]$ when every element of $L$ is at most $\alpha$ .

First-Fit ( $FF$ ) considers bins $B_1,B_2,\dots$ , all initially empty, and places $a_1,a_2,\dots,a_n$ in that order: $a_i$ goes into the bin $B_j$ of least index whose level $\beta$ satisfies $\beta\le 1-a_i$ . Best-Fit ( $BF$ ) is the same except that, among the bins with $\beta\le 1-a_i$ , it chooses one of largest level $\beta$ (least index among ties). $FF(L)$ and $BF(L)$ denote the numbers of nonempty bins at the end.

The restricted worst-case ratios are

R^\alpha_{FF}(k)=\max\Big\{\frac{FF(L)}{L^*}: L\subseteq(0,\alpha],\ L^*=k\Big\},\qquad R^\alpha_{BF}(k)=\max\Big\{\frac{BF(L)}{L^*}: L\subseteq(0,\alpha],\ L^*=k\Big\}.

Throughout, $0<\alpha\le\tfrac12$ and $m=\lfloor\alpha^{-1}\rfloor$ , an integer with $m\ge 2$ and $\tfrac1{m+1}<\alpha\le\tfrac1m$ .

Formalization targets

Goal: the asymptotic ratio (Corollary of Theorem 2.3, p. 308)

\lim_{k\to\infty}R^\alpha_{FF}(k)=\lim_{k\to\infty}R^\alpha_{BF}(k)=1+\frac{1}{\lfloor\alpha^{-1}\rfloor}.

The goal is stated as a limit, which is the stable form of the result: it is unaffected by any improvement of the additive constants below.

Theorem 2.3(i): the lower bound (p. 307)

For each $k\ge1$ there is a list $L\subseteq(0,\alpha]$ with $L^*=k$ and $FF(L)\ge\frac{m+1}{m}L^*-\frac1m$ ; likewise for $BF$ .

Two steps of the First-Fit upper bound (p. 308)

If no element of $L$ exceeds $\frac1m$ , then in the First-Fit packing every bin except possibly the last contains at least $m$ elements, and all but at most two bins have level at least $\frac{m}{m+1}$ .

Theorem 2.3(ii): the upper bounds (p. 307)

For every list $L\subseteq(0,\alpha]$ ,

FF(L)\le\frac{m+1}{m}L^*+2,\qquad BF(L)\le\frac{m+1}{m}L^*+2.

Significance

The theorem gives an exact, parametric description of how the worst case of the two greedy rules improves as items shrink: the asymptotic ratio is $\tfrac32$ when items are at most $\tfrac12$ , $\tfrac43$ when at most $\tfrac13$ , and tends to $1$ as the maximum item size tends to $0$ . Combined with the $\tfrac{17}{10}$ bound for unrestricted lists, it shows that the bad behaviour of First-Fit is caused entirely by items larger than $\tfrac12$ . Such parametric bounds are the standard way bin-packing heuristics are compared in the literature on online and semi-online packing, and the construction in part (i) is a reusable template for lower-bound lists.

The paper proves the First-Fit upper bound and the lower bound (the verification of the lower-bound construction is left to the reader). The Best-Fit upper bound is stated but not proved: the paper says only that "a similar, but slightly more complicated, argument can be used". A formal proof of the goal therefore requires supplying that argument. None of these results is known to have a machine-checked proof; Mathlib contains no bin-packing development.

Difficulty

For First-Fit the upper bound is a counting argument, but it rests on a property of the run, not of the final packing: an item that went into a later bin did not fit into an earlier bin at the moment it was placed. Turning that into a statement about the final levels requires an invariant maintained through the whole sequence of placements.

The Best-Fit upper bound is harder because that property fails: Best-Fit may put a small item into a fuller, later bin while an earlier, lighter bin still has room, so a light early bin and a light later bin can coexist longer than under First-Fit. The paper gives no argument for this case.

The lower bound requires computing the exact behaviour of both algorithms on a specific interleaved list with item sizes perturbed by powers of $m$ , and computing $L^*$ exactly for that list, which needs a matching lower bound on the optimum.

Formalization scope

A list is L : List ℝ with the hypothesis IsList L (every element in $(0,1]$ ); $L\subseteq(0,\alpha]$ is the additional hypothesis ∀ a ∈ L, a ≤ α. $L^*$ is optBins L, a sInf in ℕ over numbers of bins admitting a feasible assignment; the hypothesis IsList makes the set nonempty. The runs ffPack L and bfPack L are folds over the list that keep the nonempty bins in the order they were opened, each with its contents; an item that fits nowhere opens a new bin at the end, which is the paper's "least $j$ " over infinitely many empty bins. Comparisons are exact (classical decidability on ℝ), and $FF(L)$ , $BF(L)$ are the lengths of the final bin lists. $m$ is Nat.floor α⁻¹, cast before any division.

The ratios $R^\alpha_{FF}(k)$ , $R^\alpha_{BF}(k)$ are suprema taken in ℝ≥0∞: an unbounded family would give $+\infty$ , never a default value, and at $k=0$ the only admissible list is empty and the value is $0$ . The goal is a Tendsto … atTop (𝓝 (1 + (⌊α⁻¹⌋₊)⁻¹)) statement in ℝ≥0∞. A real-valued sSup would have returned $0$ on an unbounded family and made a false bound look provable; that encoding is ruled out. The upper bounds keep the additive constant $2$ and the lower bound the subtractive $\frac1m$ exactly as printed.

The two proof steps are stated under the proof's own hypothesis "no element exceeding $1/m$ ", which is weaker than $L\subseteq(0,\alpha]$ .

A complete development needs invariants of the First-Fit and Best-Fit folds, a lower bound $L^*\ge\sum_i a_i$ , and exact evaluation of both runs on the construction of part (i). Lemmas about the fold encoding of First-Fit and Best-Fit and about $L^*$ are reusable in the companion missions on the $\tfrac{17}{10}$ , $\tfrac{11}{9}$ and $\tfrac{71}{60}$ bounds of the same paper. Contributions on the Best-Fit upper bound are especially welcome, since the source gives no proof.

Selected references

D. S. Johnson, A. Demers, J. D. Ullman, M. R. Garey, R. L. Graham, Worst-Case Performance Bounds for Simple One-Dimensional Packing Algorithms, SIAM Journal on Computing 3(4):299–325, 1974. https://doi.org/10.1137/0203025
J. D. Ullman, The Performance of a Memory Allocation Algorithm, Technical Report 100, Princeton University, 1971.
M. R. Garey, R. L. Graham, J. D. Ullman, Worst-Case Analysis of Memory Allocation Algorithms, Proc. 4th ACM Symposium on Theory of Computing, 143–150, 1972. https://doi.org/10.1145/800152.804907
D. S. Johnson, Near-Optimal Bin Packing Algorithms, PhD thesis, Massachusetts Institute of Technology, 1973. http://hdl.handle.net/1721.1/57819
G. Dósa, J. Sgall, First Fit Bin Packing: A Tight Analysis, Proc. 30th STACS, LIPIcs 20:538–549, 2013. https://doi.org/10.4230/LIPIcs.STACS.2013.538

7 thms4 active usersReviewed

Completed

Combinatorics Operations Research Optimization·Captain: mikedeng1

Local Search Heuristics for k-Median and Facility Location Problems III: Add-Drop-Swap Local Search for Uncapacitated Facility Location Has Locality Gap 3Research Paper

Motivation

The uncapacitated facility location (UFL) problem is one of the basic models of location theory and operations research: a firm chooses which warehouses, plants or servers to open, paying a fixed cost for each open site and a service cost for every client according to its distance to the nearest open site. It is also a standard test case for approximation algorithms.

Local search is the simplest of these and the one most used in practice: start from any set of open facilities and repeatedly add, drop or exchange one facility while this lowers the cost. The question is how bad a solution can be when no such move helps. Arya, Garg, Khandekar, Meyerson, Munagala and Pandit (SIAM J. Comput. 33(3), 2004) answered it for UFL with an exact constant.

Timeline. Korupolu, Plaxton and Rajaraman (SODA 1998, J. Algorithms 2000) analysed local search with add, drop and swap moves and proved a locality gap of at most 5; their analysis contains the service cost bound restated here as Lemma 4.1. Charikar and Guha (FOCS 1999) proved a locality gap of 3 for a different local search, in which one facility is added and any number are dropped. Arya et al. (STOC 2001; journal version 2004) proved that the add/drop/swap neighbourhood itself has locality gap at most 3, and gave an instance showing that 3 cannot be improved (§4.3).

Setting

A metric instance consists of a finite set $C$ of clients, a finite set $F$ of facilities, and a distance $d$ on $C \cup F$ that is nonnegative, symmetric and satisfies the triangle inequality. The cost of serving client $j$ by facility $i$ is $c_{ji} = d(j,i)$ ; the distance $c_{ii'}$ between two facilities is also available. Each facility $i \in F$ has an opening cost $f_i \ge 0$ .

A solution is a nonempty set $S \subseteq F$ of open facilities. Every client is served by its nearest open facility, so

\mathrm{cost}_f(S) = \sum_{i \in S} f_i, \qquad \mathrm{cost}_s(S) = \sum_{j \in C} \min_{i \in S} c_{ji}, \qquad \mathrm{cost}(S) = \mathrm{cost}_f(S) + \mathrm{cost}_s(S).

The neighbourhood of $S$ is the set of solutions reachable by adding one facility, dropping one facility, or swapping one open facility for another:

\mathcal B(S) = \{S + \{s'\}\} \cup \{S - \{s\} \mid s \in S\} \cup \{S - \{s\} + \{s'\} \mid s \in S\}.

$S$ is locally optimum if $\mathrm{cost}(S) \le \mathrm{cost}(S')$ for every $S' \in \mathcal B(S)$ . The locality gap is the supremum, over all instances, of the ratio between the cost of a worst local optimum and the cost of a global optimum.

The proofs use the following notation, which appears in the milestones but not in the goal. Fix a second solution $O$ and nearest-facility assignments $\sigma_S : C \to S$ , $\sigma_O : C \to O$ ; write $S_j = c_{j\sigma_S(j)}$ , $O_j = c_{j\sigma_O(j)}$ , $N_S(s) = \sigma_S^{-1}(s)$ , $N_O(o) = \sigma_O^{-1}(o)$ and $N^o_s = N_O(o) \cap N_S(s)$ . A facility $s \in S$ captures $o \in O$ if $|N^o_s| > \tfrac12 |N_O(o)|$ ; $s$ is good if it captures no facility of $O$ and bad otherwise. The proof of the facility cost bound uses a permutation $\pi$ of the clients that maps each $N_O(o)$ onto itself, moves every client of a non-capturing block $N^o_s$ out of that block (Property 3.1), and fixes every client of a capturing block that it would map into the same block.

Formalization targets

Goal: Theorem 4.3

\mathrm{cost}(S) \le 3 \cdot \mathrm{cost}(O) \quad \text{for every locally optimum } S \text{ and every solution } O.

This is the locality gap bound of Theorem 4.3 (p. 557) in its strongest printed form: $O$ is any solution, not only an optimal one.

Milestones

Lemma 4.1 (service cost), p. 554: $\mathrm{cost}_s(S) \le \mathrm{cost}_f(O) + \mathrm{cost}_s(O)$ .
The refined mapping $\pi$ of the proof of Lemma 4.2, p. 555: such a permutation exists for any two assignments.
Inequality (5), p. 555: the drop move for a good facility $s$ ,

-f_s + \sum_{j \in N_S(s),\ \pi(j) \neq j} (O_j + O_{\pi(j)} + S_{\pi(j)} - S_j) + 2 \sum_{j \in N_S(s),\ \pi(j) = j} O_j \ge 0.

Inequality (6), pp. 555–556: the swap of a bad facility $s$ with the facility $o$ it captures that is nearest to it.
Inequality (8), p. 556: for a bad facility $s$ capturing the set $P \subseteq O$ , the analogue of (5) with $\sum_{o' \in P} f_{o'} - f_s$ in place of $-f_s$ .
Lemma 4.2 (facility cost), p. 555: $\mathrm{cost}_f(S) \le \mathrm{cost}_f(O) + 2 \cdot \mathrm{cost}_s(O)$ .

A companion item, not a milestone, states the bound in the proof of Theorem 4.4 with $\alpha = \sqrt2$ : a local optimum of the instance with facility costs $\sqrt2 f_i$ costs at most $(1+\sqrt2)\,\mathrm{cost}(O)$ in the original instance.

Significance

The result. Theorem 4.3 shows that the simplest local search for metric UFL is within a factor 3 of optimal at every local optimum, with no LP and no rounding, and the tight example of §4.3 shows the analysis cannot be improved for this neighbourhood. Because Lemmas 4.1 and 4.2 hold against every solution $O$ , scaling the facility costs before running local search trades the two bounds against each other and gives the $1 + \sqrt2 + \epsilon$ guarantee of Theorem 4.4. The same capture-and-reassign technique is used for k-median (§3) and capacitated facility location (§5).

Formalizing it. The theorem is proved on paper; no machine-checked proof of it or of any locality gap bound for facility location is known to this mission. A formal development would check the reassignment arguments, which are stated case by case in the paper, and would produce reusable Lean infrastructure for metric facility location instances, nearest-facility costs and neighbourhood-based local optimality.

Difficulty

The service cost bound is routine; the facility cost bound is where the work lies. The natural first idea, closing a facility $s \in S$ and sending each of its clients to the facility of $S$ nearest to that client's optimal facility, fails when $s$ serves most of the clients of some $o \in O$ : the nearest facility of $S$ to $o$ may be $s$ itself, so the client has nowhere to go. The proof separates good facilities, which can be dropped, from bad ones, which must be swapped with a captured facility, and pays for the clients that cannot be moved through the distance between $s$ and its nearest captured facility. The combinatorial core is the construction of a permutation within each $N_O(o)$ that avoids every non-capturing block and has fixed points only where they are unavoidable.

Formalization scope

Clients and facilities are finite types Cl and Fa. The distance is a real-valued function on Cl ⊕ Fa that is nonnegative, symmetric and satisfies the triangle inequality; $d(x,x) = 0$ is not assumed, since the paper neither states nor uses it. Opening costs are a function f : Fa → ℝ with 0 ≤ f i, and demands are unit, as in the paper.

Solutions are nonempty Finsets. The service cost is $\sum_j \min_{i \in S} c_{ji}$ (Finset.inf') and is defined only for nonempty sets, so no junk value for $\emptyset$ enters. Accordingly the drop move is considered only when a facility remains open; with at least one client, $\emptyset$ cannot serve anyone and is not a solution. Local optimality is required for all moves of $\mathcal B(S)$ : every added facility, every dropped facility and every swap, not only the moves used in the proof. The goal is stated as the multiplied-out inequality $\mathrm{cost}(S) \le 3\,\mathrm{cost}(O)$ for every nonempty $O$ , never as a ratio, since $\mathrm{cost}(O)$ may be $0$ .

In the milestones, the nearest-facility assignments $\sigma_S$ , $\sigma_O$ are arbitrary among the nearest ones (ties broken arbitrarily), and the family of bijections $\pi : N_O(o) \to N_O(o)$ is a single permutation of the clients with $\sigma_O \circ \pi = \sigma_O$ . Inequality (5) assumes at least one client, which the paper assumes implicitly: with no clients and $S = \{s\}$ it would read $-f_s \ge 0$ . The goal and Lemma 4.2 need no such assumption.

A statement that assumes local optimality only for the moves the proof uses, that fixes $O$ to be a global optimum defined by hypotheses, or that allows the empty set a zero service cost would be a different theorem; none of these is used.

Needed infrastructure: sums over nearest-facility assignments and their fibers $N_O(o)$ , the permutation $\pi$ , and bookkeeping of the three kinds of moves. The instance, cost and local optimality definitions are reusable for other local search analyses of metric location problems. Proofs of any milestone are welcome, as are alternative proofs of the goal.

Selected references

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(3):544–562, 2004. https://doi.org/10.1137/S0097539702416402
M. R. Korupolu, C. G. Plaxton, R. Rajaraman, Analysis of a Local Search Heuristic for Facility Location Problems, J. Algorithms 37(1):146–188, 2000. https://doi.org/10.1006/jagm.2000.1100
M. Charikar, S. Guha, Improved Combinatorial Algorithms for the Facility Location and k-Median Problems, FOCS 1999, 378–388. https://doi.org/10.1109/SFFCS.1999.814609

10 thms4 active usersReviewed

Completed

Linear Optimization Optimization·Captain: moutei

Primal-Dual Online Algorithms II: Finite LP Duality and Complementary SlacknessTextbook

Motivation

Almost every competitive online algorithm built by the primal-dual method rests on the same two facts about a pair of linear programs. The first is weak duality: any feasible solution of the dual is a lower bound on any feasible solution of the primal. The second is complementary slackness: if a feasible primal-dual pair satisfies a local, per-coordinate tightness condition, the pair is optimal — and if it satisfies that condition only up to factors $\alpha$ and $\beta$ , the primal is within $\alpha\beta$ of optimal.

The second fact in its approximate form is the engine of the whole method. An online algorithm cannot compute an optimum; what it can do is maintain a primal solution and a dual solution side by side so that each new request preserves an approximate tightness invariant. The approximate complementary slackness theorem then converts that local invariant into a global competitive ratio, with no reference to the optimum at all. Chapter 2 of Buchbinder's thesis states it as the background result on which the rest of the work is built.

Setting

Fix finite index types $I$ (primal variables) and $J$ (primal constraints), a matrix $A : I \times J \to \mathbb{R}$ , a cost vector $c : I \to \mathbb{R}$ and a right-hand side $b : J \to \mathbb{R}$ . The covering primal and packing dual are

(P)\quad \min \sum_{i} c_i x_i \ \text{ s.t. } \ \sum_{i} A_{ij} x_i \ \ge\ b_j \ \ (\forall j), \qquad x \ge 0,

(D)\quad \max \sum_{j} b_j y_j \ \text{ s.t. } \ \sum_{j} A_{ij} y_j \ \le\ c_i \ \ (\forall i), \qquad y \ge 0.

Note the index convention: $A_{ij}$ carries the primal-variable index first, so the primal constraint indexed by $j$ sums over $i$ and the dual constraint indexed by $i$ sums over $j$ .

Given $\alpha, \beta \ge 1$ , the pair $(x,y)$ satisfies approximate complementary slackness when

primal side: for every $i$ with $x_i > 0$ , $\quad c_i/\alpha \ \le\ \sum_j A_{ij} y_j \ \le\ c_i$ ;
dual side: for every $j$ with $y_j > 0$ , $\quad b_j \ \le\ \sum_i A_{ij} x_i \ \le\ \beta\, b_j$ .

Formalization targets

Goal — approximate complementary slackness

For a primal-feasible $x$ , a dual-feasible $y$ , and $\alpha,\beta \ge 1$ satisfying the two conditions above,

\sum_{i} c_i x_i \ \le\ \alpha\beta \sum_{j} b_j y_j .

Taking $\alpha = \beta = 1$ recovers exact complementary slackness and hence optimality of both members of the pair. The goal is stated with the source's hypotheses, including the two-sided bounds, rather than the weakest hypotheses that make the inequality go through; a separate item records the minimal-hypothesis strengthening.

Weak duality

\sum_j b_j y_j \ \le\ \sum_i c_i x_i \quad \text{for every feasible } x \text{ and } y,

with no nonnegativity assumption on $A$ , $b$ or $c$ beyond feasibility itself.

Strong duality — imported, not reproved

Strong duality is not proved in this mission. The platform already carries LinearOptimization.lp_strong_duality, proved in this exact environment, for linear programs in Bertsimas–Tsitsiklis general form over Fin-indexed data. This mission's contribution is an adapter: from a primal optimum of $(P)$ , produce a dual optimum of $(D)$ of equal value, for Fin-indexed instances. Reference items point at the imported theorem, its dual construction, and the dual-of-dual identity.

The biconditional — a dual optimum exists if and only if a primal optimum does — is deliberately left open. Weak duality does not derive the existence of a primal optimum from the existence of a dual one; the reverse implication needs strong duality applied to the dual program together with the dual-of-dual identity, and that reduction is not yet compiled. It is offered as a parallel target rather than claimed as established.

Significance

This mission is the foundation of the series. Every later mission — set cover, ski rental, and the online covering and packing problems that follow — states its approximation or competitiveness result as an instance of approximate complementary slackness. Formalizing it once, over arbitrary finite index types, is what makes the later missions short.

It also fills a real gap. Mathlib currently has no linear-programming duality: four separate attempts were closed unmerged. Approximate $(\alpha,\beta)$ complementary slackness appears not to be formalized in any public library, so the goal theorem is, as far as we can determine, first of its kind.

Difficulty

The goal is a summation argument, not a deep theorem: the work is in handling the per-coordinate case split on $x_i > 0$ versus $x_i = 0$ and in interchanging a double sum. Three mechanical milestones isolate exactly those steps. The strong-duality adapter is the hard item, because it must reconcile two different presentations of the same program — index types, matrix orientation, and bundling all differ between our definitions and the imported theorem's.

Formalization scope

Definitions cover §2.1 of the source. Four distinct notions of "the program has a finite optimum" are separated on purpose — attained optimum, nonempty feasible set, bounded objective, and the conjunction — because the source's informal word "bounded" conflates them. The definitions are stated over arbitrary finite index types; the strong-duality items are stated only for Fin, because that is the only index type for which the imported dependency path exists.

Selected references

Niv Buchbinder, Designing Competitive Online Algorithms via a Primal-Dual Approach, PhD thesis, Tel Aviv University, 2008, §2.1, pp. 7–9. https://www.tau.ac.il/~nivb/download/phd-thsis.pdf
Dimitris Bertsimas and John N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997 — the general form used by the imported strong-duality theorem.

11 thms4 active usersReviewed

Quantum Information·Captain: Goku

Stabilizer Rank of Magic StatesOpen Problem

Motivation

Quantum circuits built from Clifford gates alone are classically simulable in polynomial time. Universality is recovered by adding copies of a magic state, and the fastest known classical simulators of such circuits work by writing the magic-state input as a short linear combination of stabilizer states. The length of the shortest such combination -- the stabilizer rank -- is therefore the exponent governing classical simulation of quantum computation in this model, and lower bounds on it are among the very few unconditional obstructions to classical simulation available at all.

A timeline of what is established for the standard magic state $|H\rangle$ :

2016. Bravyi, Smith and Smolin exhibit a decomposition giving $\chi(|H^{\otimes 6}\rangle)\le 7$ , hence $\chi(|H^{\otimes n}\rangle)\le 7^{\,n/6}\le 2^{\,0.468n}$ , and prove a lower bound of order $\sqrt{n}$ .
2020. Huang, Newman and Szegedy show that hardness assumptions stronger than $\mathrm{P}\neq\mathrm{NP}$ , such as the exponential time hypothesis, imply $\chi(|H^{\otimes n}\rangle)=2^{\Omega(n)}$ (arXiv link).
2022. Peleg, Shpilka and Volk improve the unconditional lower bound to $\Omega(n)$ and give the first non-trivial bound for the approximate rank (arXiv:2106.03214).
2024. A quadratic lower bound is obtained for the approximate stabilizer rank (arXiv:2305.10277).

Between the linear unconditional lower bound and the $2^{0.468n}$ upper bound lies the open problem this mission targets.

Setting

Index the computational basis of an $n$ -qubit system by bit strings $x\in\{0,1\}^n$ , so a state is a vector $\psi\in\mathbb{C}^{2^n}$ with coordinates $\psi(x)$ .

The Pauli operators are $X^aZ^b$ for $a,b\in\{0,1\}^n$ , acting by $X^aZ^b|x\rangle=(-1)^{\,b\cdot x}|x\oplus a\rangle$ , where $b\cdot x$ counts the coordinates on which both are $1$ and $\oplus$ is bitwise addition; the Pauli group is the set of $4\cdot 4^n$ operators $i^cX^aZ^b$ . A unitary $U$ is a Clifford unitary when $UPU^\dagger$ lies in the Pauli group for every Pauli group element $P$ , and a stabilizer state is a vector $U|0\cdots0\rangle$ for some Clifford $U$ . There are $2^n\prod_{k=1}^{n}(2^k+1)$ of them up to phase -- six for a single qubit.

The stabilizer rank $\chi(\psi)$ is the least $r$ admitting coefficients $c_1,\dots,c_r\in\mathbb{C}$ and stabilizer states $\varphi_1,\dots,\varphi_r$ with $\psi=\sum_{j\le r}c_j\varphi_j$ .

The magic state is $|H\rangle=\cos(\pi/8)|0\rangle+\sin(\pi/8)|1\rangle$ , and $|H^{\otimes n}\rangle$ its $n$ -fold tensor power, with coordinates $\cos(\pi/8)^{\,n-|x|}\sin(\pi/8)^{\,|x|}$ where $|x|$ is the Hamming weight of $x$ .

Target

The goal is a super-polynomial lower bound: for every exponent $d$ and constant $C$ there exists $n$ with

\chi\bigl(|H^{\otimes n}\rangle\bigr)\;>\;C\,n^{d},

equivalently, $\chi(|H^{\otimes n}\rangle)$ is not $O(n^d)$ for any fixed $d$ .

Stronger statements are expected but are deliberately not the goal. An exponential bound $\chi=2^{\Omega(n)}$ is believed and follows from hardness assumptions, but a goal naming a specific growth rate would be superseded by the next improvement; super-polynomiality is the weakest statement that settles the question of principle.

Significance

The result itself. A super-polynomial lower bound would unconditionally rule out efficient classical simulation of Clifford-plus-magic-state circuits by stabilizer decomposition, currently the leading such technique. The converse direction shows how much is at stake: a polynomial upper bound on $\chi(|H^{\otimes n}\rangle)$ would imply $\mathrm{BPP}=\mathrm{BQP}$ , and via postselection $\mathrm{P}=\mathrm{NP}$ . There is also a purely classical payoff -- improving the known bound even to super-linear would produce a Boolean function computable in polynomial time requiring a super-linear number of summands in any decomposition into exponentials of quadratic forms over $\mathbb{F}_2$ , resolving a separate open question.

Formalizing it. The goal is open, so no known proof is being transcribed. What the mission produces is a machine-checked statement of the problem together with formalizations of the established bounds, none of which has a machine-checked proof anywhere. It also produces the first Pauli/Clifford/stabilizer layer in Lean: no existing Lean library contains the $n$ -qubit Pauli group, the Clifford group, or stabilizer states, and that layer is reusable for stabilizer error correction, magic monotones, and Clifford simulation generally.

Difficulty

Counting settles the problem for random states: the stabilizer states are too few for short combinations to cover a generic state, so almost every state has exponential stabilizer rank. This says nothing about $|H^{\otimes n}\rangle$ , which is a single explicit, highly structured vector, and the entire difficulty is that lower bounds must be proved for that specific state rather than for a typical one. Every newcomer proposes the counting argument; it does not apply.

The known techniques reduce the question to statements about decompositions of explicit Boolean functions into quadratic-form exponentials, and the barrier is quantitative: the available arguments lose a factor that caps them at linear bounds. The source of the current record documents explicitly why its method cannot pass super-linear, and the fact that going beyond linear would resolve an independent open problem in Boolean function complexity indicates the obstruction is not merely technical.

Formalization scope

State vectors are functions $\{0,1\}^n\to\mathbb{C}$ and are not required to be normalised; normalisation does not affect the rank, and stabilizer states are unit vectors automatically as Clifford images of $|0\cdots0\rangle$ . The Pauli group is given by the explicit parametrisation $i^cX^aZ^b$ rather than an abstract presentation, and the Clifford group is characterised as its unitary normaliser, equivalent to the usual generated-by- $H,S,\mathrm{CNOT}$ description. Because $e^{i\theta}U$ normalises the Pauli group whenever $U$ does, the stabilizer states are closed under global phase; this is harmless, as the coefficients are arbitrary complex numbers.

One trivialising reading must be excluded. The rank is defined as an infimum over a set of natural numbers, and Lean gives the empty infimum the value $0$ ; if no decomposition existed the rank would be $0$ for every state and the goal would be false rather than merely unproved. The milestone $\chi(\psi)\le 2^n$ is what certifies the set is nonempty, making the rank a genuine minimum, and it should be proved first. Separately, the goal quantifies $C$ over all reals including negative values, for which the inequality is trivially satisfiable; the content lies in large positive $C$ .

A complete development needs, beyond the published definitions, the correspondence between stabilizer states and affine subspaces carrying quadratic phase functions, on which all known lower-bound arguments rest. Contributions of any milestone are welcome, as are function-level reformulations of the rank and the equivalent characterisation of stabilizer states via maximal abelian Pauli subgroups.

Selected references

S. Peleg, A. Shpilka, B. L. Volk, Lower Bounds on Stabilizer Rank, Quantum 6 (2022) 652; arXiv:2106.03214.
S. Bravyi, G. Smith, J. Smolin, Trading Classical and Quantum Computational Resources, Phys. Rev. X 6 (2016) 021043; arXiv:1506.01396.
C. Huang, M. Newman, M. Szegedy, Explicit Lower Bounds on Strong Quantum Simulation, IEEE Trans. Inf. Theory 66(9) (2020) 5585--5600.
Quadratic Lower Bounds on the Approximate Stabilizer Rank: A Probabilistic Approach, STOC 2024; arXiv:2305.10277.

5 thms4 active usersReviewed

Completed

Algorithmic Game Theory·Captain: Shuze Chen

Algorithmic Game Theory I: Existence of Nash EquilibriumTextbook

Motivation

The strategic-form game is the basic object of noncooperative game theory, and the Nash equilibrium — a profile of randomized strategies from which no player benefits by deviating unilaterally — is its central solution concept. Nash proved in 1951 that every game with finitely many players and finite strategy sets has such an equilibrium (Nash, Non-cooperative games, Ann. Math. 54 (1951)); this single existence theorem is the reason the concept organizes the rest of the field, from the computational complexity of finding equilibria to the price of anarchy. The theorem is stated as Theorem 1.8 of Nisan–Roughgarden–Tardos–Vazirani (eds.), Algorithmic Game Theory (Cambridge, 2007), the source text of this mission series, whose first chapter (Tardos–Vazirani) also treats the two special cases that admit direct algorithmic proofs: two-person zero-sum games, where equilibria are exactly the optimal solutions of a dual pair of linear programs (von Neumann 1928; Theorem 1.11), and a simple linear market, where equilibrium prices are computed by an ascending tight-set algorithm (Theorem 1.17).

A timeline of the existence theorem: von Neumann (1928) proved the minimax theorem for two-person zero-sum games; Nash (1950, 1951) extended existence to arbitrary finite games, first via Kakutani's fixed-point theorem and then via Brouwer's. All known proofs of the general theorem pass through a fixed-point principle, and this is not an artifact: computing a Nash equilibrium is PPAD-complete (Daskalakis–Goldberg–Papadimitriou 2009; Chen–Deng–Teng 2009), and PPAD is precisely the complexity class of the fixed-point arguments.

Setting

A finite strategic-form game consists of a finite set $\iota$ of players, for each player $i$ a finite nonempty set $S_i$ of pure strategies, and for each player a payoff function $u_i : \prod_j S_j \to \mathbb{R}$ ; all players are utility maximizers. A mixed strategy for player $i$ is a probability distribution on $S_i$ , represented as a weight function $\sigma_i : S_i \to \mathbb{R}$ with $\sigma_i \ge 0$ and $\sum_{s} \sigma_i(s) = 1$ (a lottery). Players randomize independently, so a mixed profile $\sigma = (\sigma_i)_{i}$ induces the product distribution on pure strategy vectors, and player $i$ 's expected payoff is

U_i(\sigma) \;=\; \sum_{s \in \prod_j S_j} \Big(\prod_j \sigma_j(s_j)\Big)\, u_i(s).

A mixed profile $\sigma$ is a (mixed) Nash equilibrium if for every player $i$ and every lottery $\tau$ on $S_i$ , replacing $\sigma_i$ by $\tau$ does not increase $U_i$ .

A two-person zero-sum game is given by a matrix $A \in \mathbb{R}^{m \times n}$ : the row player picks a row distribution $p$ , the column player a column distribution $q$ , and the column player pays the row player $p^{\mathsf T} A q$ in expectation.

The market of §1.8.1 of the source has finitely many divisible goods, good $a$ in $s_a$ units, and finitely many buyers, buyer $j$ bringing budget $m_j > 0$ and interested in a nonempty set of goods; utilities are linear 0/1, so a buyer wants any goods from her interest set and none other. Market-clearing prices are positive prices under which each buyer can spend her whole budget on cheapest goods in her interest set while every good sells out exactly.

Formalization targets

Goal (capstone) — Theorem 1.8

\text{Every finite strategic-form game has a mixed Nash equilibrium.}

Stated for an arbitrary finite family of finite nonempty strategy types; no bound on the number of players, no genericity assumptions.

Supporting — Brouwer fixed-point theorem

K \subseteq E \text{ nonempty compact convex},\ E \text{ finite-dimensional},\ f : K \to K \text{ continuous} \implies \exists x,\ f(x) = x.

Mathlib currently has no form of Brouwer's theorem; every known proof of Theorem 1.8 needs it (or an equivalent), so it enters the mission as an explicit milestone rather than an assumed library fact.

Theorem 1.11 — zero-sum games

\exists\, p^\ast, q^\ast:\quad \forall p,\ p^{\mathsf T} A q^\ast \le {p^\ast}^{\mathsf T} A q^\ast, \quad \forall q,\ {p^\ast}^{\mathsf T} A q^\ast \le {p^\ast}^{\mathsf T} A q, \quad\text{and}\quad (p^\ast, q^\ast) \text{ is a mixed Nash equilibrium}

of the explicit two-player game with payoffs $A_{xy}$ to the row player and $-A_{xy}$ to the column player. The source states the result as: optimal solutions of a dual pair of LPs form a Nash equilibrium of the zero-sum game; the first two conjuncts are the saddle point that LP optimality amounts to, and the third states the Nash-equilibrium clause against the mission's own game vocabulary, so "zero-sum" is formal (the two payoffs sum to zero) rather than implicit in the shape of the statement.

Theorem 1.17 (existence form)

\text{The 0/1-utilities linear market admits market-clearing prices and allocations.}

The source proves this by an ascending-price algorithm and also bounds its running time; the complexity half has no formal counterpart in this mission.

Significance

The capstone is the foundation of the whole mission series: correlated equilibria, price-of-anarchy bounds, and mechanism-design characterizations in later missions all quantify over or compare against Nash equilibria, and the series inherits its game vocabulary (IsLottery, IsMixedProfile, expectedPayoff, IsMixedNash) from this mission.

Formalizing it produces the first Brouwer fixed-point theorem in this environment — a well-known gap in mathlib with reuse value far beyond game theory (every degree-theoretic and equilibrium-existence argument needs it). The zero-sum milestone yields the minimax theorem, reusable for the learning-dynamics mission that follows. All results here are classical and proved on paper; the work requested is machine-checked proof, not new mathematics.

Difficulty

The central difficulty is Brouwer. The standard routes are (i) Sperner's lemma plus a limit argument, which needs a formal theory of simplicial subdivisions that does not exist in mathlib; (ii) algebraic topology (no retraction of the ball onto the sphere), for which mathlib has singular homology but not yet the homology of spheres in usable form; (iii) analytic proofs (Milnor–Rogers). None is short; the milestone is deliberately stated for a general nonempty compact convex set in a finite-dimensional normed space so that any route serves, and so the lemma lands in reusable generality.

Given Brouwer, Theorem 1.8 still requires Nash's gain-function construction on the product of simplices and the verification that fixed points are equilibria — bookkeeping-heavy but standard. Theorem 1.11 does not need Brouwer: mathlib's Sion minimax theorem (Mathlib.Topology.Sion) applies to the bilinear payoff on the product of standard simplices, or one can argue by LP duality directly. Theorem 1.17 needs the tight-set/max-flow argument of Lemmas 1.15–1.16 or any direct construction of the equilibrium.

Formalization scope

Games are presented concretely: players form a finite index type, strategies a finite type per player, payoffs are functions into $\mathbb{R}$ ; mixed strategies are weight functions with a IsLottery predicate, not measure-theoretic distributions. Deviations in the equilibrium definition range over all lotteries (not only pure strategies): the pure-deviation reduction is a lemma a solver may prove, not part of the definition. Strategy sets are assumed nonempty in the capstone; the player set need not be. In the zero-sum milestone both dimensions are positive (Fin (m+1), Fin (n+1)), payoffs flow from the column player to the row player, stdSimplex plays the role of the mixed-strategy space, and the Nash-equilibrium conjunct is stated for the Boolean-indexed two-player game built by matrixGameStrat/zeroSumPayoff/matrixGameProfile from the definitions bundle. In the market milestone all supplies and budgets are positive, every buyer's interest set is nonempty, and every good has an interested buyer, matching the standing assumptions of §1.8.1; allocations are recorded as money spent, so the clearing condition is $\sum_j x_{ja} = p_a s_a$ with no division anywhere.

Trivializing readings are ruled out: the empty simplex has no lotteries, so nonemptiness hypotheses appear exactly where their absence would make an existence claim false (Brouwer on the empty set, games with an empty strategy set, zero-dimensional matrix games).

Selected references

J. F. Nash, Non-cooperative games, Annals of Mathematics 54 (1951), 286–295. DOI
J. von Neumann, Zur Theorie der Gesellschaftsspiele, Mathematische Annalen 100 (1928), 295–320. DOI
N. Nisan, T. Roughgarden, É. Tardos, V. V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007, Chapter 1. DOI
C. Daskalakis, P. W. Goldberg, C. H. Papadimitriou, The complexity of computing a Nash equilibrium, SIAM J. Computing 39 (2009), 195–259. DOI

10 thms4 active usersReviewed

Completed

Captain: marwahaha

Schönhage–Pan–Winograd Bound: omega < 2.522Research Paper

Motivation

The matrix-multiplication exponent measures the asymptotic arithmetic cost of multiplying square matrices. An upper bound $\omega<c$ means that, over the field under consideration, $N\times N$ matrices can be multiplied using $O(N^{c+\varepsilon})$ arithmetic operations for every $\varepsilon>0$ . Improvements to $\omega$ are a central benchmark in algebraic complexity because matrix multiplication is also a basic subroutine in linear algebra, graph algorithms, and symbolic computation.

The existing Prove2Me mission formalizes Schönhage's bound $\omega<2.55$ from a concrete two-summand tensor degeneration. The present mission advances the same formal development to the next clean historical construction. Pan and Winograd found a simultaneous approximate algorithm for three matrix products; Romani recorded its tensor form and the parameter choice $n=11$ , $k=5$ , which gives $\omega\le 2.5218127\ldots$ . Schönhage's 1981 paper reports the equivalent bound $3\log 52/\log 110$ in the arbitrary-field setting. The exact formal target here is the slightly weaker rational inequality $\omega<1261/500=2.522$ .

Setting

For a field $K$ , the matrix-multiplication tensor $\langle a,b,c\rangle_K$ encodes multiplication of an $a\times b$ matrix by a $b\times c$ matrix:

\langle a,b,c\rangle_K =\sum_{i<a}\sum_{j<b}\sum_{\ell<c} e_{ij}\otimes e_{j\ell}\otimes e_{\ell i}.

A direct sum places several such tensors in disjoint coordinate blocks. A tensor $T$ has border rank at most $r$ when it is a polynomial degeneration of the diagonal tensor $I_r=\sum_{s<r}e_s\otimes e_s\otimes e_s$ . In the Lean development this relation is Degenerates T (TensorObj.diagObj K 3 r). The argument order matters: the first tensor is the target and the diagonal tensor is the source.

The platform already defines ordinary tensor rank, asymptotic tensor rank, the tensor-rank exponent matMulExp K, the equivalent Strassen-preorder exponent matMulExp_strassen K, and Schönhage's asymptotic sum inequality. This mission reuses those declarations. No alternative definition of $\omega$ is introduced.

Formalization targets

The goal has exactly the same quantified proposition as the existing $2.55$ mission, with only the rational endpoint changed:

\forall K\;[\mathrm{Field}(K)],\qquad \operatorname{matMulExp}(K)<\frac{1261}{500}.

The source construction to be formalized is

\underline R\!\left( \langle1,5,22\rangle_K\oplus \langle11,2,5\rangle_K\oplus \langle10,11,1\rangle_K \right)\le156.

Each summand has volume $110$ :

1\cdot5\cdot22=11\cdot2\cdot5=10\cdot11\cdot1=110.

The milestone chain records the degeneration, its asymptotic-rank consequence, the exact numerical implication

3\cdot110^{\omega^{\mathrm{Str}}_K/3}\le156 \quad\Longrightarrow\quad \omega^{\mathrm{Str}}_K<\frac{1261}{500},

and the resulting Strassen-form exponent bound. The public goal then transfers the bound to matMulExp K through the already established equality of the two exponent definitions.

Significance

Mathematically, this construction improves the concrete exponent certified by the existing mission from $2.55$ to $2.522$ without changing the surrounding theory. It isolates the first genuinely new ingredient after the accepted Schönhage example: a larger simultaneous tensor degeneration rather than a sharper numerical estimate for the old witness.

For formalization, the mission tests whether the current polynomial-degeneration API can express a historically important trilinear aggregation at realistic scale. Once the explicit witness is available, the remaining declarations form a reusable template for later bounds: a source tensor degeneration, an asymptotic-rank bound, a specialization of the asymptotic sum inequality, and a final exponent transfer. This creates a trustworthy stepping stone toward the Coppersmith--Winograd tensor and later laser-method analyses.

The $2.522$ theorem is known mathematically; the open work is its machine-checked Lean formalization. The exact numerical endpoint and every downstream bridge from the degeneration have already been checked locally. The explicit Pan--Winograd degeneration remains the substantive open milestone.

Difficulty

The central difficulty is not the logarithmic comparison. It is constructing and verifying the polynomial family whose leading nonzero coefficient is exactly the tagged direct sum of the three matrix-multiplication tensors and whose earlier coefficients vanish. The family has $156$ diagonal source slots and many indexed target coordinates. A proof must account for all mixed-coordinate terms and all cancellations uniformly over an arbitrary field.

Romani's published summary states the approximate-rank inequality but does not spell out a Lean-ready map between its trilinear forms and the platform's TensorObj.bigAdd coordinate spaces. A solver must therefore recover the source indexing carefully and prove that the resulting modewise linear maps have the required coefficients. Reversing the degeneration direction, conflating tensor rank with asymptotic rank, or silently assuming a characteristic-zero scalar identity would invalidate the result.

Formalization scope

All theorems quantify over an arbitrary type $K$ with [Field K], matching the existing Schönhage goal and the arbitrary-field statement of the source bound. Tensor spaces are finite-dimensional function spaces already packaged by MMObj; the three products are combined with TensorObj.bigAdd. Border rank is represented by the existing finitely supported polynomial-family predicate Degenerates. Because the source summary specifies approximate rank but not a leading order, the main degeneration milestone existentially quantifies that order instead of hard-coding one.

The mission includes no placeholder laser-value definition and makes no claim about the later $2.376$ analysis. It also excludes Schönhage's additional microscopic symmetrization improvement beyond $3\log52/\log110$ . A valid solution must construct the stated degeneration itself; a vacuous hypothesis or a redefinition of matMulExp is outside scope.

Reusable contributions include coefficient lemmas for polynomial tensor families, finite-index equivalences for direct sums, and generic aggregation identities that specialize to the $n=11$ , $k=5$ witness. Contributions that merely restate the target under stronger field hypotheses do not close the arbitrary-field milestone.

Selected references

A. Schönhage, Partial and Total Matrix Multiplication, SIAM Journal on Computing 10(3), 1981, pp. 434--455. DOI 10.1137/0210032.
Francesco Romani, Some Properties of Disjoint Sums of Tensors Related to Matrix Multiplication, CNR Nota Interna B80-4, February 1980, printed p. 6; journal version, SIAM Journal on Computing 11(2), 1982. Archived preprint and DOI 10.1137/0211020.
Avi Wigderson and Jeroen Zuiddam, Asymptotic Spectra: Theory, Applications and Extensions, 2023, for the tensor-preorder and asymptotic-rank framework reused by the Lean development. Author manuscript.

27 thms4 active usersReviewed

Information Theory Quantum Information·Captain: mikedeng1

Shadow Tomography of Quantum States 3: Shadow Tomography Needs Ω(min{D², log M}/ε²) CopiesResearch Paper

Why count copies of a quantum state

A mixed state of a $D$ -dimensional quantum system is a $D\times D$ positive semidefinite matrix $\rho$ of trace $1$ . Writing $\rho$ down takes about $D^2$ real numbers, and $D$ is exponential in the number of qubits, so learning $\rho$ in full is expensive. Holevo's theorem and the random access code bounds of Ambainis, Nayak, Ta-Shma and Vazirani say that an $n$ -qubit state carries far fewer usable classical bits than its $2^n$ amplitudes suggest. Shadow tomography, introduced by S. Aaronson (arXiv:1711.01053), makes this quantitative: given $M$ known two-outcome measurements $E_1,\dots,E_M$ , how many copies of an unknown $\rho$ are needed to estimate every acceptance probability $\operatorname{Tr}(E_i\rho)$ to within $\varepsilon$ ?

Aaronson shows that $\widetilde O(\log^4 M\cdot\log D/\varepsilon^4)$ copies suffice, polylogarithmic in $M$ and $D$ . The question this mission addresses is the converse: how many copies are necessary. Section 6 of the paper proves two lower bounds. Theorem 16 gives $\Omega(\min\{D,\log M\}/\varepsilon^2)$ even when $\rho$ and the $E_i$ are diagonal (a classical distribution). Theorem 19, the goal here, strengthens the dimension term to $D^2$ for genuinely quantum states.

Timeline:

2016: full tomography of a $D$ -dimensional state to trace-distance accuracy $\varepsilon$ needs $\Theta(D^2/\varepsilon^2)$ copies up to logarithmic factors, with upper and lower bounds by O'Donnell and Wright (arXiv:1508.01907) and Haah, Harrow, Ji, Wu and Yu (arXiv:1508.01797).
2017–2018: Aaronson poses shadow tomography (Problem 1), proves the polylogarithmic upper bound (Theorem 2), and proves the lower bounds of Theorems 16 and 19.
2020 onward: classical shadows (Huang, Kueng and Preskill, arXiv:2002.08953) and later shadow-tomography algorithms study the same estimation task with other measurement models and improved upper bounds.

Setting

Fix a dimension $D$ . A two-outcome measurement is a $D\times D$ Hermitian matrix $E$ with $0\preceq E\preceq I$ ; it accepts $\rho$ with probability $\operatorname{Tr}(E\rho)$ . The tensor power $\rho^{\otimes k}$ is the $D^k\times D^k$ matrix of $k$ independent copies. A strategy using $k$ copies is a measurement of $\rho^{\otimes k}$ with finitely many outcomes $\omega\in\Omega$ , given by positive semidefinite matrices $\Pi_\omega$ with $\sum_\omega\Pi_\omega = I$ , together with outputs $b(\omega)=(b_1(\omega),\dots,b_M(\omega))$ . It succeeds on $\rho$ when, with probability at least $2/3$ over $\omega$ , $|b_i(\omega)-\operatorname{Tr}(E_i\rho)|\le\varepsilon$ for every $i\in[M]$ .

The proof works with these further objects, all defined in the mission:

an orthogonal projection $\mathbb P$ onto an $N/2$ -dimensional subspace of $\mathbb C^N$ (Hermitian, idempotent, trace $N/2$ );
$\rho_{\mathbb P} := \tfrac2N\mathbb P$ , the maximally mixed state on that subspace;
$\sigma_{\mathbb P,\varepsilon} := (1-6\varepsilon)\,\mathbb I/N + 6\varepsilon\,\rho_{\mathbb P}$ ;
the von Neumann entropy in bits, $S(\rho) = -\sum_x\lambda_x\log_2\lambda_x$ over the eigenvalues of $\rho$ ;
for states $\sigma_1,\dots,\sigma_K$ and $\zeta := \tfrac1K\sum_i\sigma_i^{\otimes T}$ , the quantum mutual information with the classical index, $I(\zeta;i) := S(\zeta) - \tfrac1K\sum_i S(\sigma_i^{\otimes T})$ .

Formalization targets

Goal: Theorem 19 (p. 23)

There are a universal constant $c>0$ and a threshold $N_0$ such that for all $D\ge N_0$ , all $M$ with $\log_2 M\ge N_0^2$ and all $0<\varepsilon\le\tfrac16$ , some measurements $E_1,\dots,E_M$ on $\mathbb C^D$ force every strategy that succeeds on every mixed state to use

k \;\ge\; c\,\frac{\min\{D^2,\ \log_2 M\}}{\varepsilon^2}

copies. The goal fixes only the shape $\Omega(\min\{D^2,\log M\}/\varepsilon^2)$ , not a constant, so a sharper constant does not invalidate it.

Milestones (pp. 23–24)

The milestones follow the proof, which sets $N:=\lfloor\min\{D,\sqrt{\log_2 M}\}\rfloor$ and $K:=\lfloor c^{N^2}\rfloor$ :

Eq. (2): for some $c\in(1,2)$ and all large even $N$ there are $K$ projections $\mathbb P_i$ of rank $N/2$ with $|\operatorname{Tr}(\mathbb P_i\rho_j)-\tfrac12|\le\tfrac1{12}$ for all $i\ne j$ .
$\operatorname{Tr}(\mathbb P_i\sigma_i) = \tfrac12+3\varepsilon$ .
$|\operatorname{Tr}(\mathbb P_j\sigma_i)-\tfrac12| = 6\varepsilon|\operatorname{Tr}(\mathbb P_j\rho_i)-\tfrac12|\le\tfrac\varepsilon2$ for $i\neq j$ .
The exact entropy $S(\sigma_i) = \log_2 N - [1-h(\tfrac12+3\varepsilon)]$ , with $h$ the binary entropy, and the bound $S(\sigma_i)\ge\log_2 N - C\varepsilon^2$ .
$I(\zeta;i)\le T(\log_2 N - S(\sigma_i))$ when all $\sigma_i$ have equal entropy.

Significance

Theorem 19 shows that the $\log M$ dependence of shadow tomography cannot be removed, and that for $M\ge 2^{D^2}$ shadow tomography is as hard as full tomography: as $M$ grows the bound becomes the $\Omega(D^2/\varepsilon^2)$ tomography lower bound, which it therefore contains. Compared with the classical Theorem 16, it shows that quantum states need quadratically more copies in the dimension term. The $1/\varepsilon^2$ factor matches the upper bound of Proposition 20 for the decision version, so the $\varepsilon$ -dependence of the lower bound is tight in that setting.

The results are proved in the paper; none of them has a machine-checked proof that we know of. Formalizing the argument requires von Neumann entropy and its additivity on tensor products, the bound $S\le\log_2(\text{dimension})$ , a Holevo-plus-Fano step that turns successful estimation into mutual information, and the existence of many nearly orthogonal half-dimensional subspaces. Each is reusable well beyond this mission.

Difficulty

The obvious attempt adapts the classical argument of Theorem 16, which hides $K$ subsets of $[N]$ in a biased distribution. Quantum states allow $\exp(\Omega(N^2))$ hidden subspaces instead of $\exp(\Omega(N))$ subsets, which is where $D^2$ comes from, but two steps change character. First, the hiding family must be shown to exist: Eq. (2) is a concentration statement for random subspaces, and the lemma the paper cites for it (Lemma 18) is misstated, as explained below. Second, the information bound must be carried out for quantum states: the step "learning $i$ from $\zeta$ requires $I(\zeta;i)\ge\log_2 K$ " needs Holevo's bound and Fano's inequality, adjusted for success probability $2/3$ rather than certainty.

Formalization scope

Matrices are Matrix n n ℂ over a finite index type; the goal uses $n=\texttt{Fin } D$ . Conventions committed to:

A mixed state is the published WildeQIT.IsDensityOperator (positive semidefinite, trace $1$ ), reused as a reference item.
A strategy is a finite-outcome POVM on $\rho^{\otimes k}$ , indexed by Fin k → Fin D, with deterministic outputs $b(\omega)\in\mathbb R^M$ ; classical randomness can be absorbed into the outcome set.
Probabilities and traces are real parts of complex traces. Entropies use $\log_2$ ; Lean's $\log_2 0 = 0$ gives $0\log 0=0$ , and vnEntropy returns $0$ on non-Hermitian matrices, which no statement uses.
Added to the goal: the threshold $N_0$ on $D$ and $\sqrt{\log_2 M}$ (for $D=1$ , $k=0$ succeeds) and $\varepsilon\le\tfrac16$ (for $\varepsilon\ge\tfrac12$ , the output $b_i=\tfrac12$ succeeds with $k=0$ ). Problem 1's $b_i\in[0,1]$ is dropped, an equivalent statement under clipping.
The measurements are chosen before the strategy (for every strategy, the same $E$ ), which is the meaning of a lower bound.

A trivializing formalization is ruled out: the goal does not mention $N$ , $K$ , $\mathbb P_i$ , $\sigma_i$ or $\zeta$ , the success condition quantifies over all mixed states rather than a vacuous class, and the measurements are fixed before the strategy.

Not drafted:

Lemma 18 (pp. 22–23) is false as printed. Since $\mathbb E_S[\rho_S] = \mathbb I/N$ , $\operatorname{Tr}(\mathbb P_T\rho_S)$ concentrates at $1/2$ , not $1/4$ . The proof needs only Eq. (2), which is centred correctly and is a milestone.
Eq. (2) is stated as existence, not as "probability $1-o(1)$ over Haar-random subspaces", because Mathlib has no Haar measure on the unitary group or the Grassmannian; existence is what the proof uses.
" $I(\zeta;i)$ must be at least $\log_2 K$ " is not drafted: as stated it is imprecise for success probability $2/3$ , and the correct Holevo–Fano form is left to the solver.
The final combination $I(\zeta;i)=O(T\varepsilon^2)$ , $T=\Omega(N^2/\varepsilon^2)$ is the goal's last step.

Contributions welcome: proofs of the milestones; a Haar-measure version of Eq. (2); von Neumann entropy infrastructure (additivity, the dimension bound, concavity); Holevo's bound and Fano's inequality for finite-dimensional states.

Selected references

S. Aaronson, Shadow Tomography of Quantum States, arXiv:1711.01053v2, 2018; STOC 2018. https://arxiv.org/abs/1711.01053
P. Hayden, D. Leung, A. Winter, Aspects of generic entanglement, Comm. Math. Phys. 265, 2006. https://arxiv.org/abs/quant-ph/0407049
R. O'Donnell, J. Wright, Efficient quantum tomography, STOC 2016. https://arxiv.org/abs/1508.01907
J. Haah, A. W. Harrow, Z. Ji, X. Wu, N. Yu, Sample-optimal tomography of quantum states, IEEE Trans. Inf. Theory 63, 2017. https://arxiv.org/abs/1508.01797
A. Ambainis, A. Nayak, A. Ta-Shma, U. Vazirani, Dense quantum coding and quantum finite automata, J. ACM 49, 2002. https://arxiv.org/abs/quant-ph/9804043
H.-Y. Huang, R. Kueng, J. Preskill, Predicting many properties of a quantum system from very few measurements, Nature Physics 16, 2020. https://arxiv.org/abs/2002.08953

16 thms3 active usersReviewed

Combinatorics Operations Research Probability·Captain: mikedeng1

A Polylogarithmic-Competitive Algorithm for the k-Server Problem: Randomized k-Server Is O(log² k · log³ n · log log n)-Competitive on Every n-Point MetricResearch Paper

Motivation

The k-server problem (Manasse, McGeoch and Sleator, 1990) is the central problem of online computation: $k$ servers sit on points of a metric space, requests arrive one at a time at points of the space, and each request must be served by moving a server to it, at a cost equal to the distance travelled. An online algorithm decides without knowing future requests; its quality is its competitive ratio, the worst-case ratio between its cost and the cost of an optimal offline schedule. Paging (caching) is the special case of a uniform metric, and weighted paging the case of a weighted star.

Timeline of the upper bounds for general metrics:

1990: Manasse, McGeoch and Sleator prove that every deterministic algorithm has ratio at least $k$ and conjecture that $k$ is achievable.
1991: Fiat, Rabani and Ravid give the first ratio depending on $k$ only (exponential in $k$ ).
1995: Koutsoupias and Papadimitriou prove that the work function algorithm is $(2k-1)$ -competitive.
For randomized algorithms against an oblivious adversary, the conjectured answer is $O(\log k)$ , achieved for paging (Fiat et al., 1991), but until 2011 nothing better than the deterministic $2k-1$ was known for general metrics, even when the ratio may depend on the number of points $n$ .
2011: Bansal, Buchbinder, Mądry and Naor give the first polylogarithmic bound, $O(\log^2 k\log^3 n\log\log n)$ (arXiv:1110.1580; J. ACM 62(5), 2015, DOI 10.1145/2783434), the result of this mission.

Setting

Let $(M,\mathrm{dist})$ be a finite metric space with $n$ points and $k$ a number of servers. A configuration $C:\{1,\dots,k\}\to M$ places server $i$ at $C(i)$ . A deterministic online algorithm maps each prefix of the request sequence to a configuration that has a server at the last request; its cost on a sequence $\rho$ is the total distance travelled. $\mathrm{OPT}(C_0,\rho)$ is the least cost of any schedule serving $\rho$ from the initial configuration $C_0$ . A randomized algorithm is a probability distribution over deterministic online algorithms, all starting at $C_0$ ; it is $c$ -competitive if there is a constant $a$ such that its expected cost on every request sequence $\rho$ is at most $c\cdot\mathrm{OPT}(C_0,\rho)+a$ .

The paper works with three auxiliary objects. A σ-HST is a rooted tree whose leaves are the points, in which all edges from a node to its children have one common length, equal to $1/\sigma$ times the length of the edge above that node; the distance between two leaves is the length of the tree path. A weighted σ-HST only requires that the edge above a non-root internal node be at least $\sigma$ times each edge below it. In the fractional k-server problem on a tree, the state is a vector $x$ of server probabilities on the leaves with $0\le x_i\le1$ and $\sum_i x_i=k$ , a request at leaf $i$ forces $x_i=1$ , and moving from $x$ to $x'$ costs $\sum_v W(v)\,|x'_v-x_v|$ , where $x_v$ is the mass below node $v$ and $W(v)$ the length of the edge above $v$ . In the allocation problem on a weighted star with weights $w_i$ , requests carry a location $i^t$ , a monotone cost vector $h^t(0)\ge\dots\ge h^t(k)\ge0$ (the cost of serving with $j$ servers there) and a server quota $\kappa(t)\le k$ .

Formalization targets

Goal: Theorem 1

There is a universal constant $C>0$ such that for all $k\ge2$ , every metric space $M$ with $n\ge3$ points and every initial configuration $C_0$ , some randomized online algorithm starting at $C_0$ is

C\,\log^2 k\,\log^3 n\,\log\log n\text{-competitive.}

Milestones

In the order the proof uses them:

Claim 15: the fix-stage inequality behind the allocation algorithm's analysis.
Theorem 5: for every $0<\varepsilon\le1$ , a fractional allocation algorithm whose hit cost is at most $(1+\varepsilon)(\mathrm{Opt}+w_{\max}g(\kappa))+a$ and whose movement cost is at most $O(\log(k/\varepsilon))(\mathrm{Opt}+w_{\max}g(\kappa))+a$ , where $g(\kappa)=\sum_t|\kappa(t)-\kappa(t-1)|$ .
Theorem 6: given such allocation algorithms, an $O(\ell\log(k\ell))$ -competitive fractional k-server algorithm on every weighted σ-HST of depth $\ell$ with $\sigma=\Omega(\ell\log(k\ell))$ .
Theorem 8: every σ-HST with $n$ leaves becomes a weighted σ-HST of depth $O(\log n)$ on the same leaves, with distances distorted by at most $2\sigma/(\sigma-1)$ .
Lemma 25 and Theorem 24: on a σ-HST with $\sigma>5$ , randomized states consistent with a changing fractional state can be maintained online at cost $O(c_t)$ per step.
Theorem 7: on a σ-HST with $\sigma>5$ , a $c$ -competitive fractional algorithm yields an $O(c)$ -competitive randomized one.

Significance

The theorem broke the exponential gap between the $\Omega(\log k)$ lower bound and the $2k-1$ upper bound for randomized k-server, and showed that randomization helps on every finite metric, not only on uniform or specially structured ones. Its two-level method (a fractional algorithm on trees driven by per-node allocation problems, followed by an online rounding) became the template for later work, including the $O(\log^2 k)$ bound on HSTs of Bubeck, Cohen, Lee, Lee and Mądry (STOC 2018) and Lee's $O(\log^6 k)$ bound on general metrics (FOCS 2018).

The result is proved, in this paper. As far as is known it has no machine-checked proof. Formalizing it means formalizing the analysis of an online algorithm driven by a continuous-time process, a potential-function argument with exact constants, a tree contraction with a distortion bound, and an online randomized rounding against a transportation cost. The allocation, HST and rounding statements are reusable for other online problems on trees (metrical task systems, weighted paging).

Difficulty

For a deterministic or randomized algorithm on a tree, the natural recursion splits the servers of each node among its children. Coté, Meyerson and Poplawski showed that this works if each node solves an allocation problem with a strong guarantee: hit cost within a factor $1+\varepsilon$ of optimal. Integral allocation algorithms cannot achieve this; the integrality gap example of the paper (p. 8) gives a factor $\Omega(k)$ . The fractional relaxation avoids the gap, but then the rounding step must keep a randomized state consistent with a fractional state at constant-factor cost, and the HSTs obtained from general metrics have depth growing with the aspect ratio, which a depth-dependent ratio cannot afford. Each of the three reductions (allocation to fractional k-server, deep HST to shallow weighted HST, fractional to randomized) loses only polylogarithmic or constant factors, and the main theorem needs all three at once.

Formalization scope

The k-server model, randomized algorithms and competitiveness are the published definitions KServer_model and KServer_randomized; competitiveness carries an additive constant fixed before the request sequence. Trees are finite rooted trees with a parent map, a depth function and positive edge lengths; points of the k-server problem are the leaves, and the theorems take an arbitrary finite metric space together with a bijection to the leaves and the hypothesis that the distance equals the tree distance. Fractional k-server states have exactly $k$ units of mass, each leaf at most $1$ , and fractional algorithms are measured against the integral offline optimum. The allocation optimum is the integral optimum; cost vectors are finite, non-negative and non-increasing; the diameter of the star is $w_{\max}=\max_i w_i$ . The cost of changing a randomized state is the transportation cost over couplings, with minimum-matching cost between configurations. Every $O(\cdot)$ is an explicit constant quantified before the instance, except that in Theorems 7 and 24 and Lemma 25 it may depend on $\sigma$ .

Formalizations that make the targets trivial are excluded: the fractional state must place a full server on every request and stay in $[0,1]$ , the benchmark is the integral optimum (not the algorithm's own or the fractional cost), and no constant may depend on $k$ , $n$ , the metric or the tree, since otherwise Theorem 1 would follow from the $2k-1$ bound.

The proof of Theorem 1 also uses the embedding of Fakcharoenphol, Rao and Talwar [18] of a finite metric into a distribution over σ-HSTs with expected distortion $O(\sigma\log_\sigma n)$ . It is an external ingredient, not a result of this paper, and is not a milestone; contributions formalizing it (or Bartal's earlier embedding) are welcome, as are formalizations of the integral optimum's properties on trees (Lemmas 21–22 of the paper), which are not stated here.

Selected references

N. Bansal, N. Buchbinder, A. Mądry, J. Naor, A Polylogarithmic-Competitive Algorithm for the k-Server Problem, arXiv:1110.1580v1, 2011; J. ACM 62(5), 2015. https://arxiv.org/abs/1110.1580, https://doi.org/10.1145/2783434
M. Manasse, L. McGeoch, D. Sleator, Competitive algorithms for server problems, J. Algorithms 11, 1990. https://doi.org/10.1016/0196-6774(90)90003-W
E. Koutsoupias, C. Papadimitriou, On the k-server conjecture, J. ACM 42(5), 1995. https://doi.org/10.1145/210118.210128
A. Fiat, R. Karp, M. Luby, L. McGeoch, D. Sleator, N. Young, Competitive paging algorithms, J. Algorithms 12, 1991. https://doi.org/10.1016/0196-6774(91)90041-V
J. Fakcharoenphol, S. Rao, K. Talwar, A tight bound on approximating arbitrary metrics by tree metrics, J. Comput. Syst. Sci. 69(3), 2004. https://doi.org/10.1016/j.jcss.2004.04.011
A. Coté, A. Meyerson, L. Poplawski, Randomized k-server on hierarchical binary trees, STOC 2008. https://doi.org/10.1145/1374376.1374474

14 thms3 active usersReviewed

Theoretical Computer Science

Missions

The k-Server ConjectureOpen Problem

Motivation

Timeline

Setting

Formalization targets

Goal — the kkk-server conjecture

Milestones — the known ladder

Significance

Difficulty

Formalization scope

Selected references

More Asymmetry Bound: omega < 2.37134Research Paper

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

Duan–Wu–Zhou Fourth-Power Bound: omega < 2.37193Research Paper

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

The Cook-Levin Theorem: NP-Completeness of Boolean Satisfiability in Lean 4Research Paper

Introduction

Main Goal

Formal Conjectures Portfolio: Bateman-Horn and CompanionsOpen Problem

1. Motivation

2. Setting

3. Target

4. Significance

5. Difficulty

6. Formalization scope

7. Selected references

Davie–Stothers Fourth-Power Bound: omega < 2.3737Research Paper

Motivation

Setting

Formalization targets

Goal: the Davie--Stothers fourth-power bound

Source-level milestones

Significance

Difficulty

Formalization scope

Selected references

Scheduling Subject to Resource Constraints: Classification and Complexity II: Unit-Time Jobs on Two Uniform Machines with Unit Resources Are Strongly NP-hardResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3

Milestones

Significance

Difficulty

Formalization scope

Selected references

Immune High-Girth Bipartite Graphs (Feghali-Lucke-Paulusma-Ries 2025)Research Paper

Motivation

Setting

Formalization targets

Lemma 5 — immune high-girth graphs

Negative OPG consequence

Significance

Difficulty

Formalization scope

Selected references

Smale's Ninth Problem: Strongly Polynomial Linear ProgrammingOpen Problem

The problem of solving linear inequalities

Why it matters

The question and what is known

A hierarchy of formalization targets

Formalization scope

Selected references

The Sipser–Gács–Lautemann TheoremResearch Paper

AlphaEvolve Eighth-Power Bound: omega < 2.371177Research Paper

Competitive Paging Algorithms IV: An Algorithm Competitive against Several Others Exists iff the Reciprocal Ratios Sum to at Most 1Research Paper

Goal — the $k$ -server conjecture