Prove2Me
Navigate
DiscoverCollectionsFormalpediaGalaxyBlogsUsersMomentumMy Missions+
Prove2Me
Log in
← Collections

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.

104 open missions

Missions

26–50 of 104
Open104Completed478All582
Machine LearningProbabilityTheoretical Computer Science·Captain: mikedeng1

What Can We Learn Privately? III: An ε-Local Algorithm Simulates Any t-Query Statistical Query Algorithm from O(t log(t/β) b²/(ε²τ²)) SamplesResearch Paper

In the local model of differential privacy, no trusted curator ever sees the raw data: each individual randomizes their own record before handing it to the analyst. This is how private telemetry is collected in practice (randomized response and its descendants), and it raises a basic question: which learning tasks remain possible when the learner only sees…

9 thms4 active usersReviewed
Complexity TheoryInformation TheoryProbability+1·Captain: mikedeng1

A Pseudorandom Generator from Any One-Way Function: One-Way Functions Exist If and Only If Pseudorandom Generators ExistResearch Paper

Cryptographic protocols use random looking strings that can be reproduced from a shorter private seed. A pseudorandom generator provides those strings if no efficient observer can tell them from uniformly sampled bits. A one-way function provides a different kind of asymmetry: anyone can evaluate it efficiently, but no efficient algorithm can usually…

18 thms4 active usersReviewed
CombinatoricsComplexity TheoryOperations Research+2·Captain: mikedeng1

A Threshold of ln n for Approximating Set Cover II: The Inapproximability of Max k-CoverResearch Paper

Max kkk-cover is the basic coverage problem of combinatorial optimization. The input is a collection of subsets of a finite ground set and a number kkk; the task is to choose kkk subsets that together cover as many points as possible. It models facility and sensor placement, the selection of a small committee or feature set representing a population, and budgeted…

23 thms4 active usersReviewed
CombinatoricsComplexity TheoryOperations Research+1·Captain: mikedeng1

A Threshold of ln n for Approximating Set Cover I: The ln n Inapproximability of Set CoverResearch Paper

Set cover is the problem of covering a finite ground set with as few members of a given family of subsets as possible. It models facility location, crew scheduling, test-suite minimization and many other selection problems in operations research, and it is one of the canonical NP-hard problems. The greedy algorithm, which repeatedly picks the subset…

20 thms4 active usersReviewed
Machine LearningProbabilityStatistics+1·Captain: mikedeng1

Foundations of Machine Learning VIII: Multi-Class Classification and the Margin BoundTextbook

Every generalization bound in chapters 2-5 is for binary classification. Most real-world classification problems have more than two classes, and the number of classes can itself be in the hundreds or thousands (topic classification, speech recognition). Chapter 9 extends the margin-based generalization theory of chapter 5 (SVMs) to this multi-class,…

18 thms4 active users
Machine LearningProbabilityStatistics+1·Captain: mikedeng1

Foundations of Machine Learning III: Structural Risk Minimization and Model SelectionTextbook

Chapters 2 and 3 bound the estimation error of a hypothesis chosen from a fixed hypothesis set HHH, but the choice of HHH itself is left open: a richer HHH lowers the approximation error (how close HHH comes to the Bayes classifier) at the price of a looser generalization bound, and a poorer HHH does the reverse. Chapter 4 is the book's answer to this trade-off. It…

16 thms4 active users
Operations ResearchProbabilityTheoretical Computer Science·Captain: iris

Order-Optimal Correlated Rounding for Fulfilling Multi-Item E-Commerce Orders: Algorithm 1 Is a (1+ln⁡q)(1 + \ln q)(1+lnq)-Competitive Rounding Scheme with Runtime O(qK)O(qK)O(qK)Research Paper

An online retailer that holds inventory in many fulfillment centres (FCs) decides, for each item of an order, where to ship it from. A linear program solved over all orders gives, for each item, a probability distribution over FCs that is right on average. The difficulty is correlation: items sent to different FCs ship in separate packages, so an order is…

20 thms3 active usersReviewed
Convex OptimizationGraph TheoryOptimization+1·Captain: marwahaha

Grothendieck inequalities for semidefinite programs with rank constraintResearch Paper

The graphical Grothendieck problem with rank constraint maximizes a quadratic form over unit vectors assigned to the vertices of a graph. Depending on the rank, the same problem is MAX CUT, Grothendieck's inequality, the ground state of a spin model, or the value of a quantum XOR game.

22 thms3 active usersReviewed
Complexity TheoryOperations ResearchOptimization+1·Captain: iris

Efficient Approximation Schemes for Stochastic Probing and Selection-Stopping Problems: Free-Order Prophets Admits an EPTAS, a t(ε)·poly(n)-Time (1 − ε)-Approximate OrderResearch Paper

In Free-Order Prophets a decision maker faces nnn independent non-negative random values with known laws, chooses in advance the order in which to inspect them, and on seeing each value must stop and take it or move on for good. The problem models selection with a sequence the decision maker controls: sequencing interviews, or inspecting alternatives whose…

43 thms3 active usersReviewed
Algorithmic Game TheoryOperations ResearchTheoretical Computer Science·Captain: iris

Computing Approximate Equilibria in Weighted Congestion Games via Best-Responses: A Polynomial-Time Best-Response Algorithm Reaches a dd+o(d)d^{d+o(d)}dd+o(d)-Approximate EquilibriumResearch Paper

Weighted congestion games model players who share resources (links of a network, machines, servers) and whose cost on a resource grows with the total weight using it. They are standard models of selfish routing and load balancing. Unlike unweighted congestion games, they need not have a pure Nash equilibrium once costs are polynomials of degree d≥2d\ge2d≥2 (Harks–…

58 thms3 active usersReviewed
Computational ComplexityQuantum Error CorrectionQuantum Information·Captain: iris

The Heisenberg Representation of Quantum Computers: Clifford circuits with Pauli measurements and classical control are perfectly simulated in randomized classical polynomial time (Knill's theorem)Research Paper

A general nnn-qubit quantum computation is described by 2n2^n2n complex amplitudes, and following them on a classical computer costs exponential time and space. Daniel Gottesman's 1998 paper The Heisenberg Representation of Quantum Computers shows that a large and practically important class of quantum networks escapes this cost. Instead of the state, one follows…

22 thms3 active usersReviewed
Operations ResearchOptimizationProbability+1·Captain: iris

On Greedy-Like Policies in Online Matching with Reusable Network Resources and Decaying Rewards: Random-Threshold Greedy Is αβ/((1+αβL)(1+ln⁡R))\alpha\beta/((1+\alpha\beta L)(1+\ln R))αβ/((1+αβL)(1+lnR))-CompetitiveResearch Paper

Online platforms repeatedly match arriving demand to resources that are used up only temporarily. A rented item, a cloud server or a hotel room is reusable: once used it is unavailable for a random time and then returns. Requests often need several resources at once (a multi-night stay, a bundle of products), which makes the resources a network, and rewards…

40 thms3 active usersReviewed
Algorithmic Game TheoryCombinatoricsMarkov Chain+1·Captain: iris

Sampling from the Gibbs Distribution in Congestion Games: Relaxed Logit Dynamics in Extension Parallel Congestion Games Mix within n3(log⁡(nlog⁡∣P∣+TΦmax⁡)+log⁡(1/(2ϵ2)))n^3(\log(n\log|P|+T\Phi_{\max})+\log(1/(2\epsilon^2)))n3(log(nlog∣P∣+TΦmax​)+log(1/(2ϵ2))) StepsResearch Paper

Logit dynamics is the standard model of noisy best-response play: repeatedly, a uniformly random player revises their strategy, choosing each option with probability proportional to e−T⋅coste^{-T\cdot\text{cost}}e−T⋅cost, where the temperature T≥0T\ge0T≥0 measures rationality. In a potential game the dynamics is a reversible Markov chain whose stationary law is the Gibbs…

41 thms3 active usersReviewed
Algorithmic Game TheoryComplexity TheoryMechanism Design+1·Captain: iris

Core Pricing in Combinatorial Exchanges with Financially Constrained Buyers: Computational Hardness and Algorithmic Solutions: Computing a Welfare-Maximizing Core Outcome Is Σ₂ᵖ-HardResearch Paper

Many markets trade packages of indivisible goods between several buyers and several sellers at once: airport time slots, spectrum licences, transport capacity, emission permits. Such a market is a combinatorial exchange. Its operator chooses who trades which package and at which prices, and wants the outcome to be stable: no group of participants should be…

16 thms3 active usersReviewed
Algorithmic Game TheoryOperations ResearchProbability+1·Captain: iris

Prophet Inequality for Bipartite Matching: Merits of Being Simple and Nonadaptive: Static Vertex Prices Earn One Third of the Prophet's Expected Matching ValueResearch Paper

A prophet inequality compares an online decision maker, who sees random values one at a time and must decide irrevocably, with a prophet who sees every value in advance. The classical single-item version (Krengel–Sucheston, Samuel-Cahn) shows that a single threshold earns half of the prophet's expected maximum. These guarantees are the analytic core of poste…

18 thms3 active usersReviewed
CombinatoricsConvex OptimizationLinear Optimization+1·Captain: iris

On Polyhedral Approximations of the Positive Semidefinite Cone: Every Polytope Between (1−ε)(D − A) and D − A Has Extension Complexity at Least exp(c√n)Research Paper

Linear programs are the workhorse of optimization, and a recurring question is which convex sets can be described, or approximated, by a linear program of small size. The relevant measure is the extension complexity xc⁡(P)\operatorname{xc}(P)xc(P) of a polytope PPP: the smallest number of facets of a polytope that projects linearly onto PPP. If xc⁡(P)=N\operatorname{xc}(P)=Nxc(P)=N,…

26 thms3 active usersReviewed
CombinatoricsOperations ResearchOptimization·Captain: iris

Semidefinite Programming Relaxations of the Traveling Salesman Problem and Their Integrality Gaps: The de Klerk–Sotirov SDP Has Integrality Gap at Least z for Every z ∈ ℕResearch Paper

The metric traveling salesman problem (TSP) asks for a shortest tour through nnn cities whose pairwise costs are symmetric and satisfy the triangle inequality. The best-known guarantees for it come from relaxations: Christofides' 3/23/23/2-approximation is analysed against the subtour-elimination linear program (Held–Karp), and the integrality gap of that LP is…

37 thms3 active usersReviewed
CombinatoricsOperations ResearchOptimization+1·Captain: iris

An Optimal Streaming Algorithm for Submodular Maximization with a Cardinality Constraint: StreamProcess Is a Single-Pass (α/(1+α)−ε)(\alpha/(1+\alpha)-\varepsilon)(α/(1+α)−ε)-ApproximationResearch Paper

A set function f:2V→Rf:2^V\to\mathbb Rf:2V→R is submodular if f(A)+f(B)≥f(A∩B)+f(A∪B)f(A)+f(B)\ge f(A\cap B)+f(A\cup B)f(A)+f(B)≥f(A∩B)+f(A∪B) for all A,B⊆VA,B\subseteq VA,B⊆V. Maximizing such a function subject to ∣S∣≤k|S|\le k∣S∣≤k models data summarization, where fff measures how informative and diverse a summary SSS is, and kkk keeps it small (Badanidiyuru et al., 2014). When the data set does not fit in memory, the relevant model is…

25 thms3 active usersReviewed
CombinatoricsGraph TheoryOperations Research·Captain: Shuze Chen

Labelling algorithms for paired-domination problems in block and interval graphs: Linear-time minimum paired domination in interval graphsResearch Paper

A dominating set chooses locations that collectively cover a network: every location outside the chosen set must be adjacent to a chosen location. Paired domination adds a backup requirement. The chosen locations must be partitionable into adjacent pairs, so every selected location has a designated partner. Minimizing the number of selected locations…

12 thms3 active usersReviewed
Complexity TheoryOptimizationTheoretical Computer Science·Captain: Shuze Chen

Tetris is Hard, Even to Approximate: Inapproximability of cleared rowsResearch Paper

Knowing every future piece removes uncertainty from Tetris, but it does not remove the computational difficulty of choosing placements. Offline Tetris asks a player to plan against an entire finite piece sequence revealed in advance. The initial board can already contain occupied cells, and its dimensions are part of the input. Demaine, Hohenberger and…

24 thms3 active usersReviewed
Complexity Theory·Captain: Shuze Chen

Sorting by Transpositions Is Difficult: Sorting by Transpositions is NP-hardResearch Paper

A transposition exchanges two neighboring stretches of a sequence without changing the order inside either stretch. In comparative genomics, such an operation models moving a contiguous sequence of genes to another position. When each gene occurs once, a genome can be represented by a permutation. The minimum number of transpositions needed to transform one…

25 thms3 active usersReviewed
CombinatoricsGraph TheoryOperations Research·Captain: iris

Counting and Enumerating Optimum Cut Sets for Hypergraph k-Partitioning Problems for Fixed k: Cut-Sets of Value OPT_k-cut Are Recovered by Every Minimum (S, T)-Terminal Cut for Some |S|, |T| ≤ 2k − 1Research Paper

Hypergraph-kkk-Cut asks for a partition of the vertex set of a hypergraph into kkk non-empty parts that is crossed by as few hyperedges as possible. It models clustering and partitioning tasks in which an interaction involves more than two objects (VLSI netlists, multi-way relations in data). For graphs, the number of optimum kkk-partitions is polynomial for…

25 thms3 active usersReviewed
CombinatoricsComplexity Theory·Captain: Shuze Chen

Tatamibari Is NP-Complete: NP-completeness of TatamibariResearch Paper

Tatamibari asks a player to divide a grid into rectangles subject to clues about their shapes. Its rules concern individual rectangles and the corners where rectangles meet, but deciding whether an arbitrary board can be solved is a computational complexity question. Adler, Bosboom, Demaine, Demaine, Liu, and Lynch establish NP-completeness in Tatamibari Is…

23 thms3 active usersReviewed
CombinatoricsComplexity Theory·Captain: Shuze Chen

Solving Mahjong Solitaire boards with peeking: NP-completeness for isolated three-tile stacksResearch Paper

Mahjong Solitaire asks a player to remove a layout of tiles by choosing matching pairs. The visible choices depend on which tiles have already been removed. Allowing peeking, meaning that all tile labels are known from the start, removes uncertainty about hidden information but leaves the constraints on legal removal. This distinction matters when studying…

7 thms3 active usersReviewed
Complexity TheoryGraph Theory·Captain: Shuze Chen

Zig-Zag Numberlink is NP-Complete: NP-completeness of full-cover disjoint paths on square gridsResearch Paper

Zig-Zag Numberlink asks a player to connect matching numbered cells by paths while using every cell of a rectangular board. The rules involve only local movements and recognizable endpoints, but a choice for one pair can prevent another pair from being connected or leave cells that no path can visit. The resulting decision problem links familiar grid…

5 thms3 active usersReviewed
PreviousPage 2 of 5Next

Top contributors

RankContributorAccepted solutionsSubmitted problems
1EYEyal199050227705
2FIfizzyinc313037
3MAmarwahaha643870
4MRmrfancypants6290
5DBdbenbenn546543
6KMkmehltretter8232892
7NINihal2960
8NINickrobbins952698
9SCShuze Chen224794
10SHshivm2080

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paperProve2Me Team
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me