Registration Deadline: September 20, 2026

Instructors: Professor Arul Shankar, University of Toronto & Dr. Kevin Wilson, Borealis AI

Course Dates: TBA
Mid-Semester Break: TBA
Lecture Times: TBA
Office Hours: TBA

Registration Fee:

• Students from our Principal Sponsoring & Affiliate Universities: Free
• Other Students: CAD$500

Capacity Limit: TBA

Format:

• In-Person: Room 210, Fields Institute
• Online: via Zoom

Course Description

Since computers have been available, mathematicians have used them both to develop complex conjectures such as Birch and Swinnerton-Dyer and to prove mathematical statements such as the Four Colour Theorem. Recently, advances in artificial intelligence have pushed computers' capabilities to new heights, with several groups announcing achievements such as automatically providing answers to IMO problems, formalizing deep theorems like the Strong Prime Number Theorem, and making substantial progress on heretofore unproved lemmas in research mathematics.

In this course, we'll cover some of the key components that have pushed this revolution forward. The course is divided into two parts. First, we will cover "formalization": how mathematicians use the Lean interactive theorem prover to check that a proof is correct. Second, we'll explore how modern AI tools are being used to "automate" parts of the workflow of mathematics, with a focus on using agentic workflows to formalize mathematics.

Each meeting of this course will consist of two components: a lecture and demonstration component & a lab component where students will get a chance to implement the topics discussed in the first part of the meeting.

Course Goals

Students who take this course should come away with:

• A familiarity with the theoretical underpinnings of the Lean programming language, namely Dependent Type Theory
• Comfort in proving basic mathematical statements in Lean
• An introduction to Mathlib, Lean’s core mathematical library
• An understanding of how recent advances in artificial intelligence (e.g., LLMs, agentic workflows) are being used to automatically formalize known mathematics and find proofs of novel statements
• An understanding of the key components used to build agentic workflows in mathematics and other domains
• Experience using agentic workflows in formalizing mathematics

Week-by-Week Topics (the exact contents may change as the field is rapidly developing)

Module 1: Formal Methods and the Lean Theorem Prover

• Week 1: Motivation and Lean Introduction
• Topics: What is a proof?, computer-assisted mathematics, milestones in formalization, introduction to Lean.
• Week 2: Type Theory
• Topics: Basic types in Lean, the Curry–Howard correspondence, propositions as types, the type hierarchy.
• Week 3: Dependent Type Theory
• Topics: What makes a type dependent?, predicates vs. propositions, universal quantifiers as dependent arrows, the axiom of choice.
• Week 4: Inductive Types
• Topics: Constructors and elimination rules, enumerations, structures and logical operators, defining the natural numbers, induction.
• Week 5: Type Classes
• Topics: Overloading and type classes, algebraic structures in Lean, adding properties, the $p$-adic norms on $\Q$, navigating Mathlib.
• Week 6: What is Equality?
• Topics: Definitional vs. propositional equality, quotients and Lean’s remaining axioms, extensionality, filters and eventual equality.
• Week 7: Frontier of Lean Formalization Efforts

Module 2: AI and Automated Theorem Proving

• Week 8: "AI" as Smart Search
• Topics: Monte Carlo tree search, self-play and AlphaGo, LLMs as guessers, agentic frameworks for mathematics.
• Week 9: Building a Better Guesser
• Topics: Benchmarks, constrained generation and chain-of-thought prompting, providing context via tools, evaluating agentic workflows.
• Week 10: Autoformalization
• Week 11: Automated Theorem Proving
• Topics: Informal mathematical approaches, formal mathematical approaches, hybrid approaches, fine-tuning models for theorem proving.
• Week 12: Automated Theorem Proving

Suggested Readings and Practicums

Much of the following will be walked through in class, but may be useful to explore ahead of time.

• Kevin Buzzard’s Natural Numbers Game: A Lean "game" focused on how Lean builds up the natural numbers and how proofs are written in Lean. This is a good first introduction to Lean for mathematicians.
• Emily Riehl’s Reintroduction to Proofs: Another Lean game, focused on how Lean "thinks" about mathematics — in particular, how dependent type theory treats propositions and how constructive mathematics differs from classical mathematics. We will walk through several aspects of this in the first several labs of class, so this is an optional but useful way to get acquainted with how Lean works.
• Installing Lean: The official documentation for installing Lean locally. The above two games are hosted on a server by Heinrich Heine University Düsseldorf. Throughout this class, we will be working with local installations of Lean. This guide will help you get your local installation set up.