Now that you have seen the theorem prover in action you might be curious as to how you guide it.
The idea is that the user submits conjectures and advice and reads the proof attempts as they are produced.
Most of the time, the conjectures submitted are lemmas to be used in the proofs of other theorems.
