Lean Seminar — Fall 2026 | University of Utah Mathematics

About the seminar

Learning formalized mathematics together

The Lean Seminar is a weekly gathering for exploring the Lean programming language and theorem prover.

Join the seminar mailing list

Useful links

Lean resources

Lean The official Lean website Mathlib search Search the mathematical library Learning Lean Guides from the Lean community Mathematics in Lean An interactive textbook Try Lean online Use Lean in your browser Lean games Learn Lean through interactive games

Weekly meetings

Fall 2026 schedule

September 1–December 8, 2026

Sep 1

Introduction and first functions

Brendan Murphy and Brian Nugent
Download FirstFunctions.lean
Sep 8

Rational and irrational numbers

Brian Nugent
Download RationalIrrational.lean
Sep 15

Installing Lean locally and induction

Karl Schwede
Download LeanInductionWorksheet.lean
Sep 22

Rings, ideals, and homomorphisms

Brian Nugent
Download RingsIdealsHoms.lean
Sep 29

Analysis & Calculus

Brendan Murphy
Download AnalysisWorksheet.lean
Oct 6
Topic to be announced
Karl Schwede
Oct 13
No meeting
Fall Break
Oct 20
Topic to be announced
Presenter to be announced
Oct 27
Topic to be announced
Presenter to be announced
Nov 3
Topic to be announced
Presenter to be announced
Nov 10
Topic to be announced
Presenter to be announced
Nov 17
Topic to be announced
Presenter to be announced
Nov 24
Topic to be announced
Presenter to be announced
Dec 1
Topic to be announced
Presenter to be announced
Dec 8
Topic to be announced
Presenter to be announced