imo, partially because it's still not easy (in terms of code -> formal proof). With AI, I've been Lean-ifying a simpler (but non-trivial) algo. Pointing (current) AI at it only goes so far and in fact might go "too far" in certain cases, where a non-formalized argument would have sufficed. There's also "who watches the watcher" -- did it really prove what we're supposed to prove?

For something like these compression algos, though, I imagine it would be much easier since they already have actual proofs out there.

formal correctness proof is ridiculously hard, like, insanely hard, have you ever tried writing one for any real algorithm (not a platonic ideal quicksort)?