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.

478 completed missions

Missions

1–25 of 478
Open104Completed478All582
🏆Completed
Theoretical Computer Science·Captain: marwahaha

More Asymmetry Bound: omega < 2.37134Research Paper

The matrix-multiplication exponent measures how the arithmetic complexity of multiplying square matrices grows with the ir dimension. Known upper bounds come from constructing large independent matrix products inside tensor powers whose asymptotic rank is controlled. Improving the extraction, rather than finding a lower-rank starting tensor, has driven…

169 thms12 active usersReviewed
🏆Completed
Theoretical Computer Science·Captain: marwahaha

Duan–Wu–Zhou Fourth-Power Bound: omega < 2.37193Research Paper

The matrix-multiplication exponent measures how the arithmetic cost of multiplying square matrices grows with their dimension. An improvement in this exponent is relevant both to algebraic complexity and to algorithms whose running times depend on matrix multiplication. This mission formalizes a known improvement using the fourth power of the…

146 thms12 active usersReviewed
🏆Completed
CombinatoricsOperations ResearchTheoretical Computer Science·Captain: mikedeng1

One-Processor Scheduling with Symmetric Earliness and Tardiness Penalties 1: Minimizing the Total Discrepancy from Preferred Times Is NP-CompleteResearch Paper

Scheduling with earliness and tardiness penalties asks for schedules in which a job finishing early is as undesirable as a job finishing late. The model fits production planned for just-in-time delivery, where finished goods held before their due date cost money, and sequences of experiments tied to fixed external events. It departs from classical…

37 thms10 active usersReviewed
🏆Completed
Formal VerificationMathematical LogicTheoretical Computer Science·Captain: Rizwan G Mir

The Cook-Levin Theorem: NP-Completeness of Boolean Satisfiability in Lean 4Research Paper

The Cook-Levin theorem states that CNF SAT is NP-complete. This mission formalizes the theorem over a multi-tape Turing machine model in Lean 4.

175 thms9 active usersReviewed
🏆Completed
Complexity TheoryOperations ResearchTheoretical Computer Science·Captain: mikedeng1

Complexity of Machine Scheduling Problems 5: KNAPSACK Reduces to Two-Machine Flow Shop Makespan with a Release Date or Tree Precedence and to Two- and Three-Machine Job Shop MakespanResearch Paper

In 1975 P. Brucker, J. K. Lenstra and A. H. G. Rinnooy Kan classified a large part of deterministic machine scheduling by computational complexity, using the then new theory of NP-completeness of Cook and Karp. Their report, Complexity of Machine Scheduling Problems (Mathematisch Centrum, Amsterdam, 1975; published in Annals of Discrete Mathematics 1,…

16 thms8 active usersReviewed
🏆Completed
CombinatoricsComplexity TheoryOperations Research+1·Captain: mikedeng1

Scheduling Subject to Resource Constraints: Classification and Complexity I: Unit-Time Chains on Two Identical Machines with One Unit Resource Are Strongly NP-hardResearch Paper

Machine scheduling asks how to assign jobs to machines over time so that a criterion such as the makespan Cmax⁡C_{\max}Cmax​, the time at which the last job completes, is as small as possible. In practice jobs also compete for scarce resources beyond the machines themselves: tools, operators, memory, power. Błażewicz, Lenstra and Rinnooy Kan (DAM 1983) extended the…

46 thms8 active usersReviewed
🏆Completed
Theoretical Computer Science·Captain: marwahaha

Davie–Stothers Fourth-Power Bound: omega < 2.3737Research Paper

The matrix-multiplication exponent ω\omegaω measures the asymptotic arithmetic cost of multiplying square matrices. An upper bound ω<c\omega<cω<c means that, over the field under consideration, two n×nn\times nn×n matrices can be multiplied using O(nc+ε)O(n^{c+\varepsilon})O(nc+ε) field operations for every ε>0\varepsilon>0ε>0. It is a central benchmark in algebraic complexity and controls…

183 thms8 active usersReviewed
🏆Completed
Linear OptimizationOperations ResearchOptimization+1·Captain: mikedeng1

Fast Approximation Algorithms for Fractional Packing and Covering Problems 3: An ε-Relaxed Decision Procedure for the General Problem Ax ≤ b, x ∈ P Using O(ρ²ε⁻² log(mρ/ε)) Oracle CallsResearch Paper

Many linear programs that arise in combinatorial optimization have a few "complicating" constraints Ax≤bAx \le bAx≤b on top of a set PPP over which linear optimization is easy: multicommodity flow, where PPP is a product of single-commodity flow polytopes; scheduling and the Held–Karp bound, where PPP is a polytope of assignments or trees. Plotkin, Shmoys and Tardos…

16 thms7 active users
🏆Completed
Complexity TheoryOperations ResearchOptimization+1·Captain: mikedeng1

Project Scheduling with Time Windows and Scarce Resources IX: Deciding Feasibility with Cumulative Resources Is NP-Complete Even for Acyclic Project NetworksTextbook

Project scheduling with cumulative resources models production and logistics projects in which activities fill and empty storage: an activity withdraws material from an inventory when it starts and deposits its output when it completes, and every inventory must stay between a safety stock and a storage capacity. Neumann, Schwindt and Zimmermann treat this…

29 thms7 active usersReviewed
🏆Completed
CombinatoricsComplexity TheoryGraph Theory+2·Captain: mikedeng1

Scheduling Subject to Resource Constraints: Classification and Complexity II: Unit-Time Jobs on Two Uniform Machines with Unit Resources Are Strongly NP-hardResearch Paper

Machine scheduling asks how to assign jobs to machines over time. In many applications a job also needs additional scarce resources while it runs: a tool, a skilled operator, a memory bank, a channel. Adding such resources can turn a problem with a polynomial algorithm into an NP-hard one. Błażewicz, Lenstra and Rinnooy Kan (DAM 1983) extended the standard…

41 thms7 active usersReviewed
🏆Completed
CombinatoricsOperations ResearchProbability·Captain: Shuze Chen

Online Matching with Stochastic Rewards: Optimal Competitive Ratio via Path-Based Formulation: Optimal competitiveness of generalized perturbed greedyResearch Paper

An allocation decision does not always produce a reward. An advertisement may receive no click, or a recommended product may not be purchased. In online matching with stochastic rewards, a failed offer uses the customer's opportunity but leaves the resource available for a later customer. This distinction changes both the algorithm and the benchmark against…

24 thms6 active usersReviewed
🏆Completed
ProbabilityQuantum InformationTheoretical Computer Science·Captain: mikedeng1

Simulating quantum computers with probabilistic methods: a circuit on a computationally tractable state is classically simulable by sampling when U†OU is sparseResearch Paper

A quantum circuit may create a state whose full list of amplitudes is far too large for a classical computer to store. That fact alone does not show that every observable feature of its output is hard to estimate. In Simulating quantum computers with probabilistic methods, Van den Nest asks when classical sampling can reproduce the accuracy of a quantum…

12 thms6 active usersReviewed
🏆Completed
Quantum InformationTheoretical Computer Science·Captain: mikedeng1

A Meet-in-the-Middle Algorithm for Fast Synthesis of Depth-Optimal Quantum Circuits: Meet-in-the-Middle Search Returns a Minimal-Depth Circuit, Generating Only Circuits of Half the DepthResearch Paper

A quantum algorithm is run as a quantum circuit: a sequence of elementary gates drawn from a fixed instruction set, such as the Hadamard, phase, controlled-NOT and TTT gates. On fault-tolerant hardware every layer of gates costs time and error-correction overhead, so the depth of a circuit, its number of layers, is a primary cost measure. Compilers therefore…

28 thms6 active users
🏆Completed
Complexity TheoryLinear algebraProbability+1·Captain: mikedeng1

Candidate Indistinguishability Obfuscation and Functional Encryption for All Circuits: Garblings of Equivalent Partial Assignments Are O(nT²/p)-Close in the Generic Colored Matrix ModelResearch Paper

An indistinguishability obfuscator (iO) is a compiler that scrambles a program so that any two programs computing the same function become computationally indistinguishable after compilation. Garg, Gentry, Halevi, Raykova, Sahai and Waters gave the first candidate construction for all circuits (SIAM J. Comput. 45(3), 2016; conference version FOCS 2013). The…

12 thms6 active usersReviewed
🏆Completed
Complexity TheoryOperations ResearchOptimization+1·Captain: mikedeng1

Scheduling Problems with Two Competing Agents 6: PARTITION Reduces to Two Agents Each Bounding Their Own Total Completion Time on One MachineResearch Paper

In many production and service settings a single resource is shared by parties with different goals: two departments sending orders to the same machine, two customers of a contract manufacturer, or two classes of requests on one processor. Multi-agent scheduling models this directly. Each agent owns its own jobs and its own objective, and a schedule is…

16 thms6 active usersReviewed
🏆Completed
Complexity TheoryOperations ResearchOptimization+1·Captain: mikedeng1

Scheduling Problems with Two Competing Agents 2: KNAPSACK Reduces to Minimizing One Agent's Total Weighted Completion Time Under a Makespan Bound for the OtherResearch Paper

In many production and logistics settings a single resource is shared by parties with different goals: two departments of a plant that send orders to the same machine, two customers of a contract manufacturer, or two classes of traffic on one processor. Multi-agent scheduling models this directly. Each agent owns its own jobs and its own objective, and a…

14 thms6 active usersReviewed
🏆Completed
Complexity TheoryOperations ResearchTheoretical Computer Science·Captain: mikedeng1

Complexity of Machine Scheduling Problems 4: KNAPSACK Reduces to Single-Machine Total Completion Time with One Release DateResearch Paper

Minimizing the total completion time ∑jCj\sum_j C_j∑j​Cj​ of jobs on a single machine is one of the oldest problems in scheduling theory. When every job is available at time 000, processing the jobs in order of nondecreasing processing time is optimal (the shortest-processing-time rule), so the problem is solved by sorting. Release dates, times before which a job may…

18 thms6 active usersReviewed
🏆Completed
Complexity TheoryOperations ResearchTheoretical Computer Science·Captain: mikedeng1

Complexity of Machine Scheduling Problems 7: Makespan Reduces to Total Completion Time on Identical Machines with Precedence ConstraintsResearch Paper

Scheduling jobs on parallel machines under precedence constraints is the core model of project and parallel-processing scheduling: a job may start only after its predecessors have finished. Two criteria dominate the literature, the makespan Cmax⁡C_{\max}Cmax​ (when does the last job finish?) and the total completion time ∑jCj\sum_j C_j∑j​Cj​ (how long do jobs wait on…

20 thms6 active usersReviewed
🏆Completed
Complexity TheoryGraph TheoryOperations Research+1·Captain: mikedeng1

Complexity of Machine Scheduling Problems 6: DIRECTED HAMILTON PATH Reduces to No-Wait Flow Shop Makespan and Total Completion TimeResearch Paper

In a no-wait flow shop every job passes through the machines M1,…,MmM_1,\dots,M_mM1​,…,Mm​ in the same order, and once it has started it may never wait between two machines. The constraint comes from processes in which the material changes state if it is left standing, such as hot metal rolling, chemical and food processing, and some pharmaceutical lines; see the survey of…

25 thms6 active usersReviewed
🏆Completed
Complexity TheoryOperations ResearchTheoretical Computer Science·Captain: mikedeng1

Complexity of Machine Scheduling Problems 3: KNAPSACK Reduces to Single-Machine Total Weighted TardinessResearch Paper

Minimizing total weighted tardiness on a single machine, written n∣1∣∣∑wjTjn|1||\sum w_jT_jn∣1∣∣∑wj​Tj​, is one of the basic problems of deterministic scheduling. A job that finishes after its due date is penalized in proportion to its lateness and its weight. Practitioners use this criterion to model penalty clauses and customer priority. In the theory it was a reference…

23 thms6 active usersReviewed
🏆Completed
Complexity TheoryOperations ResearchTheoretical Computer Science·Captain: mikedeng1

Complexity of Machine Scheduling Problems 2: KNAPSACK Reduces to Single-Machine Maximum Lateness, Weighted Number of Late Jobs, and Weighted Completion Time with DeadlinesResearch Paper

Deterministic machine scheduling was one of the first application areas of the theory of NP-completeness. After Cook (1971) and Karp (1972) showed that a large family of combinatorial problems are polynomially equivalent, Brucker, Lenstra and Rinnooy Kan set out to locate the boundary between the polynomially solvable and the NP-complete scheduling…

15 thms6 active usersReviewed
🏆Completed
Complexity TheoryOperations ResearchTheoretical Computer Science·Captain: mikedeng1

Complexity of Machine Scheduling Problems 1: PARTITION Reduces to Makespan and to Weighted Completion Time on Two Identical MachinesResearch Paper

Deterministic machine scheduling asks how to process a set of jobs on a set of machines so that an overall criterion, such as the time at which the last job finishes, is as small as possible. In the early 1970s many such problems had efficient algorithms (Johnson's rule for the two-machine flow shop, Smith's ratio rule for a single machine, Lawler's rule…

15 thms6 active usersReviewed
🏆Completed
Machine LearningProbabilityStatistics+1·Captain: mikedeng1

Foundations of Machine Learning VII: On-Line Learning and On-Line-to-Batch ConversionTextbook

Every guarantee in the preceding chapters assumes a fixed distribution and i.i.d. sampling. On-line learning drops both assumptions: an algorithm processes one example at a time, in an adversarial (worst-case) sequence, and is judged by regret against the best fixed comparator in hindsight rather than by generalization error. This chapter develops the…

28 thms6 active users
🏆Completed
Machine LearningProbabilityStatistics+1·Captain: mikedeng1

Foundations of Machine Learning VI: AdaBoost and Margin TheoryTextbook

Weak learning — a base classifier only slightly better than random guessing — is easy to come by; strong learning, in the PAC sense of Chapter 2, is not. Boosting is the technique that turns the first into the second: combine many weak classifiers, each trained on a reweighted version of the sample that emphasizes previously misclassified points, into a…

20 thms6 active usersReviewed
🏆Completed
CombinatoricsGraph TheoryTheoretical Computer Science·Captain: hao jia

Immune High-Girth Bipartite Graphs (Feghali-Lucke-Paulusma-Ries 2025)Research Paper

A matching cut is a vertex bipartition whose crossing edges form a matching. The property was introduced under the name decomposability and has links to graph algorithms, stable cutsets in line graphs, and several graph-labeling problems. An Open Problem Garden question asked whether sufficiently large girth forces a matching cut once average degree is…

20 thms6 active usersReviewed
PreviousPage 1 of 20Next

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