Algorithm and abstraction in formal mathematics
History and Overview
2024-05-09 v1
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.
Keywords
Cite
@article{arxiv.2405.04699,
title = {Algorithm and abstraction in formal mathematics},
author = {Heather Macbeth},
journal= {arXiv preprint arXiv:2405.04699},
year = {2024}
}
Comments
14 pages, 2 figures; extended abstract for an invited lecture at the 2024 International Congress on Mathematical Software