Recorded 17 February 2023. Heather Macbeth of Fordham University at Lincoln Center presents "Algorithm and abstraction in formal mathematics" at IPAM's Machine Assisted Proofs Workshop. Abstract: 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. Learn more online at: http://www.ipam.ucla.edu/programs/workshops/machine-assisted-proofs/