The Growing Map of Open Problems(opens in new tab)
A temporal map of 15,458 open, partially solved, and solved mathematics problems. A problem with a gold border has been stated in Lean. Click any problem for its statement.
Resources
Associated UW courses and seminars, and curated articles about AI for math and Lean.
Tools
TheoremSearch(opens in new tab)
A semantic search engine for mathematical results. Describe a result in natural language, and TheoremSearch finds it across arXiv, the Stacks Project, and more.
Seminars
We often hear that mathematics consists mainly of proving theorems. Is a writer's job mainly that of writing sentences?
-- Gian-Carlo Rota (1980)
- Math: Math AI Seminar
- Math: Distinguished Seminar in Optimization & Data
- CSE: Colloquium of PLSE (Programming Languages and Software Engineering)
Courses
Rigor has ceased to be thought of as a cumbersome style of formal dress that one has to wear on state occasions and discards with a sigh of relief as soon as one comes home. We do not ask any more whether a theorem has been rigorously proved but whether it has been proved.
-- André Weil (1956)
- EE 598: Automated Mathematics, Winter 2026, Eric Klavins.
- Math 480: Introduction to Mathematical Formalization, Spring 2025, Jarod Alper
- CSE 505: Programming Languages, Spring 2025, Zachary Tatlock and James Wilcox.
- EE 546: Knowledge Representation and Reasoning, Winter 2025, Eric Klavins.
- Math 480: Introduction to Mathematical Formalization, Spring 2024, Vasily Ilin.
Reading
"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 five interrelated areas:
- The mathematics behind AI
- Mathematical formalization
- Autoformalization: ML to automate formalization
- Machine learning to assist mathematical research
- The meaning of mathematics in the age of AI
Articles and guides
- Embracing AI and Formalization: Experimenting with Tomorrow's Mathematical Tools by Jarod Alper
in Bulletin Of The American Mathematical Society. - 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
Learning Lean
- 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.