Algorithm and abstraction in formal mathematics
Heather Macbeth
TL;DR
This paper compares traditional and formalised mathematical writing, highlighting differences in style related to computation and abstraction, and discusses how these differences reflect distinct mathematical aesthetics.
Contribution
It provides a detailed analysis of stylistic differences in mathematical writing, emphasizing the impact of formalisation on mathematical aesthetics.
Findings
Formalised mathematics incorporates computation more explicitly.
Differences in abstraction levels influence mathematical presentation.
Formal style reflects a distinct mathematical aesthetic.
Abstract
I analyse differences in style between traditional prose mathematics writing and computer-formalised mathematics writing, presenting five case studies. I note two aspects where good style seems to differ between the two: in their incorporation of computation and of abstraction. I argue that this reflects a different mathematical aesthetic for formalised mathematics.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsComputability, Logic, AI Algorithms