With the ever-widening use of software in safety-critical applications such as autonomous vehicles, design defects are becoming increasingly catastrophic in their consequences. Formal, mathematical techniques to prove the correctness of software provide a promising approach to ensure the safety of such systems. However, formal verification of complex systems often requires an impractical level of human effort: automated theorem provers (ATPs) typically do not scale to real-world applications, forcing correctness proofs to be written largely by hand in interactive theorem provers (ITPs). A similar challenge has arisen in mathematics, where there is growing use of ITPs to formalize (and sometimes find mistakes in) proofs: the lack of scalable automation puts formalization beyond the reach of most working mathematicians. This project aims to address these challenges by developing new techniques allowing ATPs to scale to complex theorems, as well as tools usable by mathematicians for proof formalization. Enhancing the scalability and usability of ATPs will reduce the barrier to entry for safety-critical system designers and mathematicians to verify their systems and proofs, helping to make these safer and more trustworthy. The project has three primary research thrusts. The first two thrusts tackle several obstacles to using Large Language Models (LLMs) to automate proof construction, turning an ITP into an ATP: data scarcity, sparse rewards, and lack of self-play. Thrust 1 wi