Proving Bounds for the Randomized MaxCut Approximation Algorithm in Lean4
62 points by todsacerdoti
by sevensor
0 subcomment
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.
by bo1024
0 subcomment
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.
Hacker News