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.

582 missions

Missions

126–150 of 582
Open104Completed478All582
🏆Completed
CombinatoricsGraph TheoryLinear Optimization+2·Captain: mikedeng1

The Geometry of Graphs and Some of Its Algorithmic Applications 1: Every Multicommodity Flow Network with k Source-Sink Pairs Has a Cut S with Cap(S)/Dem(S) ≤ O(log k) · maxflowResearch Paper

Routing several commodities through one capacitated network at the same time is a basic problem of network optimization, with applications to communication networks, VLSI layout and divide-and-conquer graph algorithms. Its optimum is the value of a linear program, but the natural certificates of an upper bound are combinatorial: every cut of the network…

9 thms4 active usersReviewed
🏆Completed
CombinatoricsOperations ResearchProbability+1·Captain: mikedeng1

An Optimal Algorithm for On-line Bipartite Matching 1: RANKING Finds a Matching of Expected Size at Least n(1 − 1/e) − o(n) on Every Graph with a Perfect MatchingResearch Paper

Online matching describes allocation when requests must be answered as they arrive. A matching decision uses only the edges revealed so far and cannot be revised when later requests appear. In the bipartite setting studied by Karp, U. Vazirani, and V. Vazirani, the arriving vertices are girls and the possible partners are boys. Even when the full graph has…

10 thms4 active usersReviewed
🏆Completed
Theoretical Computer Science·Captain: wurtle

Subset Sum is NP-completeResearch Paper

Prove that subset sum is NP-complete by reducing the existing 3-SAT language, to it. Given a list of positive integers and a nonnegative target, decide whether some selection of entries sums exactly to the target. Integers are encoded in binary.

26 thms4 active usersReviewed
🏆Completed
CombinatoricsGraph TheoryLinear algebra+1·Captain: mikedeng1

Explicit Expanders of Every Degree and Size 2: Attaching New Vertices to a (p+1)-Regular Ramanujan Graph and Adding Loops Keeps Every Nontrivial Eigenvalue at Most √(2(p+1)) + √p + o(1)Research Paper

Sparse graphs whose adjacency spectrum is concentrated near zero, expanders, are used throughout theoretical computer science: in error-correcting codes, derandomization, sorting and routing networks, and the construction of pseudorandom objects (Hoory, Linial and Wigderson, survey). The best possible spectral expansion for a ddd-regular graph is governed by…

9 thms4 active usersReviewed
🏆Completed
Theoretical Computer Science·Captain: wurtle

k-SAT is NP-HardResearch Paper

Prove that kkk-SAT is NP-complete for every fixed k≥3k\ge3k≥3, with at most kkk literal occurrences per clause.

16 thms4 active usersReviewed
🏆Completed
Machine LearningQuantum InformationTheoretical Computer Science·Captain: mikedeng1

Shadow Tomography of Quantum States 1: Polylogarithmically Many Copies Suffice to Estimate Every Acceptance Probability to Within εResearch Paper

Learning an unknown quantum state is expensive. Full quantum state tomography of a DDD-dimensional mixed state ρ\rhoρ to accuracy ε\varepsilonε in trace distance needs on the order of D2/ε2D^2/\varepsilon^2D2/ε2 copies of ρ\rhoρ (O'Donnell–Wright 2016; Haah et al. 2017), and this is optimal. For a system of nnn qubits, D=2nD = 2^nD=2n, so full tomography is out of reach beyond a few…

17 thms4 active usersReviewed
🏆Completed
Linear OptimizationOperations ResearchOptimization+1·Captain: mikedeng1

Real-Time Optimization of Personalized Assortments: Inventory Balancing Is α_cmin(Ψ)-CompetitiveResearch Paper

Online retailers choose, customer by customer, which products to display. The customer's type (location, history, device) is revealed on arrival. Inventories are finite and are not replenished during the selling season. A seller who shows every customer the currently most profitable products can sell out a product early and leave nothing for later customers…

14 thms4 active usersReviewed
🏆Completed
Linear OptimizationOperations ResearchOptimization+2·Captain: mikedeng1

A Dynamic Near-Optimal Algorithm for Online Linear Programming II: A Lower Bound for Every Online AlgorithmResearch Paper

Online linear programming models resource allocation under uncertainty about future demand: requests arrive one at a time, each asking for some amounts of mmm resources and offering a payment, and each must be accepted or rejected, irrevocably, on arrival. Airline seat and hotel room revenue management, online routing with bandwidth limits and the allocation…

7 thms4 active usersReviewed
🏆Completed
Machine LearningOperations ResearchProbability+1·Captain: mikedeng1

Competitive Caching with Machine Learned Advice: The Competitive Ratio of Predictive MarkerResearch Paper

Caching (online paging) is one of the oldest problems in online algorithms: a fast memory of kkk slots serves a sequence of requests, and every request for an element not in the fast memory is a cache miss that forces the element to be loaded, possibly evicting another one. With the whole request sequence known in advance, evicting the element whose next…

10 thms4 active usersReviewed
🏆Completed
Linear OptimizationOperations ResearchProbability+1·Captain: mikedeng1

Competitive Randomized Algorithms for Nonuniform Problems IV: The Optimal Randomized Two-Server Ratio 1652/1069 on the 3-4-5 TriangleResearch Paper

The kkk-server problem is a basic model of on-line decision making. kkk mobile servers move in a metric space, requests for points arrive one at a time, and each request has to be covered by a server before the next one arrives. The cost is the total distance the servers move. The problem includes paging, caching and disk-head scheduling as special cases (Manass…

7 thms4 active usersReviewed
🏆Completed
Linear OptimizationOperations ResearchProbability+1·Captain: mikedeng1

Competitive Randomized Algorithms for Nonuniform Problems I: Optimal Competitiveness of Randomized Block Snoopy CachingResearch Paper

In a shared-memory multiprocessor, each processor keeps copies of memory blocks in its own cache, and all caches listen ("snoop") on a common bus. Every bus cycle spent keeping these copies consistent is a cycle not available for useful work, so the protocol that decides when a block is shared by several caches and when it is private to one cache directly…

8 thms4 active usersReviewed
🏆Completed
CombinatoricsTheoretical Computer Science·Captain: mikedeng1

Three Partition Refinement Algorithms 2: Refining by the Smaller HalfResearch Paper

Many equivalence problems on finite structures reduce to computing the coarsest partition of a finite set that is compatible with a relation. Deciding whether two states of a finite labelled transition system are bisimilar, testing congruence of finite-state processes in Milner's calculus of communicating systems (CCS), and minimizing a deterministic finite…

12 thms4 active usersReviewed
🏆Completed
Operations ResearchProbabilityTheoretical Computer Science·Captain: mikedeng1

Competitive Paging Algorithms I: The Marking Algorithm Is 2H_k-CompetitiveResearch Paper

Paging is the problem of managing a two-level memory: a fast cache holds kkk pages out of an address space of nnn pages, requests to pages arrive one at a time, and a request to a page outside the cache (a page fault) forces the algorithm to bring that page in and, when the cache is full, to evict another. The cost is the number of faults. An on-line algorithm…

10 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
🏆Completed
CombinatoricsGraph TheoryOperations Research+2·Captain: mikedeng1

An Analysis of Several Heuristics for the Traveling Salesman Problem I: Nearest Neighbor Tours Can Be Far from OptimalResearch Paper

The traveling salesman problem with the triangle inequality asks for a shortest closed tour through nnn points whose distances form a metric. It is NP-hard, so in practice tours are built by fast construction heuristics, and the natural question is how far such a tour can be from optimal in the worst case. Rosenkrantz, Stearns and Lewis (SIAM J. Comput. 6(3),…

12 thms4 active usersReviewed
🏆Completed
CombinatoricsOperations ResearchOptimization+1·Captain: mikedeng1

Worst-Case Performance Bounds for Simple One-Dimensional Packing Algorithms 4: First-Fit Decreasing Uses at Most 71/60 L* + 5 Bins When No Item Exceeds 1/2Research Paper

Bin packing asks how to place a list of items with sizes in (0,1](0,1](0,1] into as few unit-capacity bins as possible. It models the cutting of stock material, the packing of files onto tracks of a disc and the assignment of jobs to machines with a common deadline. Deciding the optimum is NP-hard, so in practice simple rules are used, and the question is how far…

9 thms4 active usersReviewed
🏆Completed
CombinatoricsOperations ResearchOptimization+1·Captain: mikedeng1

Worst-Case Performance Bounds for Simple One-Dimensional Packing Algorithms 2: First-Fit and Best-Fit with Bounded Item SizesResearch Paper

Bin packing asks for the fewest unit-capacity bins that hold a given list of item sizes. It models cutting stock, memory allocation, file placement and the loading of trucks, and it is NP-hard, so in practice lists are packed by simple rules that look at one item at a time. The two most widely used rules are First-Fit and Best-Fit, and the question that…

7 thms4 active usersReviewed
🏆Completed
CombinatoricsOperations ResearchOptimization+1·Captain: mikedeng1

Worst-Case Performance Bounds for Simple One-Dimensional Packing Algorithms 1: First-Fit and Best-Fit Have Asymptotic Worst-Case Ratio 17/10Research Paper

Bin packing asks for the fewest unit-capacity bins that hold a given list of item sizes. It is one of the first problems studied through the worst-case analysis of approximation algorithms, and it models storage allocation, paging and file placement on tracks, as well as cutting-stock problems in operations research. Deciding the optimum exactly is NP-hard,…

9 thms4 active usersReviewed
🏆Completed
CombinatoricsOperations ResearchOptimization+2·Captain: mikedeng1

Approximation Techniques for Average Completion Time Scheduling I: Best-α on One Machine with Release DatesResearch Paper

Minimizing the average completion time of jobs that arrive over time is one of the basic objectives of machine scheduling: it measures how long, on average, a job waits in the system. On a single machine with release dates and no preemption (written 1∣rj∣∑Cj1|r_j|\sum C_j1∣rj​∣∑Cj​), the problem is strongly NP-hard, so research has focused on approximation algorithms whose…

9 thms4 active usersReviewed
🏆Completed
CombinatoricsOperations ResearchOptimization+1·Captain: mikedeng1

Local Search Heuristics for k-Median and Facility Location Problems III: Add-Drop-Swap Local Search for Uncapacitated Facility Location Has Locality Gap 3Research Paper

The uncapacitated facility location (UFL) problem is one of the basic models of location theory and operations research: a firm chooses which warehouses, plants or servers to open, paying a fixed cost for each open site and a service cost for every client according to its distance to the nearest open site. It is also a standard test case for approximation…

10 thms4 active usersReviewed
🏆Completed
Graph TheoryOperations ResearchTheoretical Computer Science·Captain: mikedeng1

The Design of Competitive Online Algorithms via a Primal-Dual Approach VII: Online Group Steiner TreesTextbook

The group Steiner tree problem generalizes the ordinary Steiner tree problem: given a rooted tree and several groups of vertices, find a minimum-cost subtree that connects at least one vertex of each group to the root. It is a canonical instance of the generalized-connectivity family this survey studies in Chapter 11 — a family that also contains the online…

11 thms4 active usersReviewed
🏆Completed
Linear OptimizationOperations ResearchTheoretical Computer Science·Captain: mikedeng1

The Design of Competitive Online Algorithms via a Primal-Dual Approach II: The Online Set-Cover ProblemTextbook

Section 4 of this survey derives a simple randomized O(log⁡mlog⁡n)O(\log m \log n)O(logmlogn)-competitive algorithm for the online set-cover problem, by rounding the fractional solution the online packing-covering framework produces. An intriguing question the survey poses next: can the same guarantee be achieved deterministically? The standard tool for removing randomness, the…

7 thms4 active usersReviewed
🏆Completed
Machine LearningProbabilityStatistics+1·Captain: mikedeng1

Foundations of Machine Learning XI: Maximum Entropy Models and DualityTextbook

Maximum entropy (Maxent) models are a widely used family of density-estimation algorithms: given a sample and a set of features, they select the distribution that matches the empirical feature averages while being otherwise as "agnostic" (close to a prior, usually uniform) as possible — a principle that, notably, never requires specifying a parametric…

15 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
PreviousPage 6 of 24Next

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