[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.