41 citations · 54 across the 13 of their papers we have counts for
4 papers · 1 filter
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…
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…
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…
Abstraction boundaries and spec driven development in pure mathematics
Johan Commelin, Adam Topaz
In this article we discuss how abstraction boundaries can help tame complexity in mathematical research, with the help of an interactive theorem prover. While many of the ideas we…