Proving Bounds for the Randomized Maxcut Approximation Algorithm in Lean4

I’m interested by this recent development where people are using LLMs with Lean to prove things that haven’t been formalized yet. This seems like a really good fit for LLMs. They’re good at translating approximate language to formal language, they’re good at information retrieval, and any failures are mitigated by Lean itself. I haven’t tried it, but I imagine failure modes might be proving useless lemmas along the way, taking a needlessly roundabout approach, or inadvertently proving something different than what you set out to do.

Nice! I'd imagine that defining a cut as simply a partition of the vertices (rather than a subset of edges) may simplify things slightly.

Nice intro challenge