Watch a 53-minute Harvard CMSA seminar presentation where DeepSeek researcher Huajian Xin explores the intersection of large language models and formal theorem proving. Discover how recent AI advancements have impacted mathematical reasoning and automated theorem proving, particularly focusing on the challenges these models face when working with formal proof assistants like Lean and Isabelle. Learn about the innovative approaches developed in the DeepSeek-Prover series, including autoformalization for training data generation, reinforcement learning with proof assistant feedback, and Monte Carlo tree search for test-time optimization. Gain valuable insights into current model capabilities, ongoing challenges, and future prospects for large language models in automated theorem proving.