Skip to main
Math equations
George Mason University

Lean Learning Seminar

Lean Learning Seminar

This is an informal learning seminar dedicated to learning the formalization of mathematical proofs in Lean4. Anyone who has taken some kind of an intro to proofs class would be able to participate without issue.

Why learn Lean? In 2013, Leonardo de Moura created Lean, a programming language which is a proof assistant.  In particular, it is possible to formalize mathematical proofs in such a way that the logic itself can be validated by a computer. Recent progress has been incredible. The Mathlib library contains formalizations of over 210,000 theorems. Celebrated mathematicians such as Thomas Hales, Kevin Buzzard, and Terence Tao have been great advocates of formalizing proofs in Lean4. Using a combination of Lean and a variety of LLM wrappers (such as GoogleProof and Aristotle) have produced new proofs of unknown results, in addition to being able to automatically perform at prize-winning levels on Math Olympiad and other competitions. In the writeup of his ICM  talk, Alex Kontorovich predicts that formalization of mathematics will win out as the standard of proof.  The goal is to be proactive and learn Lean before it becomes an existential necessity for all mathematicians. 

Meets on Wednesdays at 1:30pm in Exploratory Hall, room 4208

 

Fall 2026

 

 

* The programs and services offered by George Mason University are open to all who seek them. George Mason does not discriminate on the basis of race, color, religion, ethnic national origin (including shared ancestry and/or ethnic characteristics), sex, disability, military status (including veteran status), sexual orientation, gender identity, gender expression, age, marital status, pregnancy status, genetic information, or any other characteristic protected by law. After an initial review of its policies and practices, the university affirms its commitment to meet all federal mandates as articulated in federal law, as well as recent executive orders and federal agency directives.