[pfdietz]

Perhaps in the future we'll see golfing of formalized proofs as a valid and valuable form of mathematics, not just proving a theorem for the first time.

Of course there's no reason AI couldn't do that too.