Showing math.HOShow all
3 papers · 1 filter
math.HO2026
Mathematicians in the age of AI
Jeremy Avigad
Recent developments show that AI can prove research-level theorems in mathematics, both formally and informally. This essay urges mathematicians to stay up-to-date with the technol…
math.HO2025
Is Mathematics Obsolete?
Jeremy Avigad
This is an essay about the value of mathematical and symbolic reasoning in the age of AI.
math.HO2024
Anatomy of a Formal Proof
Jeremy Avigad, Johan Commelin, Heather Macbeth +1
Interactive proof assistants make it possible for ordinary mathematicians to write definitions and theorems in a formal proof language, like a programming language, so that a compu…