DeDeo, S. (2024). AlephZero and Mathematical Experience. Bulletin of the American Mathematical Society, 61(3), 375–386. https://doi.org/10.1090/bull/1824
Summary
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.
Atomic notes
- The value of a mathematical claim is guided by experiences of impasse and resolution, after DeDeo
- Glitches are uncanny experiences of what ought not to be, after DeDeo
- Mathematical glitches
Selected concepts and passages
- Aboutness and intentionality: “[In a philosophical sense, aboutness is] he way in which one thing (e.g., a logical formula) can be represent, be about, another (e.g., a shared idea, a personal intuition, or a mental model of a mathematical object)” (375).
- Proxies for judgement lead to a zombie mathematics: “Deployed widely enough, the reliance on such proxies—even if they correlated perfectly with ideal judgement—would lead to a strange scenario: a kind of zombie mathematics, where mathematicians celebrate a theorem not for how it untangles and reorders their reasoning, or the reasoning of their colleagues, but because it has a high [structural] centrality score” (378).
- Mathematicians identify error by a principle of explosion: “One sign of an error, as I learned during the 2022 Symposium, is that subsequent results become “too easy” to obtain, in a kind of limited principle of explosion that temporarily levels the hierarchy of value” (379).
- Mental models are refined by error: “Without the possibility of being wrong, the mental model cannot change and the process of attention is diffused. This leads to a second dystopian fantasy, one where automated methods lead to a world in which our mental models become increasingly vague and low-resolution” (380-381).
- An analogy between proof assistants and video games: “Proof assistants and video games are just ordinary computer programs, a complex system of inter-related states and state-to-state transition rules” (383).