Formal Reasoning Meets LLMs: Toward AI for Mathematics and Verification

This talk by Kaiyu Yang from Meta explores the intersection of formal reasoning and large language models in the field of AI for Mathematics (AI4Math). Discover how AI4Math is not only intellectually fascinating but essential for AI-driven system design and verification. Learn about recent progress in this field that has developed alongside advances in natural language processing, particularly through training large language models on curated mathematical text datasets. Explore formal mathematical reasoning grounded in systems like Lean that can verify reasoning correctness and provide automatic feedback. The presentation covers the fundamentals of AI for formal mathematical reasoning, with emphasis on two key tasks: theorem proving (generating formal proofs from theorem statements) and autoformalization (converting informal mathematics to formal representations). Examine the unique challenges in these areas through two recent projects: one focused on proving inequality problems from mathematics olympiads and another on autoformalizing Euclidean geometry problems.