[Tainnor]

Do you have any example of any software that can generate problems for actual proof-based courses (e.g. abstract algebra)? I'm having a really hard time imagining this, we can't even fully automate theorem proving - how are we supposed to automate theorem generation? And this ignores the fact that you also need to make sure that all the proofs are "of the same difficulty" in terms of fairness.

[sudosysgen]

Ah, no, the theorems would have to be manually selected. But given a high enough number and an automatically generated context it makes cheating much harder.