I would guess that minimum length proofs will end up like code golfing and demoscene hacks, where part of the code is also used as texture somewhere, etc. So many overlapping uses that don't make much sense but by happenstance allow making the proof shorter but less clear. The shortest proof is certainly not the most elegant. The shortest proof is also impossible to find in general due to halting problem etc. The AI isn't finding shortest proofs, and better AI will be better at finding clear and elegant proofs.

And I think many more are just spaghetti code proofs that would benefit from abstraction and cleanup, but no one has had the time to do that.