Formal Mathematical Reasoning: A New Frontier in AI

Stream: Machine Learning for Theorem Proving

[Kaiyu Yang]

Excited to share our position paper: "Formal Mathematical Reasoning: A New Frontier in AI"! https://arxiv.org/abs/2412.16075

This paper advocates for formal mathematical reasoning grounded in formal systems such as Lean. We believe combining formal and informal approaches will play an important role in future AI for not only math but also verifiable code generation and beyond.

This is a team effort with Gabriel Poesia, @Jingxuan He, @Wenda Li, Kristin Lauter, Swarat Chaudhuri, and Dawn Song.
Special thanks to @Jeremy Avigad, @Albert Jiang, @Zhaoyu Li, Peter O'Hearn, @Daniel Selsam, Armando Solar-Lezama, and @Terence Tao, who have provided valuable feedback. We also welcome additional feedback that can potentially go to the next revision!