The TCS Formalization Drive

A coordinated effort to formalize the mathematics of theoretical computer science in Lean 4.

Scope: missions in computational complexity, algorithms and optimization, data structures, automata and computability, randomized and approximation algorithms, cryptography, learning theory, information theory, algorithmic game theory, combinatorics, computational geometry, and distributed computing.

582 missions

Missions

51–75 of 582

Completed

Combinatorics Operations Research Probability+1·Captain: mikedeng1

Online Stochastic Matching: Beating 1-1/e 1: When OPT = Ω(n), the Two Suggested Matchings Algorithm Achieves ALG/OPT ≥ (1 − 2/e²)/(4/3 − 2/(3e)) − ε ≈ 0.670 with Probability 1 − e^(−Ω(n))Research Paper

Online bipartite matching models a platform that must commit each arriving request to a resource immediately. The motivating application of Feldman, Mehta, Mirrokni and Muthukrishnan is display advertising: an ad server knows from past traffic how many impressions of each type (web page, audience segment) to expect, sells them to advertisers in advance, and…

28 thms5 active users

Completed

Theoretical Computer Science·Captain: wurtle

CLIQUE is NP-CompleteResearch Paper

Prove that CLIQUE is NP-complete by reducing the existing 3-SAT language, KSat.KSAT 3, to it. An instance consists of a finite simple undirected graph and an input threshold; it asks whether the graph contains a clique of at least that size. (https://prove2.me/theorems/d82e8682-c490-4742-a5e5-dd3a0b870b90). The construction specializes Karp’s SAT-to-CLIQUE…

81 thms5 active usersReviewed

Completed

Combinatorics Graph Theory Theoretical Computer Science·Captain: mikedeng1

Eigenvalues and Expanders: A Regular Bipartite Graph Is a Strong Expander If and Only If λ(G) Is Bounded Away from 0Research Paper

Expander graphs are sparse graphs in which every set of vertices has many neighbours. Families of them with bounded degree and expansion bounded away from zero are a basic tool of theoretical computer science: they are the main component of the sorting network of Ajtai, Komlós and Szemerédi (AKS 1983), the building block of superconcentrators and other…

16 thms5 active usersReviewed

Completed

Linear Optimization Operations Research Optimization+1·Captain: mikedeng1

A Dynamic Near-Optimal Algorithm for Online Linear Programming I: The Competitive Ratio of the Dynamic Learning AlgorithmResearch Paper

Many resource-allocation problems are decided one request at a time: a seller of airline seats or hotel nights, an ad platform allocating advertiser budgets, a network operator admitting bandwidth requests. Each request asks for a bundle of resources and offers a price. It must be accepted or rejected on arrival, before the later requests are seen. The onlin…

13 thms5 active usersReviewed

Completed

Linear Optimization Operations Research Probability+1·Captain: mikedeng1

Competitive Randomized Algorithms for Nonuniform Problems III: The Optimal Randomized Two-Server Ratio on the 1-d-d Isosceles TriangleResearch Paper

The k-server problem of Manasse, McGeoch and Sleator (J. Algorithms 11 (1990)) asks how $k$ mobile servers in a metric space should respond, on-line, to a sequence of requests at points of the space, each of which must be covered by a server. It is the central model of on-line computation: paging is the special case of a uniform metric, and many caching and…

9 thms5 active usersReviewed

Completed

Theoretical Computer Science·Captain: xuanji

AlphaEvolve Eighth-Power Bound: omega < 2.371177Research Paper

Formalize $\omega < 2.371177$ , the current record from Dupont, Eisenberger, Kozlovskii, Mehrabian, Ruiz, See, Zhou, Alman, Vassilevska Williams and Balog (arXiv:2608.16884, August 2026).

9 thms5 active usersReviewed

Completed

Combinatorics Operations Research Theoretical Computer Science·Captain: mikedeng1

Competitive Paging Algorithms IV: An Algorithm Competitive against Several Others Exists iff the Reciprocal Ratios Sum to at Most 1Research Paper

Paging is the problem of managing a fast memory that holds $k$ pages out of $n$ : when a requested page is not in fast memory (a page fault), some resident page must be evicted, and the cost of an algorithm is its number of faults. Practitioners have many eviction rules. Least-recently-used (LRU) performs well on real workloads but can be $k$ times worse than the…

9 thms5 active usersReviewed

Computational Geometry Linear Optimization Operations Research+1·Captain: mikedeng1

Linear Programming in Linear Time When the Dimension Is Fixed: Fixed-Dimension LP Feasibility Decided in Linear Time on the Real RAMResearch Paper

A linear program asks for a point $x\in\mathbb{R}^d$ minimizing $c^Tx$ subject to $n$ linear inequalities $\sum_{j=1}^d a_{ij}x_j\ge b_i$ . Many problems in computational geometry and statistics are linear programs with few variables and very many constraints: separating two point sets by a line or plane, fitting a line in the Chebyshev ( $L_\infty$ ) norm, finding the…

16 thms5 active usersReviewed

Completed

Operations Research Theoretical Computer Science·Captain: mikedeng1

The Design of Competitive Online Algorithms via a Primal-Dual Approach VIII: The Bounded Allocation ProblemTextbook

The classical online allocation (AdWords) problem has a tight 1 - 1/e competitive ratio in general, achieved by the water-level algorithm and matched by a lower bound in which the number of buyers interested in each item can be as large as the total number of buyers. Buchbinder and Naor's Chapter 13 observes that in many realistic settings each item's…

16 thms5 active users

Completed

Machine Learning Probability Statistics+1·Captain: mikedeng1

Foundations of Machine Learning XII: Algorithmic StabilityTextbook

Every generalization bound in Chapters 2-11 depends only on the complexity of a fixed hypothesis set $H$ — Rademacher complexity, VC-dimension, growth function — and holds regardless of which algorithm within $H$ actually returns the hypothesis. This is both a strength (broad applicability) and a limitation: it throws away everything specific to how an…

12 thms5 active users

Completed

Machine Learning Probability Statistics+1·Captain: mikedeng1

Foundations of Machine Learning V: Kernel Methods and the Representer TheoremTextbook

Linear methods like SVMs work only when the classes are linearly separable, but most real data is not. Chapter 6 shows how to get non-linear decision boundaries for free: replace the input space's inner product with a kernel $K$ that implicitly computes an inner product in a (possibly very high- or infinite-dimensional) feature space, without ever explicitly…

7 thms5 active usersReviewed

Completed

Theoretical Computer Science·Captain: marwahaha

Coppersmith–Winograd Bound: omega < 2.376Research Paper

AI generated but i think correct. I think the milestones make it really annoying but the central theorem looks correct.

72 thms5 active usersReviewed

Algorithmic Game Theory Complexity Theory Operations Research·Captain: iris

Pure Nash Equilibria: Hard and Easy Games: Deciding Whether a Game Has a Pure Nash Equilibrium Is NP-Complete, Even for Graphical Games with 3-Bounded Neighborhood and Three ActionsResearch Paper

A pure Nash equilibrium is a choice of one action per player from which no player can gain by changing only her own action. Unlike mixed equilibria, which exist in every finite game by Nash's theorem, pure equilibria may fail to exist, so deciding whether one exists is a basic algorithmic question about any game model. It matters most for games with many…

30 thms4 active usersReviewed

Completed

Quantum Information·Captain: marwahaha

Quantum Max-Cut: $0.526$ energy estimationResearch Paper

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

47 thms4 active usersReviewed

Completed

Quantum Information·Captain: marwahaha

Classical 0.53 energy estimation for Quantum Max-CutResearch Paper

Quantum Max-Cut asks for the largest eigenvalue of $H_G=\sum_{i<j}w_{ij}(I-\mathrm{SWAP}_{ij})$ on a graph with nonnegative rational weights. This mission formalizes the classical numerical $0.53$ approximation target motivated by Anshu, Gosset, and Morenz's published TQC 2020 Theorem 3.

54 thms4 active usersReviewed

Algorithmic Game Theory Computational Complexity Economics+1·Captain: iris

The Complexity of Pacing for Second-Price Auctions: Finding an Approximate Pacing Equilibrium Is PPAD-HardResearch Paper

Online advertising platforms sell billions of impressions through auctions, and most advertisers face a budget for a whole campaign rather than for a single auction. Ad platforms handle this with budget pacing: each advertiser's bids are scaled down by a multiplier so that spending tracks the budget. When every advertiser paces at once, the multipliers…

26 thms4 active usersReviewed

Complexity Theory Operations Research Optimization·Captain: iris

Serial batching to minimize the weighted number of tardy jobs: W[1]-hardness for #d + #p and for #p + #r, with XP algorithms for #d + #p + #w and for #p + #r + #wResearch Paper

In manufacturing, items move between facilities in boxes, pallets or carts, and everything placed in one container leaves together. Serial batch scheduling models this: a single machine processes jobs in batches, each batch costs a fixed setup time plus the processing times of its jobs, and all jobs of a batch complete together. Minimizing the weighted…

30 thms4 active usersReviewed

Combinatorics Convex Optimization Operations Research+1·Captain: iris

Geometric Rescaling Algorithms for Submodular Function Minimization: Rescaling-SFM finds a minimizer of an integer-valued submodular function in $O((n^4\cdot\mathrm{EO}+n^5)\log(nL))$ timeResearch Paper

A set function $f : 2^V \to \mathbb{R}$ on a finite set $V$ is submodular if $f(X) + f(Y) \ge f(X \cup Y) + f(X \cap Y)$ for all $X, Y \subseteq V$ . Submodular function minimization (SFM) asks for a set minimizing $f$ when $f$ is available only through a value oracle of cost $\mathrm{EO}$ . Minimum cut, matroid intersection and several scheduling and image-segmentation…

55 thms4 active usersReviewed

Complexity Theory Operations Research Optimization·Captain: iris

The Complexity of Recognizing Facets for the Knapsack Polytope: Deciding Whether an Integer Inequality Defines a Facet of a Knapsack Polytope Is Dᵖ-CompleteResearch Paper

Integer programs are solved in practice by adding valid inequalities to a linear relaxation, and the strongest valid inequalities are the facet-defining ones. Knapsack polytopes are a central case: every row of a binary integer program defines one, and cuts derived from individual knapsack rows (lifted cover inequalities and their relatives) are part of…

30 thms4 active usersReviewed

Completed

Combinatorics Graph Theory Optimization·Captain: iris

Finding Hall Blockers by Matrix Scaling: without a perfect matching, (1/4)n² log(mA_max/A_min) Sinkhorn iterations and a sort of the scaling vectors output a Hall blockerResearch Paper

Matrix scaling asks for positive diagonal matrices that turn a nonnegative matrix into one with prescribed row and column sums. The Sinkhorn algorithm, which alternately normalizes rows and columns, is the standard method; it appears in statistics (iterative proportional fitting), entropic optimal transport, and combinatorial optimization. For the doubly…

16 thms4 active usersReviewed

Combinatorics Complexity Theory·Captain: Shuze Chen

Hard Tiling Problems with Simple Tiles: Decision and counting completeness for right trominoes and square tetrominoesResearch Paper

A tiling problem asks whether copies of a few shapes can cover a specified region without overlap or gaps. Even when the shapes are small and fixed in advance, the region can encode a substantial combinatorial constraint. This makes tiling a useful setting for distinguishing local geometric simplicity from computational tractability. It also separates two…

11 thms4 active usersReviewed

Complexity Theory Computational Geometry·Captain: Shuze Chen

Terrain Guarding is NP-Hard: NP-hardness of discrete and continuous terrain guardingResearch Paper

Selecting a small collection of sites with line of sight to an entire landscape is a geometric coverage problem. In the one-dimensional terrain model, the landscape is represented by a polygonal profile in the plane. The optimization question asks how many guards are needed to see every point of that profile. Applications motivating the model include road…

10 thms4 active usersReviewed

Algorithmic Game Theory Combinatorics Operations Research·Captain: iris

Efficient Black-Box Reductions for Separable Cost Sharing: In Matroid Games with Subadditive Costs, Algorithm 1 Turns Any Profile into a No Costlier Enforceable Profile Within n·m·rk IterationsResearch Paper

In a cost sharing game each player chooses a set of resources, and the cost of every resource has to be divided among the players who use it. A designer who wants a cheap outcome to be stable chooses the division rule, the cost sharing protocol, so that the cheap outcome becomes a pure Nash equilibrium. Practical protocols should be separable: the share a…

13 thms4 active usersReviewed

Algorithmic Game Theory Analysis Operations Research·Captain: iris

Existence and Complexity of Approximate Equilibria in Weighted Congestion Games: Polynomial Games of Degree d With No α-PNE for Any α < α(d), Where α(d) ≥ √d/(2 ln d) for Large dResearch Paper

Weighted congestion games model players of different sizes sharing resources whose cost grows with load: traffic of different volumes on network links, jobs of different lengths on machines. Rosenthal (1973) showed that unweighted congestion games always have a pure Nash equilibrium, but weighted games may have none, already with polynomial costs. The…

28 thms4 active usersReviewed

Operations Research·Captain: Shuze Chen

Dynamic Stochastic Matching Under Limited Time: Constant-factor reward approximation on arbitrary and bipartite graphsResearch Paper

A matching platform must decide whether to pair available agents now or wait for a more valuable partner. Waiting creates an opportunity and a risk: an agent may leave before that partner arrives. Ride sharing, service exchanges and matching markets motivate models in which arrivals continue indefinitely and departure times are not announced in advance. A…

23 thms4 active usersReviewed

Top contributors

Rank	Contributor	Accepted solutions	Submitted problems
1	Eyal1990	5022	7705
2	fizzyinc3	1303	7
3	marwahaha	643	870
4	mrfancypants	629	0
5	dbenbenn	546	543
6	kmehltretter82	328	92
7	Nihal	296	0
8	Nickrobbins95	269	8
9	Shuze Chen	224	794
10	shivm	208	0

The TCS Formalization Drive

Missions

Online Stochastic Matching: Beating 1-1/e 1: When OPT = Ω(n), the Two Suggested Matchings Algorithm Achieves ALG/OPT ≥ (1 − 2/e²)/(4/3 − 2/(3e)) − ε ≈ 0.670 with Probability 1 − e^(−Ω(n))Research Paper

CLIQUE is NP-CompleteResearch Paper

Eigenvalues and Expanders: A Regular Bipartite Graph Is a Strong Expander If and Only If λ(G) Is Bounded Away from 0Research Paper

A Dynamic Near-Optimal Algorithm for Online Linear Programming I: The Competitive Ratio of the Dynamic Learning AlgorithmResearch Paper

Competitive Randomized Algorithms for Nonuniform Problems III: The Optimal Randomized Two-Server Ratio on the 1-d-d Isosceles TriangleResearch Paper

AlphaEvolve Eighth-Power Bound: omega < 2.371177Research Paper

Competitive Paging Algorithms IV: An Algorithm Competitive against Several Others Exists iff the Reciprocal Ratios Sum to at Most 1Research Paper

Linear Programming in Linear Time When the Dimension Is Fixed: Fixed-Dimension LP Feasibility Decided in Linear Time on the Real RAMResearch Paper

The Design of Competitive Online Algorithms via a Primal-Dual Approach VIII: The Bounded Allocation ProblemTextbook

Foundations of Machine Learning XII: Algorithmic StabilityTextbook

Foundations of Machine Learning V: Kernel Methods and the Representer TheoremTextbook

Coppersmith–Winograd Bound: omega < 2.376Research Paper

Pure Nash Equilibria: Hard and Easy Games: Deciding Whether a Game Has a Pure Nash Equilibrium Is NP-Complete, Even for Graphical Games with 3-Bounded Neighborhood and Three ActionsResearch Paper

Quantum Max-Cut: 0.5260.5260.526 energy estimationResearch Paper

Classical 0.53 energy estimation for Quantum Max-CutResearch Paper

The Complexity of Pacing for Second-Price Auctions: Finding an Approximate Pacing Equilibrium Is PPAD-HardResearch Paper

Serial batching to minimize the weighted number of tardy jobs: W[1]-hardness for #d + #p and for #p + #r, with XP algorithms for #d + #p + #w and for #p + #r + #wResearch Paper

Geometric Rescaling Algorithms for Submodular Function Minimization: Rescaling-SFM finds a minimizer of an integer-valued submodular function in O((n4⋅EO+n5)log⁡(nL))O((n^4\cdot\mathrm{EO}+n^5)\log(nL))O((n4⋅EO+n5)log(nL)) timeResearch Paper

The Complexity of Recognizing Facets for the Knapsack Polytope: Deciding Whether an Integer Inequality Defines a Facet of a Knapsack Polytope Is Dᵖ-CompleteResearch Paper

Finding Hall Blockers by Matrix Scaling: without a perfect matching, (1/4)n² log(mA_max/A_min) Sinkhorn iterations and a sort of the scaling vectors output a Hall blockerResearch Paper

Hard Tiling Problems with Simple Tiles: Decision and counting completeness for right trominoes and square tetrominoesResearch Paper

Terrain Guarding is NP-Hard: NP-hardness of discrete and continuous terrain guardingResearch Paper

Efficient Black-Box Reductions for Separable Cost Sharing: In Matroid Games with Subadditive Costs, Algorithm 1 Turns Any Profile into a No Costlier Enforceable Profile Within n·m·rk IterationsResearch Paper

Existence and Complexity of Approximate Equilibria in Weighted Congestion Games: Polynomial Games of Degree d With No α-PNE for Any α < α(d), Where α(d) ≥ √d/(2 ln d) for Large dResearch Paper

Dynamic Stochastic Matching Under Limited Time: Constant-factor reward approximation on arbitrary and bipartite graphsResearch Paper

Top contributors

Quantum Max-Cut: $0.526$ energy estimationResearch Paper

Geometric Rescaling Algorithms for Submodular Function Minimization: Rescaling-SFM finds a minimizer of an integer-valued submodular function in $O((n^4\cdot\mathrm{EO}+n^5)\log(nL))$ timeResearch Paper