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
analysis
automated reasoning
beginner
computer science
formal verification
functional programming
intro to proof
lean4
logic
mathematics
natural language input
Instructor | Title | Location | Year | Tags | |
---|---|---|---|---|---|
Floris van Doorn | Collaborative Formalization in Analysis | University of Bonn | 2024 | advanced, analysis, mathematics, lean4 | |
Ralf Gerkmann | Computergestütztes mathematisches Beweisen | Ludwig-Maximilians-Universität München | 2024 | German, mathematics, lean4 | |
Heather Macbeth | Discrete Mathematics | Fordham University | 2024 | intro to proof, mathematics, lean4 | |
Thomas Henzinger, Stefanie Muroya Lei, Martin Dvořák | Formalisms Every Computer Scientist Should Know | Institute of Science and Technology, Austria | 2024 | advanced, computer science, formal verification, lean4 | |
Stavan Jain, Ricardo Prado Cunha and Anoushka Sinha (supervised by Colleen Robles) | Formalization of Mathematics: Seminar on the proof assistant Lean | Duke University | 2024 | beginner, mathematics, lean4 | |
Floris van Doorn | Formalized Mathematics in Lean | University of Bonn | 2024 | advanced, mathematics, lean4 | |
Jasmin Blanchette | Interactive Theorem Proving | Ludwig-Maximilians-Universität München | 2024 | computer science, lean4 | |
Sophie Morel, Filippo A. E. Nuccio, Xavier Roblot | Introduction to Lean and Advanced projects on Lean | ENS-Lyon, Université Claude Bernard Lyon, Université Jean Monnet Saint-Étienne | 2024 | mathematics, lean4 | |
Vasily Ilin | Introduction to Mathematical Formalization | University of Washington | 2024 | English, beginner, mathematics, lean4 | |
Tyler R. Josephson | Lean for Scientists and Engineers | University of Maryland, Baltimore County | 2024 | beginner, functional programming, intro to proof, lean4 | |
Martin Dvorak | Programování a dokazování v Leanu | online | 2024 | Czech, functional programming, intro to proof, lean4 | |
Thomas Noll | Semantics and Verification of Software | RWTH Aachen University | 2024 | beginner, computer science, lean4 | |
André Greiner-Petter, Moritz Schubotz, Bela Gipp | Seminar: Mathematical Information Retrieval (MathIR) | University of Göttingen, Germany | 2024 | beginner, computer science, mathematics, lean4 | |
Alexander Bentkamp, Jon Eugster | Computergestützte Beweisführung | Heinrich-Heine-Universität Düsseldorf | 2023 | German, beginner, lean4, 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 | |
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 | |
Jun Li | Set Theory and Logic with Lean | University of Dayton, USA | 2023 | English, intro to proof, logic, 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 |