Natarajan Shankar: Beautiful Formalizations and Proofs

Beauty in mathematics may or may not be a concept that is formalizable, but beauty is clearly critical for effective formalization. In the context of mechanization of mathematics that has been ongoing over the last four decades, the criterion for beauty needs to be adapted from that of informal mathematics. Beautiful informal arguments might turn out to be less than elegant when formalized, and conversely, the austere beauty of mechanized mathematics might defy conventional standards. In the context of mechanization, particularly the use of decision procedures, a beautiful formalization is one that elegantly leverages the power of formal language and automation to deliver clear, concise, and general definitions and proofs. We illustrate our approach to the aesthetics of formalization with examples.