Proof assistants provide a framework for the modelling and verification of theories, as well as trustworthy software. However, such power is usually only available to experts. We propose a new approach, based on algebraic effects and handlers, to integrate different automated proof strategies that enable newcomers to take advantage of proof assistants without an in-depth understanding of underlying theory. Our approach gives newcomers an effect system, a handful of effectful strategies (tactics, proof search, and SMT solvers) and their handlers under a shared interface, while advanced users can extend our system with new effects and new handlers. Lastly, we prototype the system as a library in Agda. While our prototype is minimal, it shows how easily proofs can be carried out so long as the user has the correct intuition. We believe our system empowers non-experts and has the potential to bring verified software to relevant industries, such as finance.