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 cou

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.