The TCS Formalization Drive

Posted prices turn an offline allocation problem into a sequential choice process: each agent sees a menu of outcomes and prices, then chooses an outcome without revealing its full valuation. The balanced prices framework of Dütting, Feldman, Kesselheim, and Lucier gives welfare guarantees by comparing the revenue collected from an allocation with the…

Least-squares regression, $\min_X\|AX-B\|_F$ for a tall matrix $A\in\mathbb R^{n\times d}$ with $n\gg d$, is among the most frequently solved problems in numerical computation. Direct methods (QR or SVD) cost $O(nd^2)$ time, which is prohibitive when $n$ is in the millions. Sketching replaces the problem by a much smaller one: choose a matrix $S\in\mathbb R^{t\times n}$…

The paper of Bodlaender, Drange, Dregi, Fomin, Lokshtanov and Pilipczuk (2016) has an algorithmic headline. This mission concerns one of its finite graph lemmas, Lemma 2.9. The lemma translates a condition phrased separately for every connected component into a condition on three vertex sets. A reader of graph decompositions encounters both forms:…

Multivariate multipoint evaluation asks for the values $f(\alpha_0), \dots, f(\alpha_{N-1})$ of one polynomial $f \in \mathbb F_q[X_0, \dots, X_{m-1}]$ at $N$ points of $\mathbb F_q^m$. Kedlaya and Umans showed that this problem is equivalent to modular composition, the computation of $f(g(X)) \bmod h(X)$ for univariate polynomials, and that fast algorithms for it…

Multivariate multipoint evaluation asks for the values $f(\alpha_0),\dots,f(\alpha_{N-1})$ of a polynomial $f(X_0,\dots,X_{m-1})$ over a ring $R$, with individual degrees at most $d-1$, at $N$ given points of $R^m$. Kedlaya and Umans showed that, over finite fields and rings $(\mathbb Z/r\mathbb Z)[Z]/(E(Z))$, this problem can be solved in time nearly linear in the input…

Online covering models decisions that must be made as requirements arrive. A planner knows the cost of each available resource, but learns the requirements one at a time and cannot undo an allocation already made. This occurs, for example, when requests for network service or elements needing coverage appear over time. The central question is how much more…

Treewidth measures how closely a graph resembles a tree. Bodlaender, Drange, Dregi, Fomin, Lokshtanov and Pilipczuk (SIAM J. Comput. 45(2), 2016) study an algorithm for producing tree decompositions. Its headline result is algorithmic; this mission formalizes one combinatorial lemma used in its analysis.

The rank of a matrix does not depend on the field in which its entries are read: a rational matrix has the same rank over $\mathbb Q$, $\mathbb R$ and $\mathbb C$, because rank is computed by Gaussian elimination, which never leaves the field of the entries. For 3-tensors, arrays $\mathcal A = [\![a_{ijk}]\!]$ with three indices, this fails. Tensor rank governs the…

A snark is an uncolourable, cyclically 4-edge-connected cubic graph of girth at least 5: a cubic graph whose edges cannot be properly coloured with three colours, and which is not reducible to a smaller such graph by an elementary operation. Snarks are the critical cases for several of the central conjectures of graph theory, among them the cycle double…

Differential privacy (Dwork, McSherry, Nissim, Smith 2006) asks that a randomized algorithm run on a database behave almost identically whether or not any single record is changed. A central question for data curators is non-interactive release: publish, once, a sanitized object (ideally a synthetic database) from which analysts can answer many statistical…

Differential privacy (Dwork, McSherry, Nissim and Smith 2006) is the standard guarantee for releasing statistics about a sensitive database: replacing one record changes the probability of any outcome by at most a factor $e^{\varepsilon}$. In their paper on non-interactive database privacy, Blum, Ligett and Roth propose an alternative motivated by learning…

All-pairs shortest paths (APSP) asks for the exact distance between every ordered pair of vertices in an $n$-vertex weighted directed graph. Floyd–Warshall solves it in $O(n^3)$ time, and for decades no algorithm beat $n^{3-\delta}$ for any constant $\delta>0$ on graphs with polynomially bounded integer weights. In 2026, Alman and Vassilevska Williams (arXiv:2610.06…

A non-interactive zero-knowledge (NIZK) proof lets a prover convince a verifier that a statement is true by sending a single message, computed from a common reference string $\sigma$ that both parties share, without revealing anything beyond the truth of the statement. NIZK proofs were introduced by Blum, Feldman and Micali (STOC 1988) and are a building…

A prophet inequality compares two players facing the same random sequence of rewards $X_1, X_2, \dots, X_n$. The gambler sees the values one at a time and must decide, as each value arrives, whether to stop and collect it; a value passed over is lost. The prophet knows the whole sequence in advance and simply takes its maximum. In 1978 Krengel, Sucheston and…

In the job shop problem, jobs are sequences of operations, each to be processed on a given machine for a given time, and the goal is a schedule of minimum makespan (the time at which the last job finishes). Two numbers bound the optimum from below: the longest job and the most loaded machine. Their maximum is written $\mathrm{lb}$. The best approximation…

A non-interactive zero-knowledge (NIZK) proof lets a prover convince a verifier that a statement is true by sending a single message, computed from a common reference string $\sigma$ that both parties share, without revealing why the statement is true. NIZK proofs were introduced by Blum, Feldman and Micali (STOC 1988). They are a basic component of…

The effective resistance between two vertices of a weighted graph is the voltage difference that appears between them when the graph is viewed as an electrical network, edge weights being conductances, and one unit of current is injected at one vertex and extracted at the other. Effective resistances drive the spectral sparsification algorithm of Spielman…

Parity, $\mathrm{PARITY}_n(x)=x_1\oplus\cdots\oplus x_n$, is the standard test of whether a shallow circuit can aggregate information from all of its inputs. Classically, constant-depth circuits with unbounded fan-in AND/OR gates ($\mathsf{AC}^0$) cannot compute it: Furst, Saxe and Sipser (Math. Systems Theory 1984) and Ajtai (APAL 1983) proved superpolynomial…

Pure type systems (PTSs) are a uniform framework covering the simply typed λ-calculus, System F, the calculus of constructions and the type theories behind proof assistants such as Coq and Lean. A system is specified by its sorts (like $\ast$ and $\square$), axioms ($\ast:\square$) and product rules (which dependent function types may be formed). Normalization is…

A logic for unordered finite structures (graphs, databases, relational inputs given up to isomorphism) must give answers that do not depend on how the input elements are named. Many polynomial-time algorithms nevertheless make arbitrary intermediate choices, for example the pivot in Gaussian elimination, without changing their final answer. Choiceless…

Descriptive complexity asks whether complexity classes can be characterized by logics, without reference to machines. Immerman and Vardi (1982) showed that on ordered finite structures, first-order logic with a least fixed-point operator expresses exactly the polynomial-time queries. On unordered structures, such as graphs given only up to isomorphism, an…

Add random clauses one at a time to a Boolean formula on $n$ variables until it first becomes unsatisfiable. The index $H_n$ of that first failure is the satisfiability hitting time of random $k$-SAT. Its mean, divided by $n$, converges to the satisfiability threshold; its variance measures the width of the transition window. Friedgut's sharp-threshold theorem…