Math AI Resources

Investing in applied machine learning without understanding the mathematical foundations is like investing in health care without understanding biology. —Rebecca Willett (2023)

What is Math AI? At the intersection of mathematics and AI is a broad, rapidly-developing subject. It is truly interdisciplinary subject connected to mathematics, applied mathematics, statistics, computer science, philosophy, and engineering. It can be roughly categorized into the fiber interrelated areas:

the mathematics behind AI
mathematical formalization
autoformalization: using machine learning to automate formalization
machine learning to assist mathematical research, and
the meaning of mathematics in the age of AI.

Math AI resources

Embracing AI and Formalization: Experimenting with Tomorrow's Mathematical Tools by Jarod Alper
All the articles from the April 2024 and July 2024 issues of the Bulletin of the AMS
AI for Math Resources created following the National Academies of Sciences meeting: AI to Assist Mathematical Reasoning

Lean resources

Playing around

Play the Natural Number Game (by Kevin Buzzard and Mohammad Pedramfar).
Additional Lean games
A Glimpse of Lean by Pattrick Massot
Online version of Lean (no installation)

Getting serious

Install a Lean 4 environment on your computer with VS Code: follow the directions here.
Mathematics in Lean, introductory book by Jeremy Avigad and Patrick Massot
- Follow the instructions in Section 1.1 "Getting Started" in to download the "mathematics_in_lean" repository which you should be able to view in VS Code.
Kevin Buzzard's course Formalising Mathematics 2024
Theorem Proving in Lean 4 by Jeremy Avigad, Leonardo de Moura, and Soonho Kong
Mathlib4 documentation.
Lean community resources including math courses using Lean
Search tools for Lean: Loogle, Moogle, and LeanSearch. They can be used within a VS code.
Lean tactic cheatsheets: Lean community, Buzzard
Mathlib naming conventions
Join the Lean community Zulip.