The mathematical foundations of computation: which problems can be solved, by what algorithms, and at what cost in time, space, or communication. Distinguished by its emphasis on rigor and unconditional lower bounds, it spans computational complexity, algorithm design, automata and computability, cryptography, and the analysis of Boolean functions.
Missions
🏆Completed
Captain: marwahaha
Coppersmith–Winograd Bound: omega < 2.376Research Paper
AI generated but i think correct. I think the milestones make it really annoying but the central theorem looks correct.
## Motivation
The **matrix-multiplication exponent** measures the asymptotic number of field operations needed to multiply two square matrices. A bound $\omega<c$ means that, for every $\varepsilon>0$, two $n\times n$ matrices can be multiplied using $O(n^{c+\varepsilon})$ arithmetic operations. Matrix multiplication is a central benchmark in algebraic complexity and a primitive for many algorithms in linear algebra, graph theory, and symbolic computation.
After Strassen showed that $\omega<3$, a sequence of tensor constructions reduced the exponent further. Schönhage's asymptotic sum inequality made it possible to exploit simultaneous matrix products rather than a single square product. In 1990, [Don Coppersmith and Shmuel Winograd](https://www.sciencedirect.com/science/article/pii/S0747717108800132) combined an explicit low-border-rank tensor with a block extraction argument based on Salem--Spencer sets. Their basic analysis gave $\omega<2.38719$; coupling the random weights in the tensor square sharpened this to $\omega<2.375477$, hence the exact rational consequence $\omega<2.376$.
This mission formalizes that historical Coppersmith--Winograd result. It follows the source tensor and its actual block restrictions, while excluding placeholder “laser values” that are not backed by extracted direct sums of matrix-multiplication tensors.
## Setting
For a field $K$, an order-three tensor is represented by three finite-dimensional $K$-vector spaces and an element of their tensor product. The matrix-multiplication tensor
$$
\langle a,b,c\rangle_K
=\sum_{i<a}\sum_{j<b}\sum_{k<c}
x_{ij}\otimes y_{jk}\otimes z_{ki}
$$
encodes multiplication of an $a\times b$ matrix by a $b\times c$ matrix. A **restriction** applies one linear map to each tensor leg. A **degeneration** permits those maps to depend polynomially on a formal parameter and selects their first nonzero coefficient. Thus a degeneration from the diagonal tensor $I_r$ is a border-rank certificate $\underline R(T)\le r$.
The **Coppersmith--Winograd tensor** with parameter $q$ is
$$
T_q=
\sum_{i=1}^{q}
(x_0y_i z_i+x_i y_0z_i+x_i y_i z_0)
+x_0y_0z_{q+1}+x_0y_{q+1}z_0+x_{q+1}y_0z_0.
$$
It has border rank at most $q+2$. Its coordinates carry three classes, indexed by $0,1,2$, and its six nonzero block types are
$$
(0,1,1),\ (1,0,1),\ (1,1,0),\ (0,0,2),\ (0,2,0),\ (2,0,0).
$$
The first three blocks are matrix-multiplication tensors with dimensions $(1,1,q)$, $(q,1,1)$, and $(1,q,1)$; the other three are scalar products. Tensor powers therefore contain many typed rectangular matrix products. The **laser method** selects a large family with disjoint coordinate blocks and applies Schönhage's asymptotic sum inequality to all surviving products simultaneously.
## Formalization targets
### Goal: the 1990 Coppersmith--Winograd bound
For every field $K$,
$$
\operatorname{matMulExp}(K)<\frac{297}{125}=2.376.
$$
The Lean goal has the same quantified proposition and the same `matMulExp` definition as the existing Schönhage-bound mission; only the theorem identifier and rational endpoint change.
### Tensor and block foundations
The development records the characteristic-free order-three degeneration
$$
T_q\unlhd I_{q+2}
$$
and the exact matrix-product dimensions associated with every supported type sequence in $T_q^{\otimes N}$. These statements identify the algebraic input before any asymptotic counting is used.
### Coupled-weight extraction
For $q=6$, the tensor-square grading and the coupled-weight pruning must produce the direct sums and asymptotic inequality stated in Section 8 and in the coupled-constituent lemma on journal pp. 270--272. The final numerical milestone certifies the rational endpoint $297/125$ from exact inequalities, rather than treating the decimal $2.375477$ as a proof object.
## Significance
The result was the strongest matrix-multiplication bound for roughly two decades and introduced the tensor family that underlies the classical laser-method line of work. A formal proof supplies a checked bridge from an explicit border-rank identity to an exponent bound whose combinatorial extraction is substantially more delicate than the earlier Schönhage examples.
The formalization also produces reusable infrastructure. The order-three CW degeneration is an explicit polynomial-family test case over arbitrary fields. The six block identifications and type-count formulas can be reused in analyses of tensor powers. A faithful extraction predicate, stated through actual restrictions to direct sums of `MMObj` tensors, separates sound laser arguments from formulas that count incompatible or coordinate-sharing blocks as independent.
The mathematical bound is known. The open work is its machine-checked reconstruction in Lean. The border-rank theorem, per-type matrix-product restriction layer, tensor-square support invariant, balanced block calculation, Salem--Spencer set theorem, and exact $q=6$ numerical endpoint are already proved. The unrestricted value/rank bridge, the coupled-constituent extraction, and the full Section 8 auxiliary inequality remain the substantive frontier.
## Difficulty
The main difficulty is not expanding $T_q$ or evaluating a decimal logarithm. A tensor power contains exponentially many typed terms, but most share variables. They cannot all be placed in a direct sum, and counting all joint type sequences overestimates the usable matrix products. The source hashes coordinate blocks into a large progression-free set and prunes collisions so that the surviving blocks are genuinely independent.
The $2.376$ improvement adds a second layer. It begins with $T_q^{\otimes2}$, regroups variables into five classes, couples weights that were independent in the simpler analysis, and estimates a nontrivial central block by a further extraction. A formal proof must track the direction of every restriction, the exact multiplicities of all block types, and the loss introduced by pruning. Replacing exponential surviving-block counts by a polynomial number of blocks, or using joint entropy without the marginal compatibility constraints, changes the mathematical claim and is outside the mission.
## Formalization scope
The mission uses the existing `TensorObj`, `MMObj`, `TensorObj.Restrict`, `Degenerates`, `tensorAsymptoticRank`, `matMulExp`, and `matMulExp_strassen` declarations in the Mathlib environment pinned by the earlier matrix-multiplication mission. Tensor dimensions and type counts are natural numbers; exponent and optimization inequalities are real-valued. All top-level bounds quantify over an arbitrary field, matching the integral polynomial identities used by the construction.
Laser statements must exhibit, directly or through a faithful reusable predicate, restrictions from a tensor power to a finite direct sum of concrete matrix-multiplication tensors. The number and dimensions of the summands remain part of the witness. A constant-valued “laser functional,” a vacuous witness hypothesis, or a capacity definition that discards the exponential number of surviving blocks does not satisfy the mission.
Welcome contributions include restriction composition lemmas, tensor-power block equivalences, multinomial and entropy estimates with all marginal constraints, formal Salem--Spencer pruning, exact real-inequality certificates, and the coupled central-block value lemma. Every milestone should cite the corresponding equation, table, or lemma in the primary paper.
## Selected references
- Don Coppersmith and Shmuel Winograd, *Matrix Multiplication via Arithmetic Progressions*, Journal of Symbolic Computation 9, 1990, pp. 251--280. [ScienceDirect](https://www.sciencedirect.com/science/article/pii/S0747717108800132).
- Arnold Schönhage, *Partial and Total Matrix Multiplication*, SIAM Journal on Computing 10(3), 1981, pp. 434--455. [DOI 10.1137/0210032](https://doi.org/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](https://www.math.ias.edu/~avi/PUBLICATIONS/WigdersonZu_Final_Draft_Oct2023.pdf).
69 thms3 active usersReviewed
🏆Completed
Captain: marwahaha
Schönhage–Pan–Winograd Bound: omega < 2.522Research Paper
## Motivation
The **matrix-multiplication exponent** measures the asymptotic arithmetic cost of multiplying square matrices. An upper bound $\omega<c$ means that, over the field under consideration, $N\times N$ matrices can be multiplied using $O(N^{c+\varepsilon})$ arithmetic operations for every $\varepsilon>0$. Improvements to $\omega$ are a central benchmark in algebraic complexity because matrix multiplication is also a basic subroutine in linear algebra, graph algorithms, and symbolic computation.
The existing Prove2Me mission formalizes Schönhage's bound $\omega<2.55$ from a concrete two-summand tensor degeneration. The present mission advances the same formal development to the next clean historical construction. Pan and Winograd found a simultaneous approximate algorithm for three matrix products; [Romani recorded its tensor form and the parameter choice $n=11$, $k=5$](https://iris.cnr.it/retrieve/7f08fe3e-3ef4-42b1-b84f-82ba5e09c61a/prod_421763-doc_149822.pdf), which gives $\omega\le 2.5218127\ldots$. [Schönhage's 1981 paper](https://doi.org/10.1137/0210032) reports the equivalent bound $3\log 52/\log 110$ in the arbitrary-field setting. The exact formal target here is the slightly weaker rational inequality $\omega<1261/500=2.522$.
## Setting
For a field $K$, the **matrix-multiplication tensor** $\langle a,b,c\rangle_K$ encodes multiplication of an $a\times b$ matrix by a $b\times c$ matrix:
$$
\langle a,b,c\rangle_K
=\sum_{i<a}\sum_{j<b}\sum_{\ell<c}
e_{ij}\otimes e_{j\ell}\otimes e_{\ell i}.
$$
A direct sum places several such tensors in disjoint coordinate blocks. A tensor $T$ has border rank at most $r$ when it is a polynomial degeneration of the diagonal tensor $I_r=\sum_{s<r}e_s\otimes e_s\otimes e_s$. In the Lean development this relation is `Degenerates T (TensorObj.diagObj K 3 r)`. The argument order matters: the first tensor is the target and the diagonal tensor is the source.
The platform already defines ordinary tensor rank, asymptotic tensor rank, the tensor-rank exponent `matMulExp K`, the equivalent Strassen-preorder exponent `matMulExp_strassen K`, and Schönhage's asymptotic sum inequality. This mission reuses those declarations. No alternative definition of $\omega$ is introduced.
## Formalization targets
The goal has exactly the same quantified proposition as the existing $2.55$ mission, with only the rational endpoint changed:
$$
\forall K\;[\mathrm{Field}(K)],\qquad
\operatorname{matMulExp}(K)<\frac{1261}{500}.
$$
The source construction to be formalized is
$$
\underline R\!\left(
\langle1,5,22\rangle_K\oplus
\langle11,2,5\rangle_K\oplus
\langle10,11,1\rangle_K
\right)\le156.
$$
Each summand has volume $110$:
$$
1\cdot5\cdot22=11\cdot2\cdot5=10\cdot11\cdot1=110.
$$
The milestone chain records the degeneration, its asymptotic-rank consequence, the exact numerical implication
$$
3\cdot110^{\omega^{\mathrm{Str}}_K/3}\le156
\quad\Longrightarrow\quad
\omega^{\mathrm{Str}}_K<\frac{1261}{500},
$$
and the resulting Strassen-form exponent bound. The public goal then transfers the bound to `matMulExp K` through the already established equality of the two exponent definitions.
## Significance
Mathematically, this construction improves the concrete exponent certified by the existing mission from $2.55$ to $2.522$ without changing the surrounding theory. It isolates the first genuinely new ingredient after the accepted Schönhage example: a larger simultaneous tensor degeneration rather than a sharper numerical estimate for the old witness.
For formalization, the mission tests whether the current polynomial-degeneration API can express a historically important trilinear aggregation at realistic scale. Once the explicit witness is available, the remaining declarations form a reusable template for later bounds: a source tensor degeneration, an asymptotic-rank bound, a specialization of the asymptotic sum inequality, and a final exponent transfer. This creates a trustworthy stepping stone toward the Coppersmith--Winograd tensor and later laser-method analyses.
The $2.522$ theorem is known mathematically; the open work is its machine-checked Lean formalization. The exact numerical endpoint and every downstream bridge from the degeneration have already been checked locally. The explicit Pan--Winograd degeneration remains the substantive open milestone.
## Difficulty
The central difficulty is not the logarithmic comparison. It is constructing and verifying the polynomial family whose leading nonzero coefficient is exactly the tagged direct sum of the three matrix-multiplication tensors and whose earlier coefficients vanish. The family has $156$ diagonal source slots and many indexed target coordinates. A proof must account for all mixed-coordinate terms and all cancellations uniformly over an arbitrary field.
[Romani's published summary](https://iris.cnr.it/retrieve/7f08fe3e-3ef4-42b1-b84f-82ba5e09c61a/prod_421763-doc_149822.pdf) states the approximate-rank inequality but does not spell out a Lean-ready map between its trilinear forms and the platform's `TensorObj.bigAdd` coordinate spaces. A solver must therefore recover the source indexing carefully and prove that the resulting modewise linear maps have the required coefficients. Reversing the degeneration direction, conflating tensor rank with asymptotic rank, or silently assuming a characteristic-zero scalar identity would invalidate the result.
## Formalization scope
All theorems quantify over an arbitrary type $K$ with `[Field K]`, matching the existing Schönhage goal and the arbitrary-field statement of the source bound. Tensor spaces are finite-dimensional function spaces already packaged by `MMObj`; the three products are combined with `TensorObj.bigAdd`. Border rank is represented by the existing finitely supported polynomial-family predicate `Degenerates`. Because the source summary specifies approximate rank but not a leading order, the main degeneration milestone existentially quantifies that order instead of hard-coding one.
The mission includes no placeholder laser-value definition and makes no claim about the later $2.376$ analysis. It also excludes Schönhage's additional microscopic symmetrization improvement beyond $3\log52/\log110$. A valid solution must construct the stated degeneration itself; a vacuous hypothesis or a redefinition of `matMulExp` is outside scope.
Reusable contributions include coefficient lemmas for polynomial tensor families, finite-index equivalences for direct sums, and generic aggregation identities that specialize to the $n=11$, $k=5$ witness. Contributions that merely restate the target under stronger field hypotheses do not close the arbitrary-field milestone.
## Selected references
- A. Schönhage, *Partial and Total Matrix Multiplication*, SIAM Journal on Computing 10(3), 1981, pp. 434--455. [DOI 10.1137/0210032](https://doi.org/10.1137/0210032).
- Francesco Romani, *Some Properties of Disjoint Sums of Tensors Related to Matrix Multiplication*, CNR Nota Interna B80-4, February 1980, printed p. 6; journal version, SIAM Journal on Computing 11(2), 1982. [Archived preprint](https://iris.cnr.it/retrieve/7f08fe3e-3ef4-42b1-b84f-82ba5e09c61a/prod_421763-doc_149822.pdf) and [DOI 10.1137/0211020](https://doi.org/10.1137/0211020).
- Avi Wigderson and Jeroen Zuiddam, *Asymptotic Spectra: Theory, Applications and Extensions*, 2023, for the tensor-preorder and asymptotic-rank framework reused by the Lean development. [Author manuscript](https://www.math.ias.edu/~avi/PUBLICATIONS/WigdersonZu_Final_Draft_Oct2023.pdf).
25 thms3 active usersReviewed
🏆Completed
Captain: wurtle
Generalization of Hinging PlanesResearch Paper
A continuous piecewise linear (CPWL) function is one assembled from finitely many flat pieces glued along flat seams. Every ReLU network computes such a function, and every such function is computed by some ReLU network. Questions about how deep a network must be are therefore questions about the internal structure of CPWL functions.
In 1993 Breiman built such functions from hinges: maxima of two affine maps. Sums of hinges approximate anything, but from two dimensions up they fail to represent most CPWL functions exactly. Wang and Sun (2005) widened the maxima, proving that every CPWL function on ℝⁿ is a signed sum of maxima of at most n+1 affine maps. Twenty years on it remains the workhorse structural fact, reducing any question about a network to a question about a single max gate and underpinning every known upper bound on the depth of exact representation.
That includes the newest one: at STOC 2026, Bakaev et al disproved the short standing conjecture that ⌈log₂(n+1)⌉ hidden layers are necessary, showing ⌈log₃(n−1)⌉+1 suffice. In this mission we deliver a machine-checked proof of the Wang and Sun theorem so future formalizations of network expressivity can invoke it rather than reprove it. Note that we take as given the lattice representation of Tarela and Martínez, independently proved by Ovchinnikov, which writes any CPWL function as a max of mins of its affine pieces. That is the one external ingredient the argument consumes, and our definition of CPWL builds it in.
3 thms3 active users
🏆Completed
Captain: joe
The Sipser–Gács–Lautemann TheoremResearch Paper
Randomness appears to enlarge efficient computation, but the Sipser–Gács–Lautemann theorem places every bounded-error probabilistic polynomial-time language at the second level of the polynomial hierarchy, giving one of complexity theory’s foundational limits on the power of randomization.
55 thms3 active usersReviewed
🏆Completed
Captain: marwahaha
Asymmetric Hashing Square Bound: omega < 2.3747Research Paper
AI generated, I think it's correct
## Motivation
The **matrix-multiplication exponent** measures the asymptotic arithmetic cost of multiplying square matrices. A bound $\omega<c$ means that, over the field under consideration, $n\times n$ matrices can be multiplied in $O(n^{c+\varepsilon})$ field operations for every $\varepsilon>0$. Matrix multiplication is a central benchmark in algebraic complexity and a basic subroutine in linear algebra, graph algorithms, and symbolic computation.
The Coppersmith--Winograd tensor and the laser method produced the strongest bounds on $\omega$ for several decades. The 1990 tensor-square analysis gave $\omega<2.375477$. Later analyses of larger powers improved the numerical bound, but they organized their recursion through values assigned independently to constituent tensors. Duan, Wu, and Zhou identified a loss in that organization: several fine constituents that can coexist inside one coarse block may be counted as though they had to be selected independently. Their asymmetric-hashing framework partially compensates for this **combination loss**. The paper's full second-power specialization improves the best bound obtainable from the square of the Coppersmith--Winograd tensor to $\omega<2.374631$; see Section 6.3 and its parameter Table 2 in [Duan--Wu--Zhou](https://arxiv.org/abs/2210.10173).
This mission isolates that second-power result. It is smaller than the paper's record-setting eighth-power calculation, but it contains the genuinely new asymmetric-hashing and hole-repair mechanisms in their first complete form. It therefore provides a focused bridge from the existing formalization of the classical $2.375477$ square analysis to later combination-loss methods.
## Setting
For a field $K$, the **matrix-multiplication tensor**
$$
\langle a,b,c\rangle_K
=\sum_{i<a}\sum_{j<b}\sum_{k<c}
x_{ij}\otimes y_{jk}\otimes z_{ki}
$$
encodes multiplication of an $a\times b$ matrix by a $b\times c$ matrix. A restriction applies one linear map to each tensor leg, while a degeneration permits polynomial families of such maps and takes their first nonzero coefficient. A degeneration from the diagonal tensor $I_r$ gives a border-rank upper bound of $r$.
The **Coppersmith--Winograd tensor** with parameter $q$ is
$$
CW_q=
\sum_{i=1}^{q}
(x_i y_i z_0+x_i y_0z_i+x_0y_i z_i)
+x_0y_0z_{q+1}+x_0y_{q+1}z_0+x_{q+1}y_0z_0.
$$
It has border rank at most $q+2$. Its coordinate partition has six supported types, and the square $CW_q^{\otimes2}$ has fifteen coarse constituent types $(i,j,k)$ with $i+j+k=4$. A large tensor power contains many blocks with prescribed joint and marginal type distributions. The **laser method** retains blocks whose variables are disjoint and interprets their direct sum through Schönhage's asymptotic sum inequality.
Duan--Wu--Zhou refine this organization by also retaining a split distribution for the fine indices inside each coarse constituent. Coarse $X$- and $Y$-blocks are made unique, while compatible coarse triples may initially share a $Z$-block. The resulting partially damaged constituent tensors are described as broken copies of a standard-form tensor. The formal target uses $q=6$, the full Section 6 construction, and the paper's released second-power parameters.
## Formalization targets
### Goal: the full second-power asymmetric-hashing bound
For every field $K$,
$$
\operatorname{matMulExp}(K)<\frac{23747}{10000}=2.3747.
$$
The source reports the stronger numerical endpoint $2.374631$, so the displayed rational inequality has strict slack. The Lean declaration has exactly the same field quantification and uses exactly the same `matMulExp` definition as the existing Coppersmith--Winograd $2.376$ mission; only the theorem name and rational endpoint change.
### Source-level milestones
The mission first isolates the available-block shuffling interface extracted from Definitions 5.3--5.5 and Claims 5.8--5.10, then formalizes the finite covering core of the Hole Lemma 5.6. The subsequent tensor realization by zeroing and identification, the multiple-copy Corollary 5.11, the compatibility-rate identity of Lemma 6.7, the probabilistic part of Claim 6.8, and the global restricted-splitting value inequality in Equation (25) remain visible structural leaves rather than being hidden inside scalar assumptions. The numerical milestone instantiates Equation (25) with the exact $q=6$ data of Section 6.3 and Table 2 and checks a strict value surplus at $\tau=23747/30000$. The structural proof must also make explicit the conversion from the paper's six-symmetrized value to a direct `HasTauValueAtLeast` witness for the mode-symmetric CW square. The final bridge applies the existing tau-value/rank machinery and transfers the Strassen-preorder exponent bound to `matMulExp`.
## Significance
The mathematical result gives the first improvement over the classical Coppersmith--Winograd number while continuing to use only the tensor square. It separates improvement of the tensor analysis from improvement obtained merely by moving to a much higher tensor power. The same standard-form and restricted-splitting language is then reused by the paper's higher-power algorithm, which reports $\omega<2.371866$.
For formalization, the mission adds reusable infrastructure for nested tensor partitions. Existing CW-square work records coarse support types and actual matrix-multiplication restrictions. This mission extends that layer with fine split distributions, compatibility between levels, broken-block bookkeeping, and repair of holes without replacing tensor statements by unverified scalar values. Those definitions are prerequisites for later asymmetric-hashing, complete-split, and more-asymmetry analyses.
The bound is known mathematically and was published at FOCS 2023. The open work is a machine-checked reconstruction. The underlying CW tensor, border-rank certificate, canonical tensor-square grading, Salem--Spencer sets, direct-sum tau-value notion, asymptotic sum inequality, and exponent equivalence already exist on Prove2Me. The new frontier is the cross-level combination-loss analysis and its exact numerical specialization.
## Difficulty
The central difficulty is that coarse and fine decompositions cannot be optimized independently. Two coarse triples may share a $Z$-block, and a fine $Z$-block can be useful for one triple, compatible with several, or removed by a collision. Counting all locally valuable fine constituents therefore does not certify a direct sum. Conversely, requiring every coarse $Z$-block to be unique discards precisely the combinations that produce the improvement.
The Hole Lemma must also preserve the actual tensor. A broken copy lacks some fine variable blocks; combining several such copies is useful only when a degeneration covers every required block with controlled loss and does not duplicate monomials. On the numerical side, the same-marginal maximum-entropy term and restricted-splitting values must be bounded with certified real inequalities. Floating-point output from MATLAB is evidence for a witness, not a Lean proof.
## Formalization scope
The mission uses the existing `TensorObj`, `MMObj`, restriction, degeneration, asymptotic-rank, `HasTauValueAtLeast`, `matMulExp_strassen`, and `matMulExp` declarations in environment `777aaa61dcd2a1258d2b4962dbe983ede4d23b2e`. Top-level results quantify over an arbitrary field. Finite supports and block indices are represented by finite types; probability and split distributions are nonnegative real functions of total mass one; entropy and numerical optimization live in the reals.
The formalization is restricted to $CW_6^{\otimes2}$ for the capstone, although generic definitions and source lemmas may quantify over levels and finite index types. A valid proof must connect scalar rate inequalities to witnessed restrictions or degenerations yielding direct sums of concrete matrix-multiplication tensors. A constant-valued surrogate for the restricted-splitting value, a hypothesis that already assumes the desired exponent bound, or a certificate definition containing its own conclusion is outside scope.
Contributions are welcome for standard-form tensor encodings, finite permutation arguments, hole repair, type and split counting, entropy maximization certificates, certified logarithm and power inequalities, and the final tau-value/rank assembly. Statements should identify the corresponding definition, lemma, claim, equation, or table in the source.
## Selected references
- Ran Duan, Hongxun Wu, and Renfei Zhou, *Faster Matrix Multiplication via Asymmetric Hashing*, 64th IEEE Symposium on Foundations of Computer Science (FOCS), 2023. [arXiv:2210.10173](https://arxiv.org/abs/2210.10173) and [released verification code](https://osf.io/dta6p/).
- Don Cop persmith 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](https://doi.org/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](https://doi.org/10.1137/0210032).
123 thms2 active usersReviewed
🏆Completed
Captain: wenxinzhang
Primal-Dual Online Load Balancing on Unrelated MachinesTextbook
## The model
Fix $m \ge 1$ **machines** and $n$ **jobs** arriving one at a time in the order $0, \dots, n-1$. Job $i$ carries a whole vector of nonnegative **loads** $\tilde p(i,j)$, one per machine, with no assumed relationship between the entries — the same job may be cheap on one machine and unplaceable on another. This is the **unrelated machines** model. When job $i$ arrives its load vector becomes visible, and the algorithm must commit it to a single machine immediately and **irrevocably**, knowing nothing about the jobs still to come. A machine's load is the sum of $\tilde p(i,j)$ over the jobs assigned to it.
The setting formalized here is one **normalized phase**: loads are already scaled by a guessed makespan, so machine $j$ counts as **eligible** for job $i$ exactly when $\tilde p(i,j) \le 1$. The phase is allowed to give up rather than assign badly — it **fails** if an arriving job has no eligible machine, or if an internal weight grows past $1$.
## The algorithm and the guarantee
The algorithm keeps a **weight** $x(j)$ per machine, initialized to $1/(2m)$. Job $i$ goes to the eligible machine $\ell$ minimizing $\tilde p(i,\ell)\, x(\ell)$; that machine's weight is then scaled by $1 + \tilde p(i,\ell)/2$, so a machine becomes exponentially unattractive as it fills. The weights are the primal variables of the covering LP
$$\min \sum_j x(j) + \sum_i z(i) \quad \text{s.t.} \quad \tilde p(i,j)\,x(j) + z(i) \ge 1 \ \text{ for every eligible pair } (i,j),$$
and each assignment raises one dual variable $y(i,\ell)$ to $1$. The guarantee follows from weak duality rather than a bespoke potential argument, which is the point of the primal-dual method.
The goal theorem states that if the dual admits a feasible solution putting unit total mass on every job — the certificate that the guessed makespan was large enough — then the phase does not fail, every job is assigned, and every machine ends with load
$$\sum_{i \,\text{assigned to}\, j} \tilde p(i,j) \ \le\ \frac{\ln(3m)}{\ln(3/2)}.$$
The source states this as $O(\log m)$; the explicit constant is what its proof yields.
Note that the load bound alone is not the theorem: it holds vacuously when the phase assigns nothing, and the milestones state it that way deliberately. The content is the conjunction of *succeeded*, *assigns all*, and the bound.
## Scope
The **doubling wrapper** — guess a makespan, run a phase, double the guess and restart on failure — is what turns this phase into an $O(\log m)$-competitive online algorithm. It is outside this mission; the guarantee proved here is the conditional single-phase statement. The milestones break the argument into weak duality for finite LPs, the load bound, primal feasibility at each prefix, the primal objective identity, and the failure certificate.
## Source
Niv Buchbinder and Joseph (Seffi) Naor, *The Design of Competitive Online Algorithms via a Primal-Dual Approach*, Foundations and Trends in Theoretical Computer Science 3(2–3), 2009, Chapter 8, pp. 193–196 (Theorem 8.1). [PDF](https://www.tau.ac.il/~nivb/download/pd-survey.pdf) · [doi:10.1561/0400000024](https://doi.org/10.1561/0400000024)
10 thms2 active usersReviewed
🏆Completed
Captain: marwahaha
Sensitivity ConjectureResearch Paper
Nearly every measure of Boolean function complexity was known to be equivalent — except sensitivity. Proving the conjecture unified the whole picture.
44 thms2 active usersReviewed
🏆Completed
Captain: ShouqiaoWang
Erdős Problem 788: Exponent One-Half and Explicit BoundsResearch Paper
Erdős Problem 788 asks how large a set can always be retained when prescribed distinct pair-sums are forbidden. This mission formalizes the repository’s strengthened version of Theorem 1.1: an explicit lower bound valid for every $n\ge 3$, an eventual quantitative upper bound, the conclusion $f(n)=n^{1/2+o(1)}$, and the exact affirmative answer to the original upper-bound question.
6 thms1 active userReviewed
🏆Completed
Captain: intro_user0735
Schönhage's Bound: omega < 2.55Research Paper
Prove Schönhage's 1981 bound that the matrix-multiplication exponent satisfies omega < 51/20, via the tau theorem and the asymptotic sum inequality.