Showing math.HOShow all
2 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.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…