what? how does that work?

You give it a few hundred problem classes, and constraints for possible answers, and it will randomize the class of problems and generate a unique problem as well as calculate the answer. Then you submit the answer as well as your work and it gets corrected.

For things such as proofs, it might give you a problem for which the theorem is needed, then ask you to solve the problem, indicate which theorem you used, and then prove the theorem.

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.

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.