The TCS Formalization Drive

A series system works only if every one of its components works. Deciding whether it works by inspecting components one at a time, in the order that minimizes the expected inspection cost, is the classic sequential testing problem for series systems (Mitten 1960; Butterworth 1972; Simon & Kadane 1975). It is solved by sorting the components by the ratio …

A data center can save energy by running fewer servers when demand is low, but restarting servers costs energy and queued work delays users. A controller must choose capacity while demand arrives, with limited knowledge of future traffic. Forecasts can help, yet an inaccurate forecast can make a controller perform worse than one that ignores it. Rutten and…

In linear regression with a budget, an experimenter holds $n$ candidate experiments, each described by a vector $v_i\in\mathbb R^d$, and may run only $k$ of them. If the experiments in $S\subseteq[n]$ are run and the unknown parameter is estimated by least squares, the covariance of the estimate is proportional to $\big(\sum_{i\in S}v_iv_i^\top\big)^{-1}$. A-optimal…

Many tasks on high-dimensional data ask not for the nearest neighbours of a query but for how many data points lie close to it. Density estimates of this kind feed outlier detection, kernel density estimation, classification by neighbourhood counts, and the tuning of nearest-neighbour search itself. Exact counting needs a scan of the whole dataset for every…

Quantum parallel repetition, from the OpenAI Ten Proofs formalization. The source already contains machine-checked proofs; this mission organizes its headline result and additional Comparator targets for reuse.

Shared computing infrastructure — a data-centre cluster, a cloud platform's memory — is divided among users who arrive over time. Two requirements pull against each other. Proportional fairness asks that, when $t$ users are present, each holds at least a $1/t$ fraction of the resource. Limited disruption asks that the system not take resource away from running…

A polynomial threshold function makes a Boolean decision by evaluating a real polynomial and keeping only its sign. Its average sensitivity measures how often that decision changes after one uniformly chosen input coordinate is reversed, summed over all coordinate choices. This is a basic quantitative question in the analysis of Boolean functions: how much…

Certify the classical quadratic separation between sensitivity and block sensitivity: $\alpha\ge2$.

Many computational tasks produce a real number by running a randomized procedure once, then estimate its expected value by running that procedure repeatedly. The number of repetitions needed for a given additive accuracy depends on the output variance. Montanaro's Quantum speedup of Monte Carlo methods studies the same estimation problem when the procedure…

Firms that hire for several roles at once face a timing problem. An offer occupies a candidate until they answer, a candidate can hold only one offer, and the hiring season has a fixed number of decision rounds. Sending offers one at a time is slow; sending them all at once risks over-hiring. Epstein and Ma (arXiv:2210.04059v3, Operations Research 2024)…

The original exact goal EndStatement.ThreeSum.SolvedInTime 1.960614 is Proved on Prove2Me. All seven original milestones are complete. The complete machine extension has 481 accepted theorem proofs and reuses 110 proved theorem nodes; its accepted dependencies connect to the original main reduction. The independent fixed-model lower bound remains separate…

3SUM asks whether an input sequence contains three entries at different positions whose sum is zero. The classical quadratic running time makes it a benchmark for fine-grained algorithm design: even a small fixed improvement in the exponent changes its asymptotic complexity. The setting here is polynomially bounded integers and a deterministic word RAM; the…

The general number field sieve (GNFS) is the most efficient classical algorithm known for factoring integers larger than about $10^{100}$. Its heuristic running time for an integer $n$ is

This entry records a deterministic $O(n^{1.962})$ bound for 3SUM on polynomially bounded integers, using the campaign's shared word-RAM model with $O(\log n)$-bit words. Three distinct input positions must sum to zero; repeated values are allowed. The exact exponent is $981/500$.

Online stochastic matching models display advertising and similar allocation problems in which requests arrive one at a time and must be served immediately. A bipartite graph links a set $A$ of advertisers to a set $I$ of impression types; $n$ requests arrive, each of a type drawn independently with $\mathbb P(\text{type } i) = r_i/n$, and each request must be…

Helly's theorem says that a finite family of convex sets in $\mathbb R^d$ has a common point whenever every $d+1$ of its members do. Two of its best-known strengthenings weaken the hypothesis in different directions. The colorful Helly theorem, due to Lovász and first published by Bárány (1982), distributes the sets into $d+1$ color classes and only asks that…

Multiparty communication protocols involve several participants who send messages over shared session channels. An implementation may send a later message before an earlier one has been received, so a written sequence of interactions does not by itself prevent a receiver from taking the wrong message. Honda, Yoshida, and Carbone use global types to specify…

A suffix tree of a text $T[1..n]$ answers pattern-matching and string-analysis queries (longest repeats, maximal repeats, matching statistics) in time close to optimal, but it occupies $\Theta(n)$ machine words. For highly repetitive collections, such as many genomes of one species or the versions of a document, this is far more than the information the text…

A text index answers questions about occurrences of a pattern without scanning the whole text. One reason to compress such an index is that many stored texts are repetitive: multiple versions of a document or genome often share long passages. The Burrows–Wheeler transform (BWT) rearranges a text's symbols in a way that groups related contexts. A small…

Collections of genomes, versioned documents and source-code histories are highly repetitive: most of each new item is a copy of something already stored. Full-text indexes such as the suffix array and the FM-index answer pattern queries on such collections, but their size grows with the text length $n$, not with the amount of distinct content. The number $r$ of…