Lean online learning seminar

The seminar during Fall 2025 was organized by Ben Chow (UCSD) and Zilu Ma (UT Knoxville). This quarter we had 7 talks by Lean experts. As mathematics grows increasingly complex, the formalization of mathematics is becoming ever more important. Lean is a leading tool for the formalization of mathematics.

Fall 2025 schedule of talks

VIDEOS of Fall 2025 Lean Lectures (on YouTube) With the permissions of the speakers, we have posted videos here.

Lean Texts and Documentation

Start coding in Lean now: https://live.lean-lang.org/

https://github.com/leanprover-community/mathlib4

https://leansearch.net/

https://loogle.lean-lang.org

Lean Zulip Chat: https://leanprover.zulipchat.com/

Questions I have about differential geometry in Lean. Includes SOTA reply by Michael Rothgang.

Current Work in Differential Geometry

Workshops:
Techniques and Tools for the Formalization of Analysis May 11 - 15, 2026
ItaLean 2025 Bridging Formal Mathematics and AI Bologna, Italy - December 9-12, 2025
Geometry of Machine Learning September 15 - 18, 2025
Simons Lean Workshop (New York City on June 16 - 25, 2025) Original Workshop Site

The Mathlib Initiative
mathlib-initiative.org

Lean Autoformalization:
math.inc

Platform for Collaborative Mathematical Formalization
Infinity Archive

Projects:
Geometric Analysis

Glossary of Lean and Mathlib Terms

Lean: A proof assistant based on dependent type theory. You write both mathematics and proofs in a formal language Lean can check.
mathlib: The main mathematics library for Lean, developed collaboratively on GitHub.
Tactic mode: Proof-writing style using Lean tactics (rw, apply, intro, etc.) in an imperative sequence.
Term mode: Proofs written as direct expressions (terms), often concise but requiring more familiarity with Lean syntax.
Tactic: A single command that transforms the current proof state (e.g., rw rewrites using an equation, apply applies a theorem).
rw: "Rewrite": replaces a term using a known equality.
simp: "Simplify": applies a large collection of rewrite lemmas to simplify the goal.
ring: Tactic that proves equalities in commutative rings using algebraic normalization.
intro / rintro: Introduces assumptions or hypotheses into the proof context.
calc: Block syntax for writing chained equalities/inequalities step-by-step.
structure: Lean's way of defining a record type with named fields (e.g., a group, a topological space).
instance: A declaration that registers that a type has a certain structure (e.g., ℝ is a topological space).
PR (Pull Request): A request to merge changes from a developer's branch into the main mathlib repository.
feat:: Commit/PR label meaning "feature" (adding something new).
refactor:: Commit/PR label for reorganizing/improving existing code without changing mathematical meaning.
golf: Shortening a proof while keeping it correct (like golf's fewest strokes).
upstream: The main mathlib repository.
downstream: Your own copy or fork of mathlib.
fork: Your personal copy of the repository on GitHub, where you can make changes.
push: Upload commits from your local computer to a remote repository (e.g., your fork).
pull: Download commits from a remote repository to your local copy.