## Guiding the ACL2 Theorem Prover

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.