Showing math.HOShow all
3 papers · 1 filter
math.HO2026
The Educational Proof Assistant Waterproof in an Introductory Proof Course: Proof Construction and Learning Processes
Pim Otte, Rogier Bos, Johan Commelin +1
We study the use of an educational proof assistant in an introductory proof course through a quasi-experiment in a varied setting: multiple teachers, students with different study…
math.HO2026
Shaping the Future of Mathematics in the Age of AI
Johan Commelin, Mateja Jamnik, Rodrigo Ochigame +2
Artificial intelligence is transforming mathematics at a speed and scale that demand active engagement from the mathematical community. We examine five areas where this transformat…
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…