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.

Learning with anomalies

In the on-line prediction model studied by Littlestone and Warmuth (Inform. and Comput. 108, 1994), a learner receives instances one at a time, predicts a binary label for each, and is then told the correct label. No probabilistic assumption is made: performance is measured by the number of mistakes on a worst-case sequence. When every label is given by some function of a known target class $F$, the best attainable worst-case number of mistakes is a combinatorial invariant of $F$, characterized by Littlestone (Mach. Learn. 2, 1988) through mistake trees, now called the Littlestone dimension.

Real data are rarely labelled exactly by a member of the class. Littlestone and Warmuth measure the departure by the number of anomalies: the number of trials inconsistent with the best function in the class. Their Weighted Majority algorithm makes a number of mistakes that grows linearly in the number of anomalies, and the rate of growth can be pushed towards $2$ mistakes per anomaly by the choice of the update factor $\beta$. Theorem 8.1 of the paper shows that no deterministic learner does better: rate $2$ is forced for every class with at least two members. This mission formalizes that lower bound.

Setting

Let $X$ be an arbitrary set (the domain) and $F$ a set of functions $X \to \{0,1\}$, possibly infinite. A trial is a pair $(x,y) \in X \times \{0,1\}$, and a sequence of trials $\mathcal S = ((x_1,y_1),\dots,(x_T,y_T))$ is finite; an instance may occur several times with different labels.

• The number of anomalies of $\mathcal S$ with respect to $f : X \to \{0,1\}$ is $\mathrm{anom}_f(\mathcal S) = \#\{t \le T : f(x_t) \ne y_t\}$.
• $S_\eta$ is the collection of sequences with at most $\eta$ anomalies with respect to $F$: those $\mathcal S$ with $\min_{f\in F} \mathrm{anom}_f(\mathcal S) \le \eta$.
• A deterministic on-line algorithm $A$ maps the list of earlier trials and the current instance to a predicted label. $M_A(\mathcal S)$ is the number of trials $t$ at which $A$'s prediction, computed from $(x_1,y_1),\dots,(x_{t-1},y_{t-1})$ and $x_t$, differs from $y_t$.
• $\mathrm{opt}(F,\eta) = \min_A \sup_{\mathcal S \in S_\eta} M_A(\mathcal S) \in \{0,1,\dots\} \cup \{\infty\}$.

A complete $k$-mistake tree for $F$ is a complete binary tree of height $k$ whose internal nodes carry instances of $X$ such that every labelling of a root-to-leaf path is realized by some $f \in F$; in Lean this is the predicate ShattersTree F k v.

Formalization targets

Goal: Theorem 8.1 (p. 250)

For every class $F$ with $|F| > 1$ and every $\eta \ge 0$,

The constant $2$ is the paper's, and the statement holds for infinite classes, including those with $\mathrm{opt}(F,0) = \infty$.

Milestones

1. The [Lit88, Lit89b] mistake tree (§8, p. 251): for any pool $F$ there is a complete $\mathrm{opt}(F,0)$-mistake tree. This is published and proved on the platform as UnderstandingML.soa_mistake_bound ($M_{\mathrm{SOA}}(F) \le \mathrm{Ldim}(F)$), referenced together with UnderstandingML.ldim_le_mistake_bound; together they identify $\mathrm{opt}(F,0)$ with the Littlestone dimension.
2. The first stage of the adversary (§8, p. 251): if $F$ has a complete $k$-mistake tree with $k \ge 1$, then against any deterministic algorithm there are $k-1$ trials on which it errs every time, an instance $x$, and two functions $f_1, f_2 \in F$ consistent with all these trials with $f_1(x) \ne f_2(x)$.

Significance

The theorem settles the optimal rate at which mistakes must grow with the number of anomalies for deterministic learners: $2$ per anomaly, uniformly over all non-trivial classes. Together with the upper bounds of §2 of the paper, it shows that the deterministic Weighted Majority algorithm is within an arbitrarily small factor of optimal in its dependence on the anomalies, and it explains the factor of $2$ that separates deterministic from randomized prediction (Theorem 8.2, a separate mission of this series, gives rate $1$ for randomized learners).

The result is proved in the paper; to the best of a search of the platform it has not been formalized. The mission produces a machine-checked lower bound in a general setting: arbitrary domain, arbitrary (possibly infinite) class, extended-natural-valued optimal bounds. The noise-free side, the Littlestone dimension and the Standard Optimal Algorithm, is already published on the platform from Shalev-Shwartz and Ben-David's textbook, and this mission connects it to the noisy setting.

Difficulty

The obvious argument forces one mistake per trial and stops: an adversary that always contradicts the learner leaves no function of $F$ with few anomalies once the trials outnumber the mistake tree. The difficulty is to spend the anomaly budget so that each anomaly buys two mistakes while the sequence stays in $S_\eta$, and to do so against an arbitrary algorithm, which may behave adversarially itself. The definition of $S_\eta$ through a minimum over the class (not a fixed target) and the possibility that $\mathrm{opt}(F,0)$ is infinite both have to be handled.

Formalization scope

• The domain is any type X; the class is F : Set (X → Bool); the hypothesis $|F| > 1$ is F.Nontrivial, which is meaningful for infinite classes (a cardinality ncard would be $0$ there).
• Algorithms, histories and mistake counts are those of the published module UnderstandingML_Online (OnlineAlg X Bool, history, mistakes, ShattersTree); an algorithm is an arbitrary function of the history and the current instance, so every deterministic learner is covered.
• Sequences are Fin T → X × Bool for every finite length T, with repeated instances and conflicting labels allowed.
• opt F η : ℕ∞ is an infimum over algorithms of a supremum over sequences in $S_\eta$; $\eta$ is a natural number. Membership in $S_\eta$ is "some $f \in F$ has at most $\eta$ anomalies", which is the paper's minimum over $F$.
• Swapping the quantifiers (one sequence hard for all algorithms) or replacing $\mathrm{opt}$ by a finite toNat truncation would give a different statement; neither is used.

Needed infrastructure: the identification $\mathrm{opt}(F,0) = \min_A M_A(F)$ (sequences with no anomaly are exactly the realizable ones), the existence of a shattered tree of depth $\mathrm{opt}(F,0)$ from the published Littlestone-dimension results, and the two-stage adversary. Contributions of general lemmas about ShattersTree (subtrees, truncation to smaller depth) are reusable for the randomized mission and beyond.

Selected references

• N. Littlestone, M. K. Warmuth, The Weighted Majority Algorithm, Information and Computation 108(2), 212–261, 1994. https://doi.org/10.1006/inco.1994.1009
• N. Littlestone, Learning quickly when irrelevant attributes abound: a new linear-threshold algorithm, Machine Learning 2, 285–318, 1988. https://doi.org/10.1007/BF00116827
• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 21. https://doi.org/10.1017/CBO9781107298019

Motivation

Expander graphs are sparse graphs in which every set of vertices has many neighbours. Families of them with bounded degree and expansion bounded away from zero are a basic tool of theoretical computer science: they are the main component of the sorting network of Ajtai, Komlós and Szemerédi (AKS 1983), the building block of superconcentrators and other graphs with strong connectivity properties, and an ingredient of many later constructions in coding theory, derandomization and complexity.

Expansion is hard to certify. Checking that every set of vertices has many neighbours means looking at exponentially many sets, and computing the exact expansion of a graph is coNP-complete. A spectral quantity, by contrast, is computable in polynomial time. N. Alon's paper Eigenvalues and expanders (Combinatorica 6 (1986) 83–96) proves that for regular bipartite graphs the two notions are equivalent: a graph is a strong expander if and only if the second-smallest eigenvalue of its Laplacian is bounded away from 0, with explicit constants in both directions. This is a discrete counterpart of Cheeger's inequality for Riemannian manifolds.

Timeline.

• 1983: Ajtai, Komlós and Szemerédi use bounded-degree bipartite expanders to build sorting networks of depth $O(\log n)$.
• 1984: Tanner (SIAM J. Alg. Disc. Meth. 5) bounds the neighbourhood size of a set in a regular bipartite graph by its second eigenvalue, the direction "eigenvalue gap implies expansion".
• 1985: Alon and Milman (J. Combin. Theory Ser. B 38) prove isoperimetric inequalities for graphs in terms of $\lambda(G)$ and introduce enlargers.
• 1986: Alon proves the converse direction, "expansion implies an eigenvalue gap" (Lemma 2.4 and Theorem 3.4 of the paper).

Setting

All graphs are finite and simple. For a graph $G = (V, E)$ and a set $X \subseteq V$, $N(X) = \{v \in V : vx \in E \text{ for some } x \in X\}$ is the set of neighbours of $X$; it may meet $X$.

The Laplacian of $G$ is $Q_G = \mathrm{diag}(d(v))_{v \in V} - A_G$, where $A_G$ is the 0–1 adjacency matrix and $d(v)$ the degree of $v$. It is symmetric with eigenvalues $0 = \lambda_0 \le \lambda_1 \le \dots \le \lambda_{n-1}$, counted with multiplicity, and $\lambda(G) = \lambda_1$ is its second-smallest eigenvalue. It is positive exactly when $G$ is connected.

• An $(n, d, c)$-magnifier is a graph on $n$ vertices with maximal degree $d$ in which every $X \subseteq V$ with $|X| \le n/2$ satisfies $|N(X) - X| \ge c|X|$.
• An $(n, d, \varepsilon)$-enlarger is a graph on $n$ vertices with maximal degree $d$ and $\lambda(G) \ge \varepsilon$.
• A bipartite graph $G = (I, O; E)$ has inputs $I$, outputs $O$ and edges only between $I$ and $O$. It is a strong $(n, d, c)$-expander if $|I| = |O| = n$, the maximal degree is $d$, and for every $X \subseteq I$

Formalization targets

Goal: Theorem 3.4

Let $G = (I, O; E)$ be a $d$-regular bipartite graph with $|I| = |O| = n$ and $\lambda = \lambda(G)$.

1. If $G$ is a strong $(n, d, c)$-expander then

2. If $\lambda \ge \varepsilon$ then $G$ is a strong $(n, d, c)$-expander with

Milestones, in the order of the paper

• Lemma 2.2 (Alon–Milman, already on the platform): for disjoint sets $A, B$ at distance $\varrho > 1$, $b \le (1-a)/(1 + (\lambda/d)a\varrho^2)$.
• Corollary 2.3: every $(n, d, \varepsilon)$-enlarger is an $(n, d, 2\varepsilon/(d+2\varepsilon))$-magnifier.
• Eq. (2.1): if $f$ is an eigenvector of $Q_G$ for $\lambda(G)$ and $g$ its positive part, then $\sum_{uv \in E}(g(u)-g(v))^2 \le \lambda \sum_v g^2(v)$.
• Lemma 2.4: every $(n, d, c)$-magnifier has $\lambda(G) \ge c^2/(4 + 2c^2)$.
• Lemma 3.1: a strong $(n, d, c)$-expander is a $(2n, d, c/16)$-magnifier.
• Proof of Lemma 3.3, spectrum: the two largest eigenvalues of $C^TC$, with $C$ the $I \times O$ biadjacency matrix, are $d^2$ and $(d - \lambda)^2$.
• Proof of Lemma 3.3, Tanner's bound: $|N(X)| \ge d^2|X| / \bigl(\alpha(d^2 - (d-\lambda)^2) + (d-\lambda)^2\bigr)$ with $\alpha = |X|/n$.
• Lemma 3.3: a $d$-regular bipartite graph is a strong $(n, d, (2d\lambda - \lambda^2)/d^2)$-expander.

Part (1) of the goal combines Lemmas 3.1 and 2.4; part (2) follows from Lemma 3.3.

Significance

The result. Theorem 3.4 makes expansion of regular bipartite graphs checkable in polynomial time up to a constant-factor loss. A random regular bipartite graph can be generated and its expansion certified by computing one eigenvalue. Lemma 2.4 is one of the first discrete Cheeger inequalities. Together with Corollary 2.3 it shows that magnifiers and enlargers are the same graphs up to the constants, and it underlies the later theory of spectral expanders, including the Alon–Boppana bound and Ramanujan graphs.

The formalization. The results are proved in the paper. The work is to formalize the known proofs. That includes Tanner's eigenvalue bound, which the paper only cites, and a max-flow min-cut argument, for which Mathlib has no general theorem. No machine-checked version of Lemma 2.4, Lemma 3.1, Lemma 3.3 or Theorem 3.4 is known to exist. Lemma 2.2 is already stated and proved on the platform as part of the Alon–Milman mission.

Difficulty

The direction "eigenvalue gap implies expansion" is a variational argument on the spectrum of $C^TC$. The converse is the hard one. A first attempt bounds $\lambda(G)$ from below by testing the Rayleigh quotient on indicator vectors of sets. That only gives upper bounds on $\lambda$: any one test vector does. A lower bound has to control every vector orthogonal to the constants at once. The paper first reduces to the positive part of an eigenvector (Eq. (2.1)). It then turns the combinatorial expansion of the graph into an analytic inequality for that function, using a network flow whose existence comes from the max-flow min-cut theorem. Step (ii) of the flow conditions printed on p. 87 is false as stated: the arcs $(u, u)$ of the network absorb part of the flow. The flow argument has to be repaired before it can be formalized.

Lemma 3.1 has its own obstacle: one-sided expansion of inputs must be converted into expansion of arbitrary vertex sets that mix inputs and outputs. This needs the strong form of expansion; for ordinary expanders the lemma is false.

Formalization scope

Graphs are SimpleGraph V on a Fintype. A bipartite graph lives on the sum type I ⊕ O, and IsIOBipartite forbids edges inside I and inside O. Cardinalities $|N(X)|$ are Set.ncard. "Maximal degree $d$" is read as G.maxDegree ≤ d; every statement is monotone in $d$ or fixes $d$ by regularity (G.IsRegularOfDegree d). The condition $|X| \le n/2$ is written $2|X| \le n$ in $\mathbb{N}$. All constants are real, and every subtraction and division is taken in $\mathbb{R}$.

Reused published items:

• $\lambda(G)$ is AlonMilman.Diameter.lambda1, the second-smallest eigenvalue of G.lapMatrix ℝ, which is $0$ by convention on fewer than two vertices.
• $N(X)$ is AKSSorting.Core.neighbours.
• Lemma 2.2 is AlonMilman.Diameter.theorem_2_5, which carries Alon–Milman's standing hypotheses that $G$ is connected and $n \ge 2$; outside them the inequality is trivial.

The page omits a few degenerate cases, and the following hypotheses are added for them. Each is necessary, with a counterexample recorded in the item's statement:

• $n \ge 1$ and $c \ge 0$ in Theorem 3.4 (1);
• $\varepsilon > 0$ in Theorem 3.4 (2);
• $n \ge 2$ and $c \ge 0$ in Lemma 2.4;
• $n \ge 2$ in Lemma 3.1 and in the $C^TC$ statement;
• $d \ge 1$ in Lemma 3.3;
• $\varepsilon \ge 0$ in Corollary 2.3.

Eq. (2.1) is stated in multiplied form, so no quotient by $\sum g^2$ appears.

The closing sentences of Theorem 2.5 and Theorem 3.4 ("Thus … one can prove efficiently …") are not formalized. Read as implications between expanders they reduce to monotonicity in $c$, because $c' \le c$; their content is algorithmic.

Several encodings would trivialize the mission and are excluded:

• a $\lambda$ other than the published second-smallest Laplacian eigenvalue, in particular one defined as the best constant of a quotient;
• expansion or magnifier conditions with a negative constant in a hypothesis;
• $|X| \le n/2$ with truncating natural-number division.

Contributions are welcome:

• Tanner's bound in Lean, which is reusable for any regular bipartite graph;
• a max-flow min-cut theorem for finite networks;
• the corrected flow lemma behind Eqs. (2.2)–(2.3);
• the spectral facts about $\lambda(G)$ for bipartite graphs ($\lambda \le d$ for $n \ge 2$, and $\lambda = d - \sigma_2(C)$).

Selected references

• N. Alon, Eigenvalues and expanders, Combinatorica 6 (1986) 83–96. https://doi.org/10.1007/BF02579166
• N. Alon and V. D. Milman, λ₁, isoperimetric inequalities for graphs, and superconcentrators, J. Combin. Theory Ser. B 38 (1985) 73–88. https://doi.org/10.1016/0095-8956(85)90092-9
• R. M. Tanner, Explicit concentrators from generalized N-gons, SIAM J. Algebraic Discrete Methods 5 (1984) 287–293. https://doi.org/10.1137/0605030
• M. Ajtai, J. Komlós and E. Szemerédi, Sorting in c log n parallel steps, Combinatorica 3 (1983) 1–19. https://doi.org/10.1007/BF02579338

Motivation

The k-server problem of Manasse, McGeoch and Sleator (J. Algorithms 11 (1990)) asks how $k$ mobile servers in a metric space should respond, on-line, to a sequence of requests at points of the space, each of which must be covered by a server. It is the central model of on-line computation: paging is the special case of a uniform metric, and many caching and scheduling problems reduce to it. For two servers the deterministic picture is complete: the optimal competitive ratio is $2$ on every metric space with at least three points.

Randomization changes the picture, and the smallest nontrivial case already shows how. On the equilateral triangle the optimal randomized ratio against an oblivious adversary is $3/2$. Karlin, Manasse, McGeoch and Owicki (Algorithmica 11 (1994) 542–571) computed the exact optimal randomized ratio for several nonuniform triangles, where the distances differ, and showed that it depends on the geometry. Their Theorem 12 settles the whole family of isosceles triangles with edge lengths $1$, $d$, $d$. These exact values are among the few known optimal randomized ratios for server problems.

Timeline:

• 1990: Manasse, McGeoch and Sleator introduce the $k$-server problem and prove the deterministic two-server ratio is $2$.
• 1990–1994: Karlin, Manasse, McGeoch and Owicki submit this paper (received August 1990, revised September 1991) and publish it in Algorithmica in 1994, with the isosceles-triangle ratios of Theorem 12 and the 3-4-5 triangle ratio $1652/1069$ of Theorem 13.
• Later: Karloff, Rabani and Ravid extend the technique to $\Omega(\log\log k)$ and $\Omega(\log k)$ randomized lower bounds (cited on p. 564); Bubeck, Coester and Rabani (STOC 2023) refute the randomized $k$-server conjecture.