Abstract:
The field of AI for Mathematics has moved its focus from solving benchmark problems with numerical solutions to generating formal proofs to research-level mathematical questions. In this survey talk we will cover recent developments and future directions in AI4Math, including the following three topics:
-
Formalization and auto-formalization, where natural language math contents (with LaTeX formulas) is converted into Lean, Isabelle, and Coq programs.
-
Automated theorem proving using LLMs, where transformer‑based models now guide symbolic search of formal proofs and achieve competitive performances on benchmarks such as Mini-F2F and PutnamBench.
-
Conjecturing, where programming language helps with new knowledge generation in Euclidean Geometry and pairing conjecturer and prover gives advances in performance.