Algorithm and abstraction in formal mathematics

Heather Macbeth
Fordham University at Lincoln Center

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.

Presentation (PDF File)

Back to Machine Assisted Proofs