Formal Reasoning Meets LLMs: Toward AI for Mathematics and Verification

AI for mathematics (AI4Math) is intellectually intriguing and crucial for AI-driven system design and verification. Much of the recent progress in this field has paralleled advances in natural language processing, especially by training large language models on curated mathematical text datasets. As a complementary yet less explored avenue, formal mathematical reasoning is grounded in formal systems such as Lean, which can verify the correctness of reasoning and provide automatic feedback. This talk by Kaiyu Yang (Meta) from the Simons Institute and SLMath joint workshop on AI for Mathematics and Theoretical Computer Science introduces the basics of formal mathematical reasoning, focusing on two central tasks: theorem proving (generating formal proofs given theorem statements) and autoformalization (translating from informal to formal). Yang highlights the unique challenges of these tasks through two recent projects: one on proving inequality problems from mathematics olympiads, and another on autoformalizing Euclidean geometry problems.