Theoretical Computer Science

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

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

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.

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

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.

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:

under the decider and reduction hypotheses.

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

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

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

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$,

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.

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

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

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

1. 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.
2. 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$.
3. 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.
4. 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

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:

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:

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

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.

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$

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)$,

Milestones

In the order of the paper's proof:

1. 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)$.
2. 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$.
3. 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.
4. 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|$.
5. 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

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

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

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

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$,

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

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.

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

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}$:

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$;
2. if $Q_K = X_K$, then $Q_K$ is the coarsest stable refinement of $P$;
3. if $Q_K \neq X_K$, another step applies;
4. $K \le n - 1$;
5. every $x \in U$ satisfies

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.

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$:

1. Marking. $r$ is marked; the moment $k+1$ vertices are marked, all marks except the one on $r$ are erased.
2. 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

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

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

1. 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).
2. At the start of every phase the marked vertices are exactly the covered ones, and the first request of a phase is unmarked.
3. 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.
4. It also pays $C_A \ge d'$, where $d'$ counts its servers off the final marked set at the end of the phase.
5. Hence $C_A \ge \max(l-d, d') \ge \tfrac12(l - d + d')$.
6. A request to a stale vertex is a fault with probability $c/s$ ($c$ clean vertices requested so far, $s$ stale vertices left).
7. 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

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

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

1. (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)$.
2. $\bar G_i$ is a traveling salesman graph: the shortest-path distance of $G_i$ is symmetric, nonnegative and satisfies the triangle inequality.
3. (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$.
4. Property a): every edge of $G_i$ is a shortest path between its endpoints.
5. 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$.
6. The optimal tour: $\mathrm{OPTIMAL}(\bar G_i)=2^{i+1}-1$.
7. 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$.
8. 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$.