I'd agree with your dislike of ugly solutions. I guess the benefit of this being accepted as a proof is that all the conjectures that begin 'Assuming that x is

I'd agree with your dislike of ugly solutions. I guess the benefit of this being accepted as a proof is that all the conjectures that begin 'Assuming that x is true...' can now be converted to theorems saying 'x is true, therefore...', which might tidy up a lot of loose ends.