AlephZero and Mathematical Experience
Simon DeDeo

TL;DR
This paper discusses how automated proof construction influences mathematical cognition, affecting our understanding, reasoning, and perception of mathematical theorems, and introduces the concept of 'glitching' as a new mathematical experience.
Contribution
It offers a philosophical analysis of automated proof methods' impact on mathematical thinking and proposes 'glitching' as a novel, game-like exploration of mathematical definitions.
Findings
Automated proofs alter how we perceive the role of mathematical components.
They influence our reasoning errors about mathematical objects.
They enable a new 'glitching' experience for exploring mathematical consequences.
Abstract
This essay explores the impact of automated proof construction on three key areas of mathematical cognition: on how we judge the role one piece of mathematics plays in another, on how we make mistakes in reasoning about mathematical objects, and on how we understand what our theorems are truly about. It concludes by speculating on a new form of mathematical experience that these methods could make possible: ``glitching'', a game-like search for uncanny consequences of our definitions.
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
TopicsLogic, Reasoning, and Knowledge · Computability, Logic, AI Algorithms · Logic, programming, and type systems
