The ACL2 theorem prover finds proofs in the ACL2 logic. It can be automatic. But most often the user must help it.
The user usually guides ACL2 by suggesting that it first prove key lemmas. Lemmas are just theorems used in the proofs of other theorems.
