This note briefly reports on a set of practical tools that are part of a larger system, the full description of which will be presented elsewhere. These tools are designed to assist mathematicians working with theorem provers like Prover9 on open problems. While Prover9 is appreciated for its intuitive syntax, many other widely-used provers utilize TPTP or Waldmeister syntax. This divergence poses challenges for the working mathematicians who wish to take advantage of the fact that some provers excel in certain types of problems while others are better suited for different kinds. Additionally, some of these provers struggle with handling theories containing multiple goals, a common scenario when mathematicians are exploring meaningful conjectures. To address these issues, we have developed a translator to facilitate the creation of a prover portfolio in the user's preferred language, as well as a dedicated algorithm for processing multiple goals. This tool enables the use of various provers without the need to rewrite theories, and proves conjectures sequentially, each proven conjecture serving as a new axiom for subsequent ones.