Our experience with the current prover interface is very new and as such we are still very much experimenting with it and don't expect it to be perfect at this point in time. Many simple theorems will be provable. Some that the user thinks should be might not, and the user will be required to add further hypothesis and lemmas that may seem unnecessary. We are currently working on making this interface as robust and predictable as possible, and welcome any feedback the user can offer.
One area where the user can directly experiment is with the axioms that make up the ProverBase. The axioms that make up an effective prover library are best determined by an experimental evolutionary process. The user is welcome to play with the axioms in the ProverBase, by adding new ones or changing or deleting old ones. Keep in mind the goal is to have a single library that is useful for a wide range of proofs. Axioms that are specific to different proofs should be created in separate specs and imported where needed.