I don't see how they have any incentive to do so.

I communicated loosely; I meant AI users in general, not OpenAI specifically.

My hunch is that improving those proofs specifically might be a similar endeavour as improving a large vibe coded app.

It's a search problem; finding the shortest and most elegant path through the space of arguments.