Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Explore how artificial intelligence can revolutionize mathematical discovery through a comprehensive examination of symbolic, neural, and neuro-symbolic approaches in this 53-minute keynote presentation from Lambda Days 2025. Delve into the cutting-edge field of AI-assisted lemma construction for mathematical reasoning and computer program verification within proof assistant systems like Lean, Isabelle, and Coq. Discover how these tools are increasingly adopted by research mathematicians for large-scale collaborations and complex proof verification, with insights into Terrence Tao's prediction that AI-enabled proof assistants will become trustworthy mathematical co-authors by 2026. Learn about the challenges of mathematical formalization and examine innovative approaches to autoformalisation that translate English-expressed mathematics into proof assistant languages. Understand the specific focus on conjecturing lemmas designed to assist human users in mathematical formalization while strengthening automated theorem provers. Investigate how Large Language Models can be effectively utilized for lemma generation and discover optimal strategies for combining them with symbolic tools. Gain insights into developing practical, generic conjecturing tools that span broad mathematical theories and provide real utility for proof assistant users, representing a significant step forward in AI-assisted mathematical research and formal verification.
