Title: Beautiful Formalizations and Proofs
Speaker: Natarajan Shankar, SRI Computer Science Laboratory

Abstract: 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 actively pursued 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 the aesthetics of formalization with
examples.

Bio: Dr. Natarajan Shankar is a Distinguished Senior Scientist and SRI Fellow at
the SRI Computer Science Laboratory.  He received a B.Tech. degree in Electrical
Engineering from the Indian Institute of Technology, Madras, and Ph.D. in
Computer Science from the University of Texas at Austin.  He is the author of
the book, "Metamathematics, Machines, and Godel's Proof" (Cambridge
University Press) and the co-developer of a number of technologies
including the PVS interactive proof assistant, the SAL model checker, and the
Yices SMT solver.  He is a co-recipient of the 2012 CAV Award and the recipient
of the 2022 Herbrand Award.