Algorithm and Abstraction in Formal Mathematics - IPAM at UCLA

Explore the intriguing intersection of algorithms, abstraction, and formal mathematics in this 50-minute conference talk by Heather Macbeth from Fordham University at Lincoln Center. Delve into the paradoxical nature of formalized proofs, which often appear more abstract and computational than their paper counterparts. Discover a unique mathematical aesthetic for formalized mathematics, where algorithms and abstractions become acceptable due to instant cross-referencing of prerequisites. Examine how these elements, typically seen as "tonal shifts" in traditional mathematical discourse, find their place in formalization. Gain insights into attractive proofs that exemplify this aesthetic approach, presented by Macbeth at IPAM's Machine Assisted Proofs Workshop at UCLA.