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