Published on: 2025-12-19
Proving bounds for the Randomized MaxCut Approximation algorithm in Lean4
For a given graph G = (V, E) , a cut C is a set of edges such that there is a partition V = (A, B) where all edges e ∈ C have one vertex in A and the other in B .
MaxCut is a very famous combinatorial optimization problem wherein we want to find the largest such cut. This is useful in scheduling, partitioning, financial portfolio optimization, and more! While the problem itself is NP-Complete, there exist a host of approximation algorithms that allow us to do “pretty good” in practice. To see a careful treatment of deterministic MaxCut algorithms, check out these two lecture notes.
Some quick nomenclature: an α-approximation for a (maximization/minimization) problem is when we:
(max) Do as good as 1/α * OPT (min) Do as good as α * OPT
For our purposes, lets say we don’t even care about doing good right now, just that we care about doing good in expectation. That is, while there exists a 1/2-approximation for MaxCut, we want to create an algorithm such that the expected size of our output cut satisfies the 1/2 approximation ratio.
Our simple algorithm
For every vertex v ∈ V = (A, B) , choose with 50% probability whether it is in A or B . That’s it, that creates the cut.
Good job! Take a well-deserved break now.
... continue reading