We have seen this before even with human-generated proofs. Inelegant 100+ page proofs of the global stability of Minkowski space-time or the four colour problem leave humans reeling. Is it worth-while learning? Any lessons to generalise? If not it is just a mechanical exercise (like coding).