The TCS Formalization Drive

3SUM asks whether three distinct positions in an integer array hold values summing to zero. This mission imports Jionghan Wang's sharper weighted-cache refinement into the 3SUM Exponent campaign, improving the previously published exponent $1.92027942$ to $1.920279408185$.

Many learning problems take a set as input rather than a vector: a point cloud, the collection of words in a document, a group of users in an audience, a sample from a distribution. A model for such data must give the same answer however the elements of the set are listed. Deep Sets (Zaheer, Kottur, Ravanbakhsh, Póczos, Salakhutdinov, Smola,…

Online bipartite matching, introduced by Karp, Vazirani and Vazirani (1990), models a platform that must assign arriving customers to a known stock of items, one customer at a time and irrevocably. In e-commerce, job search and online advertising, a recommendation is only a suggestion: a customer buys an offered item with some known probability, and after…

A proof assistant based on type theory has to reject non-terminating definitions: a function that loops can inhabit any type, including the empty one, and so proves everything. Agda therefore checks every recursive definition for termination before accepting it. Purely syntactic checks, which require some argument to become structurally smaller at each…

Maximizing a set function is a basic task in combinatorial optimization and algorithmic game theory. Computing an agent's demand under prices $p$ amounts to maximizing $v(X)-\sum_{x\in X}p_x$, which need not be monotone even when the valuation $v$ is. XOS functions generalize submodular functions, and they are studied in combinatorial auctions, where they are…

Eyal and Sirer (2014) showed that a mining pool can earn more than its share of the hashrate by withholding blocks: the pool's revenue share under the selfish strategy exceeds $\alpha$ exactly when $\alpha > (1-\gamma)/(3-2\gamma)$, where $\gamma$ is the fraction of honest hashrate that mines on the pool's block during a tie. The result is usually quoted as…

When a faster multiplication algorithm becomes available, its consequences depend on which problems reduce to multiplication and how the reduction changes input size. A displayed runtime bound alone does not identify this connection. The surrounding computation can also consume the improvement if its cost is omitted or underestimated.

The 3SUM problem — does an integer array contain three values, at three distinct positions, that sum to zero — is a canonical benchmark of fine-grained complexity. Hundreds of reductions sit beneath it in the 3SUM-hardness lattice, so its worst-case exponent governs the reported complexity of convex-hull degeneracies, motion planning, and many…

A data structure can hide each stored share individually while revealing their joint value through its visible layout. This distinction matters when a ledger publishes both a collection of shares and the markers identifying which cells were filled by genuine insertions. The GBFPlus protocol records cross-domain transfers in ledger attestations and uses a…

In many sequential decision problems an unknown quantity is revealed only when paid for: a medical test, a sensor reading, a database query. Stochastic submodular cover is the common abstraction: items are probed one at a time at a cost, each probe reveals a random outcome, and probing stops once the revealed outcomes jointly reach a coverage target. It…

Directed network design asks which connections can be bought under a limited budget when traffic follows the directions of arcs. In directed tree orienteering, the reward comes from vertices reached by a rooted directed tree. The submodular version allows the reward of a new vertex to depend on which vertices have already been reached. This captures…

Scheduling independent jobs on machines that run at different speeds, so that the last job finishes as early as possible, is one of the basic problems of scheduling theory. In the classification of Graham, Lawler, Lenstra and Rinnooy Kan it is denoted $Q\|C_{\max}$, the minimum makespan problem on uniform parallel machines. It is strongly NP-hard, so the…

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