Georgia Institute of Technology College of Sciences

In recent years we have seen an explosion of interest in AI tools that excel at mathematical reasoning.  These tools, such as AlphaProof from Google DeepMind and Aristotle from Harmonic, combine tools and techniques from two core sub-fields of AI, namely, machine learning in the form of LLMs and symbolic reasoning in the form of theorem provers (e.g., Lean) and computer algebra systems (e.g., Maple). In response to these dramatic shifts in the capabilities of AI for math tools, peer universities are setting up AI for math centers. 

In this townhall, we will present a vision of a similar AI for math center at Georgia Tech, under the auspices of the Institute for Data Engineering and Science (IDEaS). The goals include enabling GT and GTRI research groups focused on AI4Math by bringing in funding , conducting seminars/workshops on AI4Math topics, and setting up tutorials such as Introduction to Lean and AI4Math Tools.