Math 583E: Mathematics and AI

Fall quarter 2025

• Mon, Sept 29: Introduction and discussion, slides
  References:
  • Alan Turing, Computing Machinery and Intelligence, 1950
  • William Thurston, On proof and progress in mathematics, 1989
  • Akshay Venkatesh, Some thoughts on automation and mathematical research, 2024
  • Simon DeDeo, AlephZero and mathematical experience, 2024
  • Rodrigo Ochigame, Automated mathematics and the reconfiguration of proof and labor, 2024
  Discussion topics:
  • How would you design a modern version of Turing's 'imitation game'.
    • How do we measure intelligence?
    • Is imitation intellignece?
  • What will mathematical research look like in 15 years?
  • Is there an identity crisis in mathematics?
    • What does it mean to be a mathematician?
    • Who gets to call themselves a mathematician?
    • What value do we get from doing mathematics?
    • How should PhD students navigate emerging AI?
• Wed, Oct 1: Evolution of research math, teaching math, and AI, slides
  References:
  • Timothy Gowers, Rough structure and classification, 1999
  • Jarod Alper, Embracing AI and Formalization, pdf, 2025
  Books on existential risk:
  • Nick Bostrom, Superintellgience: Paths, Dangers, and Strategies, 2014
  • Max Tegmark, Life 3.0: Being human in the age of Artificial Intelligence, 2017
  • Toby Ord, The Precipice: Existential risk and the future and humanity, 2020

• Mon, Oct 6: Neural networks and backpropagation
  • Blackboard lecture on backpropagation
  • discussion of ideas for Project 1.
• Wed, Oct 8: Approximation theorems and discussion of AI
  • Blackboard lecture on approximation theorems in mathematics: universal approximation theorem for neural networks, Stone-Weierstrass theorems, Fourier approximation, Runge's Theorem, Mergeleyan's Theorem, ...
  • Brief remarks on sociology of mathematics, slides
  • Discussion topics:
  • What is mathematics good for? Does doing mathematics lose value when computers get better than us?
  • How might Tao’s pre-rigorous / rigorous / post-rigorous stages change with formalization?
  • Should we still teach long division? Should we teach integration rules? Is there an enfeeblement risk of incorporating AI in mathematics?

• Mon, Oct 13: Implementing ML pipelines in Python, slides
  • A curated list by Seewoo Lee on papers using ML for mathematical discovery.
  • Some of other MathAI graduate courses:
    • Berkeley Math 270: A Survey of Deep Learning for Mathematicians
    • Brown Math 1810C: Artificial Intelligence and Euclidean Geometry
    • UW CSE543: Deep Learning
    • UW CSE573: Introduction to AI
    • Harvard CS 2881: AI Safety
    • Stanford CS 336: Language Modeling from Scratch
    • Nebius Academy: AI in Mathematics
• Wed, Oct 15: Recurrent neural networks (RNNs) and transformers
  • Discussion of course projects
  • Blackboard lecture on recurrent neural networks and transformers with some use of these slides by Isabel Agostino and Bryan Pan
  • References for RNNs and LTSMs:
    • Chapter 10, Goodfellow, et al. Deep Learning
    • Chapter 6 of Tony Feng's lecture notes on recurrent neural networks.
    • Andrej Karpathy blog post: The Unreasonable Effectiveness of Recurrent Neural Networks
    • Original papers introducing encoder-decoder architecture:
      • Cho, et al: Learning Phrase Representations using RNN Encoder–Decoder for Statistical Machine Translation, 1995
      • Sutskever, et al: Sequence to Sequence Learning with Neural Networks, 1995
    • Colah: Understanding LSTM Networks
    • Andreas Madsen's Distill.pub post: Visualizing RNNs
    • Limitations of RNNs:
      • Bengio, Simard, and Frasconi, Learning Long-Term Dependencies with Gradient Descent is Difficult, 1994
      • Kaplan, et al., Scaling Laws for Neural Language Models , 2020
  • 3Blue1Brown Deep Learning Chapter 6, Attention in transformers, step-by-step

• Mon, Oct 20: Transformers
  • Blackboard lecture on transformers
  • References:
    • Karpathy's blog post The Unreasonable Effectiveness of Recurrent Neural Networks, 2015.
    • Vaswani, et al., Attention is All you Need, 2017.
    • Google Research’s blog post on attention, 2017
    • Chapter 7 of Tony Feng's lecture notes on transformers, 2025
    • Bahdanau, et al., Neural Machine Translation by Jointly Learning to Align and Translate, 2014
    • 3Blue1Brown Deep Learning Chapter 6, Attention in transformers, step-by-step, 2024.
• Wed, Oct 22: Large language models and reasoning models
  • Blackboard lecture on large language models and reasoning models
  • References:
    • Serrano, et al. Language Models: A Guide for the Perplexed, arXiv, 2023.
    • word2vec: Mikolv, et al, Efficient Estimation of Word Representations in Vector Space, arXiv, 2013.
    • Chapter 8 of Tony Feng's lecture notes on transformers, 2025
    • Chain of Thought: Wei, et al, Chain-of-Thought Prompting Elicits Reasoning in Large Language Models, arXiv, 2022.
    • Minverva: Google Research's blog post, 2022.
    • DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning, arXiv, 2023.

• Mon, Oct 27: Presentations of Project 1
• Wed, Oct 29: First glimpse at Lean
  • References:
    • Mathematics in Lean
    • Glimpse of Lean

• Mon, Nov 3: Logical foundations of Lean
  • Blackboard lectures on logical foundations of ZFC set theory, lambda-calculus, type theory, and finally the inductive calculus of constructions underlying Lean
• Wed, Nov 5: Discussion of group projects and a Lean tutorial

• Mon, Nov 10: Metaprogramming in Lean
  • Guest lecture by Dhruv Bhatia, github repo
• Wed, Nov 12:
  • Math AI News
    • Discussion of Erdös problems, Formal Conjectures Benchmark, Terence's Tao's comments on the power of today's LLMs for literature search, and the recent article Forbidden Sidon subsets of perfect difference sets, featuring a human-assisted proof by Alexeev and Mixon on the formalization in Lean of counterexamples of Erdös problem 707 including both a counterexample they discovered and a counterexample due to Marshall Hall, Jr from 1976 (even before Erdôs made the conjecture).
    • Discussion of AlphaEvolve (including original paper AlphaEvolve: A coding agent for scientific and algorithmic discovery and the more recent preprint Mathematical exploration and discovery at scale)
  • Group project work

• Mon, Nov 17: Defining structures and classes in Lean
  • Tutorial in Lean: nov17-structures.lean and nov17-classes.lean
• Wed, Nov 19: Group work in Lean

• Mon, Nov 24: Group work in Lean
• Wed, Nov 26: No class (Thanksgiving)

• Mon, Nov 24: Overview of autoformalization, automated theorem proving, and agentic formalization
  • Quotes from Dean and Naibo's paper Artificial intelligence and inherent mathematical difficulty
  • Daily news:
    • Recent progress on Erdös problems: Erdös problem 124, Tao's mathstodon post , and Lean zulip discussion.
    • Mathoverflow post on Examples for the use of AI and especially LLMs in notable mathematical developments.
    • Recent paper including mathematical results: Early experiments in accelerating science with GPT-5
    • Mochizuki's comments on Lean in Section 3.2 of his recent report
  • Mathlib: dependency graph and documentation overview
  • Tactic cheat sheets: Leanprover community and Buzzard's list
  • Blackboard lecture on autoformalization, automated theorem proving, and agentic formalization
  • Discussion of benchmarks for mathematical reasoning: MiniF2F, Humanity's Last Exam, HoList, MiniCTX, HoList, Herald, Lean-Workbook, Lisa, ProofNet, LeanDojo, CoqGym, VERINA, FrontierMath, FormalConjectures, IMProofBench, GaussMath, ...
  • Demonstration of Harmonic's Aristotle tool.
• Wed, Nov 26: From AlphaGo to AlphaProof
  • Daily news:
    • Math AI in the news: Logical Intellgience and Harmonic and Axiom
    • Aleph prover breakthrough?: Twitter post, github, news article, Zulip discussion
    • Erdös problem 481
  • Further demo of Harmonic's Aristotle
    • Calculus test: calculus-test.lean and Aristotle's output calculus-test_aristotle.lean
    • Attempt to prove that the fundamental group of S^1 is Z: prompt and Aristotle's partial proof
  • Blackboard lecture on reinforcement learning, Monte Carlo tree search, AlphaZero, and AlphaProof
  • References:
    • Atari games: Mnih, et al, Human-level control through deep reinforcement learning, 2015.
    • AlphaGo: Silver, et al, Mastering the game of Go with deep neural networks and tree search , 2016.
    • AlphaGo Zero: Silver, et al, Mastering the game of Go without human knowledge, 2017.
    • Alphazero: Silver, et al, A general reinforcement learning algorithm that masters chess, shogi, and Go through self-play, 2018.
    • AlphaProof: Hubert, et al, Olympiad-level formal mathematical reasoning with reinforcement learning, 2025.
  
  
  Expectations and grades: The evaluation metrics for this course will be based on class participation and project assignments. Successful class participation will earn a 3.0. To earn a 4.0, in addition to class participation, you must complete at least one of the two class projects successfully. Your project can be a collaborative group project.
  • Project 1: Machine learning (due Dec 5)
    • Design your own challenge to evaluate computer intelligence. It could be as simple as seeing if a computer could learn a certain mathematical function from data (e.g., number of primes less than a given integer). Another option is to copy typical tasks seen in machine learning courses, e.g., recognizing handwritten digits.
    • Using Python and the Numpy library, implement a simple neural network from scratch to solve your problem. Extra credit for implementing backpropagation.
    • Using Pytorch libraries, implement a more sophisticated neural network to solve your problem. Compare the results between your two implementations using a predesigned methodology.
  • Project 2: Formalization in Lean (due Dec 5)
    • Choose an accessible mathematical goal to formalize in Lean. There are many different types of options: a basic theorem in undergraduate mathematics, an IMO or Putnam problem, formalizing examples and counterexamples of a particular result, formalizing the definition of a sophisticated mathematical structure, or the metaprogramming of a simple tactic.
  
  
  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.
  Course policies

  • AI-based tools: In this course, students are permitted to use any AI tools. However, you must properly cite every AI tool used, you must explain how they were used, and you must specify which models were used. For instance, if you use github copilot while coding, indicate how you used it (e.g., tab code completion and using the chatbox to ask for documentation for Python commands) and which agent (e.g., Claude Sonnet 4), or if you used a prompt to generate template Python code for your project, write what prompt you used and which agent (e.g., Claude Sonnet 4).
    
    Use of AI in ways that are inconsistent with the parameters above will be considered academic misconduct and subject to investigation.
    
    Please note that AI results can be biased and inaccurate. It is your responsibility to ensure that the information you use from AI is accurate. Additionally, pay attention to the privacy of your data. Many AI tools will incorporate and use any content you share, so be careful not to unintentionally share copyrighted materials, original work, or personal information.
    
    Learning how to thoughtfully and strategically use AI-based tools may help you develop your skills, refine your work, and prepare you for your future career. If you have any questions about citation or about what constitutes academic integrity in this course or at the University of Washington, please feel free to contact me to discuss your concerns.
  
  
  • Religious accommodation: Washington state law requires that UW develop a policy for accommodation of student absences or significant hardship due to reasons of faith or conscience, or for organized religious activities. The UW’s Reglious Accommodation Policy, including more information about how to request an accommodation, is available here. Accommodations must be requested within the first two weeks of this course using the Religious Accommodations Request form.
  
  
  • Student disability resources: UW offers disability accommodations. If you have already established accommodations with Disability Resources for Students (DRS), please communicate your approved accommodations to me at your earliest convenience so we can discuss your needs in this course. If you have not yet established services through DRS, but have a temporary health condition or permanent disability that requires accommodations (conditions include but not limited to; mental health, attention-related, learning, vision, hearing, physical or health impacts), you are welcome to contact DRS at 206-543-8924 or uwdrs@uw.edu or disability.uw.edu. DRS offers resources and coordinates reasonable accommodations for students with disabilities and/or temporary health conditions.
  
  
  • Student conduct code: The University of Washington Student Conduct Code (WAC 478-121) defines prohibited academic and behavioral conduct and describes how the University holds students accountable as they pursue their academic goals. Allegations of misconduct by students may be referred to the appropriate campus office for investigation and resolution. More information can be found online here.