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 metaprogramming natural language input theorem proving

Instructor Title Location Year Tags
Assaf KfouryCombinatoric StructuresBoston University2025beginner, computer science, lean4
Judith Ludwig and Florent SchaffhauserComputer-assisted MathematicsHeidelberg University, Heidelberg (Germany)2025beginner, logic, mathematics, lean4
Assaf KfouryFormal Methods for High-Assurance Software EngineeringBoston University2025computer science, mathematics, lean4
Leni Aniva, Abdalrhman MohamedFunctional Programming and Theorem Proving in Lean 4Stanford University2025English, computer science, functional programming, mathematics, metaprogramming, theorem proving, lean4
Florent SchaffhauserInteractive Theorem Proving in LeanMax Planck Institute for Mathematics in the Sciences, Leipzig (Germany)2025beginner, logic, mathematics, lean4
Patrick Massot, Valérie de Clippel, Christine PaulinLogique et démonstrations assistées par ordinateurUniversité Paris-Saclay2025French, intro to proof, natural language input, lean4
Antoine Meyer and Marie-Hélène MourguesLogique et preuve assistée (Logic and computer-assisted proof)Université Gustave Eiffel, Paris area, France2025computer science, logic, mathematics, lean4
Filippo A. E. NuccioPreuve assistée par ordinateur dans Lean (Assisted proofs in Lean)CS/Math Lyon Graduate School, France2025mathematics, lean4
Floris van DoornCollaborative Formalization in AnalysisUniversity of Bonn2024advanced, analysis, mathematics, lean4
Ralf GerkmannComputergestütztes mathematisches BeweisenLudwig-Maximilians-Universität München2024German, mathematics, lean4
Heather MacbethDiscrete MathematicsFordham University2024intro to proof, mathematics, lean4
Robert Y. LewisDiscrete Structures and ProbabilityBrown University2024computer science, intro to proof, lean4
Robert Y. LewisFormal Proof and VerificationBrown University2024advanced, computer science, logic, lean4
Thomas Henzinger, Stefanie Muroya Lei, Martin DvořákFormalisms Every Computer Scientist Should KnowInstitute of Science and Technology, Austria2024advanced, 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 LeanDuke University2024beginner, mathematics, lean4
Floris van DoornFormalized Mathematics in LeanUniversity of Bonn2024advanced, mathematics, lean4
Kevin BuzzardFormalizing Mathematics 2024Imperial College London2024English, beginner, mathematics, lean4
Jasmin BlanchetteInteractive Theorem ProvingLudwig-Maximilians-Universität München2024computer science, lean4
Sophie Morel, Filippo A. E. Nuccio, Xavier RoblotIntroduction to Lean and Advanced projects on LeanENS-Lyon, Université Claude Bernard Lyon, Université Jean Monnet Saint-Étienne2024mathematics, lean4
Vasily IlinIntroduction to Mathematical FormalizationUniversity of Washington2024English, beginner, mathematics, lean4
Tyler R. JosephsonLean for Scientists and EngineersUniversity of Maryland, Baltimore County2024beginner, functional programming, intro to proof, lean4
Martin DvorakProgramování a dokazování v Leanuonline2024Czech, functional programming, intro to proof, lean4
Thomas NollSemantics and Verification of SoftwareRWTH Aachen University2024beginner, computer science, lean4
André Greiner-Petter, Moritz Schubotz, Bela GippSeminar: Mathematical Information Retrieval (MathIR)University of Göttingen, Germany2024beginner, computer science, mathematics, lean4
Alexander Bentkamp, Jon EugsterComputergestützte BeweisführungHeinrich-Heine-Universität Düsseldorf2023German, beginner, lean4, lean4
Riccardo Brasca and Antoine Chambert-LoirDémontrer avec un ordinateurUniversité Paris Cité, France2023French, intro to proof, mathematics, lean4
Jim FowlerFormal ProofThe Ohio State University2023advanced, mathematics, lean4
Matthew BallardFormalization and mathematicsUniversity of South Carolina2023advanced, computer science, mathematics, lean4
Matthew BallardFormalization of mathematicsUniversity of South Carolina2023advanced, mathematics, lean4
Floris van DoornFormalized Mathematics in LeanUniversity of Bonn2023advanced, mathematics, lean4
Siddhartha GadgilProofs and ProgramsIndian Institute of Science, Bangalore2023computer science, intro to proof, lean4
Enric Cosme LlópezTaller de Lean 4Universitat de València2023Catalan, mathematics, lean4
Damiano TestaTheorem Proving with LeanUniversity of Warwick2023advanced, mathematics, lean4
Patrick MassotTopics in formal mathematicsCarnegie Mellon University2023mathematics, lean4
Jakob von RaumerTheorem Prover Lab -- Applications in Programming LanguagesKarlsruhe Institute of Technology2022German, advanced, computer science, lean4
Matthew BallardTransition to Advanced MathematicsUniversity of South Carolina2022intro to proof, mathematics, lean4
Jeremy AvigadLogic and Mechanized ReasoningCarnegie Mellon University2021advanced, automated reasoning, logic, lean4
Frédéric Tran MinhComplement to general Analysis/Algebra 1st year undergraduate courseEsisar, Grenoble Institute of Technology2023French, intro to proof, mathematics, lean3
Kevin BuzzardFormalising Mathematics 2023Imperial College London2023advanced, mathematics, lean3
Bjørn Kjos-HanssenGraduate Introduction to LogicUniversity of Hawaii at Manoa2023advanced, logic, mathematics, lean3
Philip Matchett WoodIntroduction to formal verification of mathematicsHarvard University2023mathematics, lean3
Patrick KinnearLean learning group 2023Glasgow-Maxwell School2023advanced, mathematics, lean3
Robert Y. Lewis, Jasmin Blanchette, Anne BaanenLogic and ModellingVrije Universiteit Amsterdam2023computer science, intro to proof, logic, lean3
Patrick MassotLogique et démonstrations assistées par ordinateurUniversité Paris-Saclay2023French, intro to proof, natural language input, lean3
Marc Masdeu, Roberto RubioPoden els ordinadors entendre les matemàtiques? De la geometria axiomàtica als theorem proversUniversitat Autònoma de Barcelona2023Catalan, English, beginner, mathematics, lean3
Jun LiSet Theory and Logic with LeanUniversity of Dayton, USA2023English, intro to proof, logic, lean3
Peter PfaffelhuberSome high-school mathematics in LeanUniversity of Freiburg, Germany2023German, intro to proof, mathematics, lean3
Miguel MarcoTopología generalUniversidad de Zaragoza2023Spanish, mathematics, lean3
Jeremy AvigadInteractive Theorem ProvingCarnegie Mellon University2022mathematics, lean3
Sina HazratpourIntroduction to Proofs with Lean Proof AssistantJohns Hopkins University2022intro to proof, mathematics, lean3
Gihan MarasinghaModern Mathematics with LeanUniversity of Exeter2022intro to proof, logic, mathematics, lean3
Jeremy AvigadLogic and ProofCarnegie Mellon University2017intro to proof, logic, lean3