Syllabus: Mathematics and AI is a new course that explores the intersection of mathematical research and artificial intelligence. It is a rapidly evolving interdisciplinary area covering a broad range of themes:
- Mathematics of AI:
- Mathematical foundations of machine learning using probability theory, optimization, statistics, and data science.
- What are neural networks, transformers, (large) language models, and reasoning models?
- What limitations if any do neural networks or transformers have?
- Trillion dollar question: Why are modern machine learning algorithms as effective as they are?
- AI for Mathematics:
- Formalization: process of writing a mathematical proof into a formal language that can be checked by a computer.
- Autoformalization: formalization of natural language mathematics with minimal human input.
- Machine learning to assist mathematical research: using modern machine learning algorithms together with extremely large data sets and computational power to uncover new insights.
- History/philosophy/anthropology of mathematics: What is the meaning of mathematics in the age of AI?
- Teaching and AI: How will AI change the way we teach and learn mathematics?
While this course is meant to be a broad survey of the above themes, we will not have time to dive into every topic above in detail. This course will focus much more on the AI for Math angle than Math of AI.
The first and last lecture will be devoted to group discussions on the meaning of mathematics in the shifting landscape of AI.
The first component of the course will cover the fundamentals of neural networks, transformers, (large) language models, and reasoning models. We will also discuss approximation theorems, e.g., the universal approximation theorem for neural networks. We will also experiment with programming our own machine learning models using Python (first by building simple neural networks from essentially scratch) and then using PyTorch (utilizing their sophisticated libraries for ML algorithms).
The second part of the course will cover formalization in the Lean Theorem Prover. We will introduce Lean as a functional programming language, discuss dependent type theory (as opposed to ZFC), and then learn how to formalize our own mathematics in Lean using both tactics and Lean's mathematical library mathlib.
The third component of the course in on autoformalization. We will give background on classical reinforcement learning algorithms and discuss AlphaZero's success on mastering board games such as Chess and Go. We will overview the algorithms underlying the powerful tactics such as exact?, simp, linarith, ring, canonical, grind, etc. We will also
cover the approaches of recent autoformalization successes such as AlphaProof, GoedelProver, SeedProver, Gauss/Mathinc, etc.
Depending on time, the final component is on how machine learning can assist mathematicians in research. We will discuss to what extent frontier models can behave as copilots for mathematicians providing useful references and insights to guide discovery. We will also discuss recent successes on (a) using large data sets to discover new relationships, e.g., elliptic curve murmurations, (b) generating counterexamples, e.g., in graph theory, and (c) producing efficient formulas, e.g., efficient tensor decompositions.