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

526–550 of 582
Open104Completed478All582
🏆Completed
CombinatoricsGraph TheoryOperations Research+2·Captain: mikedeng1

An Analysis of Several Heuristics for the Traveling Salesman Problem II: Every Insertion Method Is Within ⌈lg n⌉ + 1 of the Optimal TourResearch Paper

The traveling salesman problem asks for a shortest closed route visiting every node of a weighted complete graph exactly once. It is NP-hard, so practitioners use fast heuristics, and the basic question about a heuristic is how far from optimal its tour can be. Rosenkrantz, Stearns and Lewis (SIAM J. Comput. 6(3), 1977) gave the first systematic worst-case…

10 thms2 active usersReviewed
🏆Completed
CombinatoricsDynamic ProgrammingTheoretical Computer Science·Captain: mikedeng1

A Faster Algorithm Computing String Edit Distances 1: for a finite alphabet and discrete costs, the block algorithm (Algorithms Y and Z) computes the edit distance from a finite tableResearch Paper

The edit distance between two strings is the least total cost of a sequence of single-character insertions, deletions and replacements turning one string into the other. It is the basic similarity measure of spelling correction, file comparison and biological sequence alignment. Wagner and Fischer (JACM 1974) showed that it can be computed by filling a …

10 thms2 active usersReviewed
🏆Completed
Graph TheoryLinear OptimizationOperations Research+1·Captain: mikedeng1

Finding Minimum-Cost Circulations by Canceling Negative Cycles: Polynomial Termination of Minimum-Mean Cycle CancelingResearch Paper

The minimum-cost circulation problem is a central problem of network optimization: transportation, assignment, shortest-path and maximum-flow problems are all special cases, and it is one of the few classes of linear programs with fast combinatorial algorithms. The oldest algorithm for it, the cycle-canceling algorithm of Klein (1967), repeatedly finds a…

10 thms2 active usersReviewed
🏆Completed
Operations ResearchOptimizationProbability+1·Captain: mikedeng1

An Optimal On-Line Algorithm for Metrical Task System 2: The Randomized Competitive Ratio of the Uniform Task System Lies Between H(n) and 2H(n)Research Paper

Metrical task systems, introduced by Borodin, Linial and Saks (J. ACM 39(4), 1992), are a common abstraction of on-line problems in which a server occupies one of finitely many states, pays a cost for each task depending on its current state, and may pay a transition cost to change state first. Paging, list update and the kkk-server problem all fit into this…

9 thms2 active usersReviewed
🏆Completed
Operations ResearchOptimizationTheoretical Computer Science·Captain: mikedeng1

An Optimal On-Line Algorithm for Metrical Task System 1: Every n-State Metrical Task System Has Competitive Ratio 2n - 1Research Paper

A system that processes a stream of tasks can often be configured in several ways, and the configuration affects both the cost of the current task and the cost of switching before the next one: paging schemes, replicated files, server placements. When the future is unknown, the natural worst-case yardstick is competitive analysis, introduced by Sleator and…

12 thms2 active usersReviewed
🏆Completed
Information TheoryTheoretical Computer Science·Captain: marwahaha

Most Informative Boolean Function ConjectureResearch Paper

Send a uniformly random string X∈{0,1}nX \in \{0,1\}^nX∈{0,1}n through a memoryless binary symmetric channel with crossover probability ppp: each coordinate is flipped independently with probability ppp, producing Y∈{0,1}nY \in \{0,1\}^nY∈{0,1}n. An observer sees YYY and wants to learn about XXX — but the summary of XXX they are allowed to keep is a single bit f(X)f(X)f(X), computed by a Boolean function fff…

7 thms2 active usersReviewed
🏆Completed
AnalysisMachine LearningProbability+1·Captain: MiltMont

Flow Matching Theorem 1: Marginal Continuity EquationResearch Paper

Flow matching models a changing probability distribution using a time-dependent velocity field. A conditional model specifies a density and a velocity separately for each conditioning point. The mathematical question is whether those conditional descriptions determine a velocity for the mixture distribution. This mission concerns the continuity-equation…

6 thms2 active usersReviewed
🏆Completed
Information TheoryTheoretical Computer Science·Captain: Lucas

Shannon 1949: Perfect SecrecyResearch Paper

Cryptography before 1949 was a catalogue of ciphers and of the tricks that broke them. C. E. Shannon's Communication Theory of Secrecy Systems (Bell System Technical Journal 28(4):656–715, 1949) replaced the catalogue with a probabilistic model: a cipher is a family of invertible maps from messages to cryptograms, indexed by a key drawn from a known…

7 thms2 active usersReviewed
🏆Completed
Linear OptimizationOperations ResearchTheoretical Computer Science·Captain: mikedeng1

The Design of Competitive Online Algorithms via a Primal-Dual Approach IX: General Packing-Covering ConstraintsTextbook

Chapter 4's framework (formalized in this series' 04-framework mission) solves the online covering-packing pair only in the restricted setting a(i,j) ∈ {0,1}, b(j) = 1 — every constraint is an unweighted "cover me with at least one of these" condition. Chapter 14 delivers the promise made at the very start of the survey (p. 115: "we show how to extend the…

7 thms2 active usersReviewed
🏆Completed
Operations ResearchTheoretical Computer Science·Captain: mikedeng1

The Design of Competitive Online Algorithms via a Primal-Dual Approach V: Online RoutingTextbook

Network routing is one of the paradigmatic applications of the online primal-dual method: requests for bandwidth between a source and target arrive one at a time, and the algorithm must commit bandwidth to paths without knowing future requests. Chapter 4 already gave a simple (3, O(log n))-competitive routing algorithm as an illustration of the general…

2 thms2 active usersReviewed
🏆Completed
Operations ResearchTheoretical Computer Science·Captain: mikedeng1

The Design of Competitive Online Algorithms via a Primal-Dual Approach III: Metrical Task Systems on a Weighted StarTextbook

The metrical task system (MTS) problem is one of the earliest and most general online models: a server occupies a state in a metric space, requests arrive with per-state service costs, and the server may change state (paying the metric's transition cost) before serving each request. On a general metric, competitive algorithms are hard to design directly.…

6 thms2 active usersReviewed
🏆Completed
Machine LearningProbabilityStatistics+1·Captain: mikedeng1

Foundations of Machine Learning XIII: The Johnson-Lindenstrauss LemmaTextbook

High-dimensional data is often computationally expensive to work with and hard to visualize. The Johnson-Lindenstrauss lemma answers a striking question in this setting: can any finite set of points, no matter how high-dimensional the ambient space, be squeezed into a space of dimension depending only on the number of points (logarithmically) and the…

6 thms2 active usersReviewed
🏆Completed
Mechanism DesignTheoretical Computer Science·Captain: Shuze Chen

Algorithmic Game Theory III: Arrow and Gibbard–SatterthwaiteTextbook

Before a mechanism can pay anyone, it must decide something — and the impossibility theorems of social choice say that deciding honestly is already hard. Arrow's theorem (1951) showed that any method of aggregating individual rankings into a social ranking that respects unanimity and independence of irrelevant alternatives must be a dictatorship; Gibbard…

4 thms2 active usersReviewed
🏆Completed
Algorithmic Game TheoryTheoretical Computer Science·Captain: Shuze Chen

Algorithmic Game Theory II: No-Regret Learning and Correlated EquilibriaTextbook

Equilibrium concepts are static; play is dynamic. The bridge between the two is regret minimization: simple adaptive rules that, against arbitrary — even adversarial — opponents, perform nearly as well as the best fixed alternative in hindsight. The subject begins with Hannan (1957) and Blackwell (1956), whose consistency theorems predate most of…

7 thms2 active usersReviewed
🏆Completed
CombinatoricsProbabilityTheoretical Computer Science·Captain: sr

Erdős (1947): The Probabilistic Ramsey Lower BoundResearch Paper

Ramsey theory asks for the smallest number R(k)R(k)R(k) such that every graph on R(k)R(k)R(k) vertices contains either a clique of size kkk or an independent set of size kkk. Beyond being one of the oldest problems in extremal combinatorics, Ramsey numbers sit at the junction of combinatorics, probability, and computer science: the two-coloring of edges they quantify is…

5 thms2 active usersReviewed
🏆Completed
Theoretical Computer Science·Captain: wenxinzhang

Primal-Dual Online Load Balancing on Unrelated MachinesTextbook

Fix m≥1m \ge 1m≥1 machines and nnn jobs arriving one at a time in the order 0,…,n−10, \dots, n-10,…,n−1. Job iii carries a whole vector of nonnegative loads p~(i,j)\tilde p(i,j)p~​(i,j), one per machine, with no assumed relationship between the entries — the same job may be cheap on one machine and unplaceable on another. This is the unrelated machines model. When job iii arrives its load vector…

10 thms2 active usersReviewed
🏆Completed
Complexity TheoryTheoretical Computer Science·Captain: marwahaha

A 2o(n)2^{o(n)}2o(n) Time Algorithm for 3-SAT: Refuting ETHResearch Paper

The Exponential Time Hypothesis (ETH) asserts that deciding whether a Boolean formula with at most three literals per clause has a satisfying assignment requires a positive exponential rate in its number of variables. It is a benchmark assumption in computational complexity. The paper A 2o(n)2^{o(n)}2o(n) Time Algorithm for 3-SAT, attributed to Claude (Anthropic),…

8 thms1 active userReviewed
🏆Completed
Theoretical Computer Science·Captain: kmehltretter82

Exponential lower bounds for Cunningham’s ruleResearch Paper

A local improvement algorithm can reach an optimum without coming close to doing so quickly. A pivot rule chooses the next neighboring solution of a linear program. Cunningham’s rule uses a fixed cyclic order and remembers the last variable selected. It resumes its scan from that variable, choosing the first eligible entering variable. Avis and Friedmann…

13 thms1 active userReviewed
🏆Completed
Formal VerificationTheoretical Computer Science·Captain: pitimespi

OpenSearch cluster coordination: randomized election timersTextbook

When an OpenSearch cluster has no cluster-manager, every cluster-manager-eligible node in candidate mode that has discovered enough peers to form an election quorum (or has just bootstrapped the cluster) starts an election scheduler (ElectionSchedulerFactory), which fires at random intervals; each firing starts a new pre-voting round if the node is still a…

8 thms1 active userReviewed
🏆Completed
Formal VerificationTheoretical Computer Science·Captain: pitimespi

OpenSearch cluster coordination: progress under a stable periodTextbook

The safety mission proves that OpenSearch's cluster coordination never forks, whatever the network does: messages lost, duplicated, delayed or reordered, nodes restarting. Progress cannot be proved in that generality. In that model a message may never be delivered, and nothing stops candidates from starting elections in ever higher terms, each start-join…

7 thms1 active userReviewed
🏆Completed
Formal VerificationTheoretical Computer Science·Captain: pitimespi

OpenSearch cluster coordination: safety of the Zen2 consensus protocolTextbook

An OpenSearch cluster keeps its metadata in one cluster state that an elected node, the cluster-manager, publishes to the others. Every node runs the per-node consensus state machine CoordinationState, transcribed and specified in the OpenSearchCoordination mission, driven by the Coordinator over a network that loses, duplicates, delays and reorders…

45 thms1 active userReviewed
🏆Completed
Formal VerificationTheoretical Computer Science·Captain: pitimespi

OpenSearch cluster coordination: pre-voting and election schedulingTextbook

In OpenSearch's cluster coordination a node starts an election by sending StartJoinRequests for a new term, and every node that handles one moves to that term (CoordinationState.handleStartJoin, transcribed in the per-node mission) and discards its election and publication state: a leader that handles one is no longer leader. A node that started elections…

11 thms1 active userReviewed
🏆Completed
Formal VerificationTheoretical Computer Science·Captain: pitimespi

OpenSearch cluster coordination: the per-node consensus state machine (CoordinationState)Textbook

OpenSearch (and Elasticsearch since 7.0) keeps the metadata of a cluster — which indices exist, their mappings and settings, which node holds which shard — in a single cluster state that one elected node, the cluster-manager (formerly "master"), publishes to all others. The algorithm that elects the cluster-manager and makes every published state durable is…

19 thms1 active userReviewed
🏆Completed
Quantum Information·Captain: marwahaha

Quantum Max-Cut: 0.5950.5950.595 energy estimationResearch Paper

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

26 thms1 active userReviewed
🏆Completed
Quantum Information·Captain: marwahaha

Quantum Max-Cut: 0.6030.6030.603 energy estimationResearch Paper

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

25 thms1 active userReviewed
PreviousPage 22 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