Algorithm and abstraction in formal mathematics

2024/05/07 by Heather Macbeth, Macbeth, Heather · 1 voice · 1 citation
Computer Science · Mathematics · #03B35 #68-02 #68V15 (Secondary) #68V20 (Primary) 00A30 #Computability, Logic, AI Algorithms #F.4.1 #FOS: Mathematics #History and Overview (math.HO) #math.HO

paper · pdf · doi:10.48550/arxiv.2405.04699

openalex publication_date 2024/05/07 · arxiv published 2024/05/07 · arxiv updated 2024/05/07 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Cited by

• Thinking Machines: Mathematical Reasoning in the Age of LLMs

Discussions

• Algorithm and Abstraction in Formal Mathematics [hn, 3 points, 0 comments]

Related

• Mathematics and the formal turn
• Mathematics: abstraction and reality. A sketch toward deeper analysis
• Abstraction boundaries and spec driven development in pure mathematics
• Mathematics in the Age of the Turing Machine
• Mathematics ... Applications