Alumni Club Study Group: Formalising Math with Lean
Summer 2026
May 18, 2026
-
Jul 17, 2026
Tu 11:00am - 12:00pm ET
I'm a paragraph. Click here to add your own text and edit me. It's easy.
Checking your registration status...
To access the program content, you must first create an account and member profile and be logged in.
You are registered for this program.
Computer setup
Next Event
NEXT EVENT
Registration Deadlines
May 19, 2026
-
Erdős Institute Alumni Club Members with a strong background in graduate level mathematics
-
-
Category
Advance, Alumni Club Study Group
Overview
This study group introduces participants to formalizing mathematics in Lean 4, an interactive theorem prover. Over our time together, we will work through the fundamentals of Lean's type-theoretic foundations, learn to navigate Mathlib (Lean's enormous mathematics library!) and gain hands-on experience translating familiar mathematical arguments into machine-checkable proofs.
Topics will range from basic tactic-mode proving through structuring larger formalization projects. No prior experience with proof assistants is required, but participants should be comfortable writing proofs for humans. By the end of the study group, participants will be equipped to formalize results in their own area of expertise.
Click here to be invited to the slack organization: The Erdős Institute
Click here to access the slack cohort channel: #slack-cohort-channel
Click here to access the slack program channel: #slack-program-channel
Click here to download the Events & Deadlines .ics calendar file
Organizers, Instructors, and Advisors
Jim Fowler
Associate Professor of Mathematics, Ohio State
Office Hours:
by appointment
Email:
Preferred Contact:
Objectives
1. Learn the basics of Lean 4 syntax, its type system, and tactic-based programming
2. Gain fluency with core Lean tactics (intro, apply, exact, rw, simp, ring, linarith, etc.)
3. Understand how Mathlib is organized and how to search for and use existing library results
4. Formalize nontrivial mathematical proofs using Mathlib.
The overall goal is to prepare Erdős alumni to formalize results drawn from their own interest or even to contribute to Mathlib itself.
First Steps/Prerequisites
I'm a paragraph. Click here to add your own text and edit me. It's easy.
Program Content
I'm a paragraph. Click here to add your own text and edit me. It's easy.
Textbook/Notes
Note: our video player does not support playback speed options. You can find a third party browser extension which will allow you to modify video playback speed. For example, this one works for Chrome: video-speed-controller. If you would prefer to avoid a browser extension you can manually modify the playback speed in the javascript console as well: Speed up any HTML5 video player!
Project/Homework Instructions
I'm a paragraph. Click here to add your own text and edit me. It's easy.
Schedule
Click on any date for more details
Orientation & Setup
Phase 1: Instruction and Project Completion
Project Review & Judging
Phase 2: Intense Interview Prep & Career Connections
Computer setup
May 21, 2026 at 03:00 PM UTC
EVENT
Sets, Functions, and Structures
Jun 9, 2026 at 03:00 PM UTC
EVENT
Analysis in Lean
Jun 30, 2026 at 03:00 PM UTC
EVENT
Meeting #1
May 26, 2026 at 03:00 PM UTC
EVENT
Navigating Mathlib
Jun 16, 2026 at 03:00 PM UTC
EVENT
Formalization Projects #1
Jul 7, 2026 at 03:00 PM UTC
EVENT
Tactics and Logic
Jun 2, 2026 at 03:00 PM UTC
EVENT
Abstract algebra in Lean
Jun 23, 2026 at 03:00 PM UTC
EVENT
Formalization Projects #2
Jul 14, 2026 at 03:00 PM UTC
EVENT
Project/Homework Deadlines