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

176–200 of 478
Open104Completed478All582
🏆Completed
Machine LearningOperations ResearchTheoretical Computer Science·Captain: mikedeng1

The Weighted Majority Algorithm 4: The Continuous Master WMC Has Total Absolute Loss at Most ln(w_init/w_fin)/(1−β)Research Paper

In sequential prediction, several forecasters can issue different answers for the same instance. A master algorithm must combine their advice before the true label is known. Littlestone and Warmuth's Weighted Majority framework gives worst-case guarantees for this setting: the instances and labels need not come from a probability distribution. The paper…

6 thms3 active usersReviewed
🏆Completed
Complexity TheoryProbabilityQuantum Information+1·Captain: mikedeng1

Strengths and Weaknesses of Quantum Computing II: Relative to a Random Permutation, a Quantum Algorithm Needs Ω(2^{n/3}) Queries to Decide the First Bit of A⁻¹(1ⁿ)Research Paper

An oracle lets an algorithm ask for the value of a function without giving it a description of that function. An oracle lower bound isolates how many questions are needed, even when computation between questions is unrestricted. Bennett, Bernstein, Brassard and Vazirani used this viewpoint to compare classical and quantum access to randomly chosen functions…

10 thms3 active usersReviewed
🏆Completed
CombinatoricsLinear OptimizationOperations Research+1·Captain: mikedeng1

Approximation Algorithms for Scheduling Unrelated Parallel Machines 2: Enumerating Long Assignments and Rounding the LP Gives a (1 + ε)-Approximation for MakespanResearch Paper

Scheduling independent jobs on unrelated parallel machines to minimize the makespan is one of the basic NP-hard problems of scheduling theory: each job has its own processing time on each machine, with no relation between machines, and the goal is to finish all jobs as early as possible. When the number of machines is part of the input, Lenstra, Shmoys and…

10 thms3 active usersReviewed
🏆Completed
Graph TheoryLinear OptimizationTheoretical Computer Science·Captain: mikedeng1

Multicommodity Max-Flow Min-Cut Theorems and Their Use in Designing Approximation Algorithms III: Every Directed Uniform Multicommodity Flow Problem Has Ω(𝒮/log n) ≤ f ≤ 𝒮Research Paper

Many graph problems in routing, VLSI layout and scheduling ask for a cut that separates a lot of demand while cutting little capacity. For a single commodity, the max-flow min-cut theorem of Ford and Fulkerson says that the largest flow equals the smallest cut. For several commodities sharing one network this equality fails, and the question becomes how far…

8 thms3 active usersReviewed
🏆Completed
Graph TheoryLinear OptimizationTheoretical Computer Science·Captain: mikedeng1

Multicommodity Max-Flow Min-Cut Theorems and Their Use in Designing Approximation Algorithms II: Every Product Multicommodity Flow Problem with k Commodities Has Ω(𝒮/log k) ≤ f ≤ 𝒮Research Paper

For a single commodity, the Ford–Fulkerson theorem says that the maximum flow between two nodes equals the minimum capacity of a cut separating them. Many routing and partitioning problems involve many source–sink pairs at once, and for those the equality fails: the largest fraction of every demand that can be routed simultaneously can be strictly smaller…

8 thms3 active usersReviewed
🏆Completed
CombinatoricsComplexity TheoryProbability+1·Captain: mikedeng1

Software Protection and Simulation on Oblivious RAMs: Every Oblivious Simulation of t Steps Makes max{|y|, Ω(t log t)} AccessesResearch Paper

Programs often reveal information through the memory locations they touch, even when the contents of those locations are hidden. An oblivious RAM simulation aims to conceal this access pattern. Goldreich and Ostrovsky studied the cost of doing so for arbitrary RAM programs and showed that the access sequence itself imposes a lower bound on simulation…

7 thms3 active usersReviewed
🏆Completed
Algorithmic Game TheoryOperations ResearchOptimization+1·Captain: mikedeng1

Assortment Optimisation Under a General Discrete Choice Model: A Tight Analysis of Revenue-Ordered Assortments IV: Uniform Pricing Earns OPT/(1 + ln(v_m/v_1)) in Unit-Demand Min-PricingResearch Paper

A seller with nnn distinct items faces mmm consumers, each of whom wants at most one item. Choosing item prices to maximise revenue in this setting is the unit-demand envy-free pricing problem, introduced by Rusmevichientong and studied in algorithmic game theory and revenue management since the mid-2000s. Optimal prices are hard to compute in general, so the…

13 thms3 active usersReviewed
🏆Completed
CombinatoricsNumber TheoryProbability+1·Captain: mikedeng1

A New Class of Random Number Generators 1: For Prime m = bʳ + bˢ − 1, Every Nontrivial Add-with-Carry Sequence Is Periodic After r Steps, with Period the Order of b mod mResearch Paper

Simulation, Monte Carlo integration and randomized algorithms consume long streams of numbers that should behave like independent uniform draws. A deterministic generator with finite state is eventually periodic, so its period is the first figure of merit: a stream cannot be longer than its cycle. G. Marsaglia and A. Zaman, A new class of random number…

17 thms3 active usersReviewed
🏆Completed
Machine LearningOperations ResearchTheoretical Computer Science·Captain: mikedeng1

The Weighted Majority Algorithm 2: On Any Partition into Segments, WML Makes at Most Σ min(l_i, (log(n/(βγ)) + m_i log(1/β))/log(1/u)) MistakesResearch Paper

Prediction with expert advice asks a master algorithm to combine the binary predictions of a pool of nnn prediction algorithms, trial after trial, so that it makes few more mistakes than the best member of the pool, without any probabilistic assumption on the data. Littlestone and Warmuth's Weighted Majority Algorithm WM (Littlestone and Warmuth 1994) keeps a…

4 thms3 active usersReviewed
🏆Completed
AlgebraNumber TheoryTheoretical Computer Science·Captain: mikedeng1

Factoring Polynomials with Rational Coefficients III: A Reduced Basis of the Lattice of Multiples of h mod p^k Finds the Irreducible Factor h₀ = gcd(b₁, …, b_t)Research Paper

Factoring a polynomial with rational coefficients into irreducible factors is one of the basic tasks of computer algebra. Before 1982 the standard method (Berlekamp's algorithm modulo a small prime, Hensel lifting, then recombination of the ppp-adic factors, as in Zassenhaus's approach) could take exponential time, because the number of ways to recombine…

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

Packet Routing and Job-Shop Scheduling in O(Congestion + Dilation) Steps: Edge-Simple Paths with Congestion c and Dilation d Admit an O(c + d)-Step Schedule with Constant-Size QueuesResearch Paper

In a store-and-forward network, messages are cut into packets that travel from node to node along wires, one wire per time step, and wait in buffers between moves. Routing such traffic splits into two problems: choosing a path for each packet, and scheduling the packets along their paths, deciding at every step which packets move and which wait. Leighton,…

10 thms3 active usersReviewed
🏆Completed
CombinatoricsOperations ResearchTheoretical Computer Science·Captain: mikedeng1

Flowshop and Jobshop Schedules: Complexity and Approximation 2: The 3-Partition Flow Shop on Three Machines Has a Preemptive Schedule of Finish Time 2tB Iff a 3-Partition ExistsResearch Paper

A flow shop is the simplest multi-stage production model: every job passes through the same machines in the same order, and the question is how to sequence the work so that everything is finished as early as possible. Gonzalez and Sahni's 1978 paper in Operations Research settled the computational complexity of the preemptive version of this problem, in…

8 thms3 active usersReviewed
🏆Completed
CombinatoricsOperations ResearchProbability+1·Captain: mikedeng1

An Optimal Algorithm for On-line Bipartite Matching 2: No Randomized On-line Algorithm Guarantees an Expected Matching Larger Than n(1 − 1/e) + o(n)Research Paper

An online matching algorithm must commit to each assignment when a request arrives, before it sees later requests. This limitation arises whenever waiting for the full instance is impossible: an available resource can be assigned to a current request or saved for an unknown future request. The quality of the assignment is measured by how many requests can…

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

Online Stochastic Matching: Beating 1-1/e 3: No Online Algorithm Beats Expected Approximation Factor 26/27 on a 6-Cycle, and None Reaches 1 − o(1) on Disjoint 6-CyclesResearch Paper

Online bipartite matching asks an algorithm to assign arriving requests to resources it cannot reassign later. In display advertising, the requests are page views (impressions) and the resources are advertisers who have bought a fixed number of impressions in advance; each impression must be served immediately or lost. In the adversarial model, Karp,…

5 thms3 active usersReviewed
🏆Completed
CombinatoricsOperations ResearchProbability+1·Captain: mikedeng1

Online Stochastic Matching: Beating 1-1/e 2: The Suggested Matching Algorithm Achieves 1 − 1/e with High Probability, and This Is Tight Even in ExpectationResearch Paper

Online bipartite matching models decisions that must be made as requests arrive: an advertiser can be assigned to a compatible request once, and an assignment cannot be revised when later requests reveal a better alternative. Display advertising is the motivating example in Feldman, Mehta, Mirrokni, and Muthukrishnan's 2009 preprint: an ad server knows…

12 thms3 active usersReviewed
🏆Completed
CombinatoricsLinear OptimizationOperations Research+1·Captain: mikedeng1

Online Primal-Dual Algorithms for Covering and Packing 3: A Deterministic O(log d log(n/OPT))-Competitive Algorithm for Online Unweighted Set CoverResearch Paper

Online set cover is the basic covering problem in which the requests arrive over time. A ground set of elements and a family of sets are known in advance, but which elements must be covered is revealed one element at a time, and each arriving element has to be covered at once by a set chosen irrevocably. The problem models resource placement under unknown…

10 thms3 active usersReviewed
🏆Completed
CombinatoricsOperations ResearchTheoretical Computer Science·Captain: mikedeng1

On the Approximability of Single-Machine Scheduling with Precedence Constraints 2: Every Convex Bipartite Order Has a Realizer of Size 3Research Paper

The single-machine scheduling problem 1∣prec∣∑wjCj1|\mathrm{prec}|\sum w_j C_j1∣prec∣∑wj​Cj​ asks for an order in which to process nnn jobs, each with a processing time and a weight, on one machine, respecting a partial order of precedence constraints, so that the weighted sum of completion times is as small as possible. It is NP-hard, and the best known approximation ratio for…

7 thms3 active usersReviewed
🏆Completed
CombinatoricsGraph TheoryTheoretical Computer Science·Captain: mikedeng1

On the Approximability of Single-Machine Scheduling with Precedence Constraints 3: The Incomparable-Pairs Graphs of Canonical Interval Orders Have Unbounded Chromatic NumberResearch Paper

Single-machine scheduling with precedence constraints asks for an order in which one machine processes jobs while respecting prescribed comparisons between them. For the objective of minimizing total weighted completion time, the structure of the precedence order can influence the quality of approximation algorithms. Ambühl, Mastrolilli, Mutsanas, and…

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

Online Primal-Dual Algorithms for Covering and Packing 1: The Online Fractional Packing Scheme Is B-Competitive and Violates Each Packing Constraint by at Most 2 log(1 + n·a_i(max)/a_i(min))/BResearch Paper

Many resource-allocation problems arrive one request at a time and must be answered immediately: a bandwidth request is admitted or refused when it appears, an advertiser's budget is charged when a query arrives, a job is accepted before later jobs are seen. Their linear-programming relaxations are packing problems: maximize a total profit subject to…

8 thms3 active usersReviewed
🏆Completed
CombinatoricsGraph TheoryOperations Research+1·Captain: mikedeng1

On the Approximability of Single-Machine Scheduling with Precedence Constraints 1: A k-Fold Realizer of Size t Yields a Vertex Cover of Expected Weight at Most (2 − 2/(t/k)) Times OptimalResearch Paper

Single-machine scheduling with precedence constraints, written 1∣prec∣∑wjCj1|\mathrm{prec}|\sum w_jC_j1∣prec∣∑wj​Cj​ in the notation of Graham et al., asks for an order of nnn weighted jobs on one machine that respects a given partial order and minimizes the weighted sum of completion times. The problem is strongly NP-hard (Lawler 1978; Lenstra and Rinnooy Kan 1978), and closing its…

10 thms3 active usersReviewed
🏆Completed
Operations ResearchProbabilityStochastic Systems+1·Captain: mikedeng1

Approximation Algorithms for Stochastic Inventory Control Models 1: The Dual-Balancing Policy Costs at Most Twice the OptimumResearch Paper

Periodic-review inventory control with backorders is one of the basic models of operations research: in each period a manager decides how much to order, orders arrive after a lead time, unmet demand is backlogged at a penalty, and stock left over is charged a holding cost. When demands in different periods are independent, dynamic programming yields an…

6 thms3 active usersReviewed
🏆Completed
Information TheoryQuantum InformationTheoretical Computer Science·Captain: mikedeng1

Shadow Tomography of Quantum States 3: Shadow Tomography Needs Ω(min{D², log M}/ε²) CopiesResearch Paper

A mixed state of a DDD-dimensional quantum system is a D×DD\times DD×D positive semidefinite matrix ρ\rhoρ of trace 111. Writing ρ\rhoρ down takes about D2D^2D2 real numbers, and DDD is exponential in the number of qubits, so learning ρ\rhoρ in full is expensive. Holevo's theorem and the random access code bounds of Ambainis, Nayak, Ta-Shma and Vazirani say that an nnn-qubit state…

16 thms3 active usersReviewed
🏆Completed
CombinatoricsOperations ResearchOptimization+2·Captain: mikedeng1

A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization 2: Randomized Double Greedy Achieves 1/2 of the Optimum in ExpectationResearch Paper

Many selection problems assign a value to each subset of a finite collection: the coverage supplied by chosen facilities, the influence reached by chosen seeds, or the value of a coalition. A submodular set function has diminishing returns in the precise sense that the combined value of two sets, counting their overlap once, does not exceed the sum of their…

11 thms3 active usersReviewed
🏆Completed
Operations ResearchProbabilityStochastic Systems+1·Captain: mikedeng1

Approximation Algorithms for Stochastic Inventory Control Models 2: The Triple-Balancing Policy Costs at Most Three Times the Optimum for Stochastic Lot-SizingResearch Paper

Periodic-review inventory control with a fixed ordering cost is one of the oldest problems in operations research. A firm reviews its stock at the beginning of each of TTT periods, decides whether to place an order, pays a fixed cost KKK for every order it places, and pays holding costs on leftover stock and penalties on unmet (backlogged) demand. When demand…

7 thms3 active usersReviewed
🏆Completed
CombinatoricsGraph TheoryOperations Research+2·Captain: mikedeng1

Secretary Problems: Weights and Discounts 5: A 3e-Competitive Algorithm for the Graphic Matroid Secretary ProblemResearch Paper

In the secretary problem, nnn items with nonnegative values arrive one at a time in a uniformly random order, and an online algorithm must decide on each arrival, irrevocably, whether to keep it. The classical version keeps one item; the rule that observes a 1/e1/e1/e fraction of the arrivals and then takes the first item better than everything seen picks the best…

10 thms3 active usersReviewed
PreviousPage 8 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