Paradoxically, the formalized version of a proof is often both more abstract and more computational than the paper version. I will argue that this is part of a different mathematical aesthetic for formalized mathematics: algorithms and abstractions, which read as “tonal shifts” in the context of ordinary mathematical discourse, become acceptable in formalization, which features pervasive and instant cross-referencing to prerequisites. Finally, I will sketch some proofs which I find attractive according to this aesthetic.
Copyright. All Rights Reserved.