I've yet to see AI be good at extracting good abstractions. More often than not it jumps to creating a battery of special case checks.

No. AI sucks at formal languages and implications.

Lossy decompression probably won’t ever be really good at this. If it’s missing from the data, then it won’t be there.

The AI math proofs were probably already out there in tiny pieces and nobody got all of the pieces together. That is valuable. It’s different from making a piece that is missing. And the AI will just hallucinate.

May work for simple cases, but how would you come up with something like typst, or thunderbird?