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

76–100 of 478
Open104Completed478All582
🏆Completed
CombinatoricsGraph TheoryTheoretical Computer Science·Captain: mikedeng1

Generation and Properties of Snarks 3: A Snark on 26 Vertices All of Whose 2-Factors Consist of Odd Cycles Refutes the Abreu–Labbate–Sheehan ConjectureResearch Paper

A cubic graph has chromatic index 3 or 4 (Vizing). Cubic graphs of chromatic index 4 — the uncolourable ones — are where most of the open problems on cubic graphs live: a minimal counterexample to the cycle double cover conjecture or to Tutte's 5-flow conjecture would be among them. Uncolourable graphs with small edge cuts or short cycles reduce to smaller…

12 thms4 active usersReviewed
🏆Completed
Complexity TheoryLinear OptimizationTheoretical Computer Science·Captain: mikedeng1

The Power of the Combined Basic LP and Affine Relaxation for Promise CSPs I: BLP+Affine Correctly Solves Every PCSP with Symmetric Polymorphisms of Arbitrarily Large AritiesResearch Paper

A constraint satisfaction problem (CSP) asks whether variables can be assigned values from a finite domain so that every constraint, drawn from a fixed list of allowed relations, is satisfied. A promise CSP (PCSP) relaxes the question: given two templates A\mathbf AA and B\mathbf BB with a homomorphism A→B\mathbf A\to\mathbf BA→B, distinguish instances satisfiable in …

11 thms4 active usersReviewed
🏆Completed
CombinatoricsGraph TheoryTheoretical Computer Science·Captain: mikedeng1

Generation and Properties of Snarks 2: A Cyclically 5-Edge-Connected Permutation Snark on 34 Vertices Refutes Zhang's Conjecture That Only the Petersen Graph Is OneResearch Paper

A snark is a cubic graph that cannot be properly edge-coloured with three colours and that does not reduce to a smaller such graph. Snarks are the smallest possible counterexamples to several central conjectures about cubic graphs, among them the cycle double cover conjecture, Tutte's 5-flow conjecture and the Berge–Fulkerson conjecture, so structural…

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

A Learning Theory Approach to Non-Interactive Database Privacy 1: The Net Mechanism Is (α, δ)-Useful for Every Class of Counting Queries with Error Governed by Its VC-DimensionResearch Paper

A data curator holds a database of nnn individual records and wants to publish something from which many statistics can be computed, while guaranteeing differential privacy: no single record should noticeably change what is published (Dwork, McSherry, Nissim, Smith 2006). Interactive mechanisms answer queries one at a time and add noise to each answer, so…

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

Matroid Prophet Inequalities 1: Against Any Online Weight-Adaptive Adversary, the 2-Balanced Threshold Algorithm Earns at Least Half the Expected Max-Weight BasisResearch Paper

The prophet inequality of optimal stopping compares a gambler, who sees independent non-negative random values X1,…,XnX_1, \dots, X_nX1​,…,Xn​ one at a time and must accept or reject each on arrival, with a prophet who sees them all in advance. Krengel, Sucheston and Garling showed that the gambler can secure E[Xτ]≥12 E[max⁡iXi]\mathbb E[X_\tau] \ge \tfrac12\,\mathbb E[\max_i X_i]E[Xτ​]≥21​E[maxi​Xi​], and…

16 thms4 active usersReviewed
🏆Completed
Operations ResearchOptimizationTheoretical Computer Science·Captain: mikedeng1

Optimal Inapproximability Results for MAX-CUT and Other 2-Variable CSPs? 2: Random-Hyperplane Rounding Approximates Balanced MAX-2SAT within β ≈ 0.943Research Paper

MAX-2SAT asks for an assignment of Boolean variables that maximizes the total weight of satisfied clauses, each clause being a disjunction of two literals. It is one of the basic constraint satisfaction problems of approximation theory, and its approximability has been studied alongside MAX-CUT since semidefinite programming entered the field.

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

AdWords and Generalized On-line Matching II: No Randomized Online Algorithm for b-Matching Has Competitive Ratio Better Than 1 − 1/e, for Every Budget bResearch Paper

Search engines sell advertising slots query by query. Each advertiser states a bid per keyword and a daily budget; queries arrive one at a time, and the engine must assign each to an advertiser immediately, without knowing which queries will come later. Mehta, Saberi, Vazirani and Vazirani (J. ACM 2007) called this the adwords problem and gave a…

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

On the (Im)possibility of Obfuscating Programs 3: A Random Injection G : [K] → [L], L ≥ K², Fools Every K^δ-Query Distinguisher with Oracle G up to 1/K^δ, Except with Probability 2^(−K^δ)Research Paper

Barak, Goldreich, Impagliazzo, Rudich, Sahai, Vadhan and Yang proved that general-purpose program obfuscation in the virtual black-box sense is impossible (J. ACM 59(2), 2012). A natural question is whether the impossibility proof relativizes, that is, whether it survives when every party gets access to the same oracle. Proposition 4.14 of the paper shows…

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

Projection moments, positive cap domination, and Riesz estimates on the sphereResearch Paper

A linear projection can concentrate a measure even when the measure has no atoms; how much depends on how much mass sits near the affine subspaces that the projection collapses. Quantitative versions of this principle go back to the potential-theoretic projection method of Kaufman and Mattila, which relates ball-growth bounds ν(B(x,r))≤Krβ\nu(B(x,r)) \le K r^\betaν(B(x,r))≤Krβ to…

52 thms4 active usersReviewed
🏆Completed
CombinatoricsDiscrete GeometryTheoretical Computer Science·Captain: wurtle

The Euclidean Steinitz–Bergström theoremResearch Paper

Given vectors v1,…,vNv_1,\dots,v_Nv1​,…,vN​ in the Euclidean unit ball of Rd\mathbb R^dRd that sum to zero, can they always be reordered so that every partial sum stays in a ball whose radius depends only on ddd? Steinitz's lemma, from his work on rearrangements of conditionally convergent vector series, says yes: in any norm, radius ddd suffices (Grinberg–Sevast'yanov 1980). For…

9 thms4 active usersReviewed
🏆Completed
Dynamical SystemsOperations ResearchStochastic Systems+1·Captain: mikedeng1

The Power of Two Choices in Randomized Load Balancing I: In the Limiting Supermarket System the Expected Time Converges to T_d(λ) = Σ λ^((d^i−d)/(d−1))Research Paper

Randomized load balancing asks how much a dispatcher gains from a little information. In the supermarket model, jobs arrive at nnn servers and each job inspects a few servers chosen at random before joining one. With one random choice every server is an independent M/M/1 queue, and the expected time a job spends in the system is 1/(1−λ)1/(1-\lambda)1/(1−λ) at load λ\lambdaλ.…

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

On Lattices, Learning with Errors, Random Linear Codes, and Cryptography 1: A Discrete Gaussian on L + u Plus Continuous Gaussian Noise ν_s Is Within Statistical Distance 4ε of ν_t, t = √(r² + s²)Research Paper

The learning with errors (LWE) problem underlies most of post-quantum public-key cryptography. Its hardness rests on Regev's reduction from worst-case lattice problems to LWE (Regev, J. ACM 2009). The reduction is iterative: it repeatedly turns samples of a discrete Gaussian on a lattice into samples of a narrower one. Its classical step, Lemma 3.11, needs…

11 thms4 active usersReviewed
🏆Completed
Number TheoryProbabilityTheoretical Computer Science·Captain: mikedeng1

On Lattices, Learning with Errors, Random Linear Codes, and Cryptography 5: If Every χ^⋆k Is Below ⌊p/2⌋/2 with Probability > 1 − δ, the Cryptosystem Decrypts Correctly with Probability ≥ 1 − δResearch Paper

Learning with errors (LWE) asks to recover a secret vector s∈Zpns \in \mathbb Z_p^ns∈Zpn​ from noisy inner products (ai,⟨ai,s⟩+ei)(a_i, \langle a_i, s\rangle + e_i)(ai​,⟨ai​,s⟩+ei​), where the aia_iai​ are uniform and the errors eie_iei​ are drawn from a narrow distribution χ\chiχ on Zp\mathbb Z_pZp​. Regev introduced the problem and showed that solving it is at least as hard as solving worst-case lattice problems…

5 thms4 active usersReviewed
🏆Completed
Machine LearningOperations ResearchTheoretical Computer Science·Captain: mikedeng1

The Weighted Majority Algorithm 9: With η Anomalies Every Randomized Learner Can Be Forced to ½ opt(F, 0) + η Expected MistakesResearch Paper

Prediction with expert advice asks a learner to predict a binary label on each of a sequence of trials, after seeing the predictions of a pool of candidate functions, and to make few more mistakes than the best member of the pool. Littlestone and Warmuth's The Weighted Majority Algorithm (Inform. and Comput. 108, 1994) gave the deterministic algorithm WM…

7 thms4 active usersReviewed
🏆Completed
AlgebraInformation TheoryTheoretical Computer Science·Captain: mikedeng1

Fuzzy Extractors: How to Generate Strong Keys from Biometrics and Other Noisy Data 3: Shingling plus PinSketch Gives an Average-Case Secure Sketch for Edit DistanceResearch Paper

Biometric readings, physical unclonable functions and typed passphrases share two defects as cryptographic keys: they are not uniformly distributed, and they are never reproduced exactly. Dodis, Ostrovsky, Reyzin and Smith (SIAM J. Comput. 38(1), 2008; preprint arXiv:cs/0602007v4) introduced the secure sketch to handle the second defect without destroying…

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

Fast Approximation Algorithms for Fractional Packing and Covering Problems 2: An ε-Relaxed Decision Procedure for Fractional Covering Using O(m + ρ log² m + ε⁻²ρ log(m/ε)) Oracle CallsResearch Paper

Many linear programs that arise in combinatorial optimization ask only whether a convex set contains a point satisfying a family of nonnegative linear constraints. In the fractional covering problem the constraints have the form Ax≥bAx\ge bAx≥b with A≥0A\ge 0A≥0: the fractional relaxation of set cover, the Held–Karp lower bound for the travelling salesman problem, and…

10 thms4 active usersReviewed
🏆Completed
CombinatoricsNumber TheoryProbability+1·Captain: mikedeng1

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

A pseudorandom number generator replaces repeated random sampling with a deterministic update of a small state. Its useful lifetime depends on the length and structure of the resulting orbit. In Marsaglia and Zaman’s 1991 paper, the subtract-with-borrow generators use only digit subtraction and a one-bit borrow while attaining cycles that can be almost as…

17 thms4 active usersReviewed
🏆Completed
Linear algebraNumber TheoryTheoretical Computer Science·Captain: mikedeng1

Factoring Polynomials with Rational Coefficients II: The Basis Reduction Algorithm Terminates and Returns a Reduced Basis of the LatticeResearch Paper

A lattice is the set of integer combinations of nnn linearly independent vectors in Rn\mathbb R^nRn. Many computational problems — factoring polynomials over Q\mathbb QQ, simultaneous diophantine approximation, integer programming in fixed dimension, breaking knapsack cryptosystems, and the analysis of lattice-based cryptography — reduce to finding a good basis of…

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

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

A multicommodity flow problem asks to route several commodities simultaneously through a capacitated network, each from its own source to its own sink. For a single commodity, the max-flow min-cut theorem of Ford and Fulkerson says that the largest routable flow equals the capacity of the smallest separating cut. For many commodities the natural analogue…

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

Multicommodity Max-Flow Min-Cut Theorems and Their Use in Designing Approximation Algorithms IV: A Uniform Flow of Size Ω(𝒮/log n) on Paths of Length O(C_max log n/(n𝒮))Research Paper

Communication networks must route many source–destination demands through shared edges. A multicommodity flow describes how much of each demand can be carried simultaneously without exceeding an edge's capacity. In an undirected network, a cut bounds the traffic that can pass between two groups of vertices, but many commodities can interfere even when no…

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

Quick Approximation to Matrices and Applications I: Every Real Matrix Is a Sum of at Most 1/ε² Cut Matrices plus an Error W with |W(S,T)| ≤ ε√(|S||T|)‖A‖_FResearch Paper

Many dense combinatorial optimization problems (Max-Cut, graph bisection, quadratic assignment on dense instances) have objective functions that are sums of matrix entries over rectangles S×TS\times TS×T. If a matrix can be replaced by a simple surrogate that agrees with it on every rectangle up to a small error, such problems can be solved approximately on the…

5 thms4 active usersReviewed
🏆Completed
Computational GeometryDiscrete GeometryTheoretical Computer Science·Captain: mikedeng1

An Optimal Algorithm for Approximate Nearest Neighbor Searching in Fixed Dimensions: Priority Search in a BBD-Tree Visits at Most ⌈1 + 6d/ε⌉^d Leaf CellsResearch Paper

Nearest neighbor searching asks for a data structure that stores nnn points S⊂RdS\subset\mathbb R^dS⊂Rd and, given a query point qqq, returns a point of SSS closest to qqq. It underlies classification, vector quantization, data compression, pattern recognition and similarity search in databases. In dimension d≥3d\ge 3d≥3, exact methods either use space growing like …

8 thms4 active usersReviewed
🏆Completed
CombinatoricsMachine LearningOperations Research+1·Captain: mikedeng1

The Weighted Majority Algorithm 7: On a Class Shattered by Its Domain, Every Deterministic Learner's Mistake Bounds Satisfy Σ 2^(−M_i) < 2Research Paper

An online learner predicts a binary label for each instance before seeing that instance's correct label. Its guarantee is usually measured by its worst possible number of mistakes against a target function. Such guarantees can differ greatly across target functions: an algorithm might learn one target quickly while taking much longer on another. Littlestone…

5 thms4 active usersReviewed
🏆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
PreviousPage 4 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