The TCS Formalization Drive

Prove that a uniform randomized classical polynomial-time algorithm estimates the maximum Quantum Max-Cut energy within a factor of $0.614$ on every graph with nonnegative rational edge weights.

This completed mission proves a deterministic classical polynomial-time $1/2$ approximation to the Quantum Max-Cut optimum. Compute total edge weight $W$ and a greedy maximum-edge matching of weight $g$, then return the exact rational estimate $v=(W+3g)/2$.

This completed mission proves existence of a classical polynomial-time numerical $0.498$ approximation to Quantum Max-Cut. Every returned rational estimate is at most the unrestricted optimum, and its expectation is at least $0.498\,\mathrm{OPT}(G)$.

This completed foundation proves a deterministic classical polynomial-time numerical estimator for Quantum Max-Cut. If $W$ is total edge weight, the algorithm returns the exact rational $v=W/2$.

Quantum Max-Cut is an optimization problem for a system of interacting qubits. An input graph specifies which pairs interact and the nonnegative weight of each interaction. The task is to prepare a quantum state with high energy relative to the maximum permitted by quantum mechanics. This makes approximation algorithms a way to compare feasible state…

The selfish-mining mission took the stationary distribution of Eyal and Sirer's equation (7) as a definition and proved it is invariant with total mass 1. That leaves a gap a careful reader will point out: the revenue analysis is only meaningful if the chain has no other stationary distribution. This mission closes it: every nonnegative, lead-summable,…

"Bitcoin is secure as long as honest miners hold the majority of the hashrate" is the informal reading of Garay, Kiayias and Leonardos's backbone analysis: in a synchronous network, if the adversary finds fewer blocks than there are uniquely successful honest rounds over every long enough window, then honest chains grow (chain growth), agree on all but…

Hardness of the closest vector problem, 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.

Arithmetic formula lower bounds for the permanent, 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.

Binary and spherical codes, 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.

In a two-player one-round nonlocal game, a verifier samples a pair of questions, sends one to each of two players who cannot communicate, and accepts or rejects the pair of answers. The players may share an arbitrary quantum state and measure it; the entangled value of the game is the supremum of their acceptance probability over all such strategies.…

Prove2Me mission category: Textbook.

Prove2Me mission category: Textbook.

Prove2Me mission category: Textbook.

Prove2Me mission category: Textbook.

Sampling an entire finite-state execution is a different computational task from recognizing a supplied word. A membership circuit must answer correctly on its given input. A sampler instead chooses the input together with its associated output, while preserving their joint distribution. This distinction is relevant when finite-state models describe…

A set of unit-length jobs with precedence constraints is to be run on a fixed number of identical machines so that all jobs finish as early as possible. For two machines this was solved in 1969–1972; for a number of machines given as part of the input the problem is NP-complete (Ullman, 1975). Whether the problem is polynomial-time solvable for three machine…

Multiplying matrices is a basic operation whose asymptotic cost is measured by the number of scalar arithmetic operations needed as the matrix dimensions increase. The familiar entry-by-entry algorithm has cubic cost. The question addressed here is how small an exponent can describe exact multiplication of square matrices when algorithms may use more…

Status: complete. This mission records a finished formalization rather than an open call for work. Every statement below, including the goal, was uploaded together with a proof that the platform has verified, so there is nothing left to prove.

All-pairs shortest paths (APSP) computes the shortest distance between every pair of vertices in a weighted graph.