Courses using Lean
We maintain a list here of past and future courses either using Lean to teach mathematics, or directly teaching Lean as an interactive theorem prover or programming language. Please add courses by making a pull request editing courses.yaml.
Select tags to start filtering:
lean4
lean3
Catalan
Czech
English
French
German
Spanish
advanced
automated reasoning
beginner
computer science
functional programming
intro to proof
logic
mathematics
natural language input
Instructor | Title | Location | Year | Tags | |
---|---|---|---|---|---|
Heather Macbeth | Discrete Mathematics | Fordham University | 2023 | intro to proof, mathematics, lean4 | |
Robert Y. Lewis | Discrete Structures and Probability | Brown University | 2023 | computer science, intro to proof, lean4 | |
Riccardo Brasca and Antoine Chambert-Loir | Démontrer avec un ordinateur | Université Paris Cité, France | 2023 | French, intro to proof, mathematics, lean4 | |
Jim Fowler | Formal Proof | The Ohio State University | 2023 | advanced, mathematics, lean4 | |
Robert Y. Lewis | Formal Proof and Verification | Brown University | 2023 | advanced, computer science, logic, lean4 | |
Matthew Ballard | Formalization and mathematics | University of South Carolina | 2023 | advanced, computer science, mathematics, lean4 | |
Matthew Ballard | Formalization of mathematics | University of South Carolina | 2023 | advanced, mathematics, lean4 | |
Floris van Doorn | Formalized Mathematics in Lean | University of Bonn | 2023 | advanced, mathematics, lean4 | |
Siddhartha Gadgil | Proofs and Programs | Indian Institute of Science, Bangalore | 2023 | computer science, intro to proof, lean4 | |
Enric Cosme Llópez | Taller de Lean 4 | Universitat de València | 2023 | Catalan, mathematics, lean4 | |
Damiano Testa | Theorem Proving with Lean | University of Warwick | 2023 | advanced, mathematics, lean4 | |
Patrick Massot | Topics in formal mathematics | Carnegie Mellon University | 2023 | mathematics, lean4 | |
Martin Dvorak | Programování a dokazování v Leanu | online | 2022 | Czech, functional programming, intro to proof, lean4 | |
Jakob von Raumer | Theorem Prover Lab -- Applications in Programming Languages | Karlsruhe Institute of Technology | 2022 | German, advanced, computer science, lean4 | |
Matthew Ballard | Transition to Advanced Mathematics | University of South Carolina | 2022 | intro to proof, mathematics, lean4 | |
Jeremy Avigad | Logic and Mechanized Reasoning | Carnegie Mellon University | 2021 | advanced, automated reasoning, logic, lean4 | |
Frédéric Tran Minh | Complement to general Analysis/Algebra 1st year undergraduate course | Esisar, Grenoble Institute of Technology | 2023 | French, intro to proof, mathematics, lean3 | |
Kevin Buzzard | Formalising Mathematics 2023 | Imperial College London | 2023 | advanced, mathematics, lean3 | |
Bjørn Kjos-Hanssen | Graduate Introduction to Logic | University of Hawaii at Manoa | 2023 | advanced, logic, mathematics, lean3 | |
Philip Matchett Wood | Introduction to formal verification of mathematics | Harvard University | 2023 | mathematics, lean3 | |
Patrick Kinnear | Lean learning group 2023 | Glasgow-Maxwell School | 2023 | advanced, mathematics, lean3 | |
Robert Y. Lewis, Jasmin Blanchette, Anne Baanen | Logic and Modelling | Vrije Universiteit Amsterdam | 2023 | computer science, intro to proof, logic, lean3 | |
Patrick Massot | Logique et démonstrations assistées par ordinateur | Université Paris-Saclay | 2023 | French, intro to proof, natural language input, lean3 | |
Marc Masdeu, Roberto Rubio | Poden els ordinadors entendre les matemàtiques? De la geometria axiomàtica als theorem provers | Universitat Autònoma de Barcelona | 2023 | Catalan, English, beginner, mathematics, lean3 | |
Peter Pfaffelhuber | Some high-school mathematics in Lean | University of Freiburg, Germany | 2023 | German, intro to proof, mathematics, lean3 | |
Miguel Marco | Topología general | Universidad de Zaragoza | 2023 | Spanish, mathematics, lean3 | |
Jeremy Avigad | Interactive Theorem Proving | Carnegie Mellon University | 2022 | mathematics, lean3 | |
Sina Hazratpour | Introduction to Proofs with Lean Proof Assistant | Johns Hopkins University | 2022 | intro to proof, mathematics, lean3 | |
Gihan Marasingha | Modern Mathematics with Lean | University of Exeter | 2022 | intro to proof, logic, mathematics, lean3 | |
Jeremy Avigad | Logic and Proof | Carnegie Mellon University | 2017 | intro to proof, logic, lean3 |