Comment by wiz21c

the good news I guess are

1/ lean-zip is open source so it's much easier to have more Claude's eyes looking at it

2/ I don't think Claude could prove anything substantial about the zip algorithm. That's what lean is for. On the other side, lean could not prove much about what's around the zip algorithm but Claude can be useful there.

So in the end lean-zip is now stronger!