Neural language models have opened a fascinating, flexible platform for reasoning in mathematics, programming, and beyond. This talk will explore the intersection of these models and the rigor of formal reasoning. First, I discuss my work on building foundation models for mathematics and using language to guide the search for formally verified proofs. Then, I present our research on inference-time reasoning, which uncovers new scaling laws for reasoning based on optimally combining generators and verifiers. Finally, I discuss the challenge of building AI systems that improve their reasoning capabilities over time by learning from both formal and informal feedback. I close by discussing opportunities and future directions in mathematics, programming, agents, and beyond.