[bocklund]

One of the keys to learning is making students engage in the material and to fix their mistakes. Computers are uniquely able to give individual, rapid feedback.

Even at the advanced level it would be really cool for students to have access to and use proof software. I wish I could have had the opportunity to work out proofs for myself, guided by software, instead of just being given them.

[nmca]

Interactive theorem proving is an active area of research, but it's quite hard to do well, and the main area of focus is on theory atm, as opposed to UX