[mseri]

Jim Portegies (TU/e, Netherlands) and Jelle Wemmenhobe have done a lot of research on this, using their “waterproof” (controlled natural language compiled to coa) to test this directly in class. The results are very interesting, and indeed actively messing around is still a very important part of the learning experience, but you can see at least some benefits in also having a theorem prover to check if your proofs are correct.

What I was surprised is that the students learn some patterns of proof properly, but only if you make sure that they are explicitly exposed by the proof assistant (so the more automation the less learning also in this case).

You can find a lot of the work summarized in Jelle’s PhD thesis at https://research.tue.nl/nl/publications/waterproof-transform...