The TCS Formalization Drive

Randomized load balancing assigns arriving jobs to servers without inspecting every server. Uniformly choosing one destination is inexpensive, but a small number of servers can accumulate substantially more work than the average. Sampling a fixed number of destinations and choosing a least-loaded one provides an alternative with little additional…

A cryptographic key can become unavailable when a single custodian loses it, while distributing complete copies gives every custodian the ability to use it alone. A threshold scheme distributes evaluations of one hidden object so that a sufficiently large coalition can recover a secret and a smaller coalition learns no information from its observations. Adi…

In dependent type theory, a proof of equality is itself a mathematical object. If two objects $a,b:A$ are equal, the identity type $\mathrm{Id}_A(a,b)$ contains the evidence for that equality. A further identity type can express equality between two such proofs. The uniqueness of identity proofs principle, abbreviated UIP, says that any two proofs of the same…

Static resource analysis aims to derive machine-checkable upper bounds on the computational cost of a program without executing it on every input. In Tarjan's potential method (1985), each program state is assigned a nonnegative potential so that the drop in potential across a step pays for both its immediate cost and the potential required by subsequent…

Most conditional lower bounds for polynomial-time problems trace back to one hypothesis about satisfiability. The Strong Exponential Time Hypothesis (SETH) of Impagliazzo and Paturi says that for every $\varepsilon>0$ there is a clause width $k$ for which $k$-SAT on $n$ variables cannot be solved in time $O(2^{(1-\varepsilon)n})$. Quadratic-time problems are seldom…

Retailers, online travel agencies and search engines display products in an ordered list or on a physical layout, and customers inspect only a prefix of it. Display optimization asks how to assign products to positions so as to maximize expected revenue when each customer considers only the products shown in the first $k$ positions, with $k$ random. Aouad and…

Ride-pooling platforms receive trip requests one at a time and must decide, within a short waiting window, which requests to group into a shared vehicle. A request that is not grouped before its window closes is served alone or lost. Online hypergraph matching with delays is the combinatorial core of this decision: requests are vertices that arrive over…

The incremental knapsack problem is a multi-period extension of the binary knapsack problem. Items are inserted over a planning horizon whose capacity grows over time, and an item, once inserted, stays. Sharp (2007) and Hartline (2008) introduced it in their theses on incremental optimization. It models resource allocation in which the available budget…

Agrawal, Kayal, and Saxena's "PRIMES is in P" (Annals of Mathematics 160 (2004) 781-793) settled a question open since the birth of complexity theory: primality has an unconditional, deterministic, polynomial-time test. The paper's algorithm is elementary - six steps: reject perfect powers; fix a small r; reject trivial factor witnesses; accept small…

Capacitated vehicle routing asks how to serve clients from a depot with vehicles that can carry only a limited load. In the unsplittable version, one vehicle must deliver each client's entire demand. This makes the choice of routes interact with bin packing: a short tour can fail because its total demand exceeds the vehicle's capacity. Approximation…

Submodular function minimization asks for a subset $X$ of a finite set $V$ that minimizes a set function $f$ satisfying $f(X) + f(Y) \ge f(X \cup Y) + f(X \cap Y)$. Cut functions, matroid rank functions and entropy are submodular, and minimizing them is a subroutine in dynamic flows, facility location and source coding. Grötschel, Lovász and Schrijver showed in…

The secretary problem asks an online decision maker to pick the best of $n$ candidates who arrive in uniformly random order, deciding irrevocably on each one at arrival. Its matroid generalization, the matroid secretary problem (MSP) of Babaioff, Immorlica and Kleinberg (SODA 2007), asks the algorithm to select an independent set of a matroid whose elements…

Certify the separation exponent $\alpha\ge2.000252407$ using OpenAI's construction. Sensitivity $s(f)$ counts individual bit flips that change the output; block sensitivity $bs(f)$ counts disjoint sensitive blocks. Both are maximized over inputs. The notation $bs(f,x)$ fixes one input, and $0$ denotes the all-zero input.

A firm with $k$ open positions often cannot interview and offer sequentially: hiring seasons are short, and offers go out in one batch. Some recipients decline, so the firm overbooks, sending more offers than it has positions, and pays for every hire beyond capacity. The same trade-off appears in airline and hotel overbooking and in university admissions.…

A firm that fills a fixed number of positions from a pool of applicants faces uncertainty at every stage: applicants differ in value, and an offer may be declined. When offers must go out at once, as in a recruiting season with a common deadline, the firm decides a single offer set and lives with however many candidates accept. Sending too few offers leaves…

Hiring is a pipeline: a firm with $k$ openings and a large pool of applicants cannot interview everyone, so it must decide whom to interview, in what order, and whether to hire on the spot. The ProbeTop-k problem models this. Each applicant has a random value with a known distribution, an interview reveals the value, at most $T$ interviews may be conducted, and…

Two vertices belong to the same strongly connected component when each can reach the other by a directed path. The partition separates the mutually reachable parts of a directed graph without requiring the whole graph to be connected. This mission formalizes the two-pass DFS algorithm of CLRS, fourth edition, Chapter 20, §20.5, often called Kosaraju's…