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 MacbethDiscrete MathematicsFordham University2023intro to proof, mathematics, lean4
Robert Y. LewisDiscrete Structures and ProbabilityBrown University2023computer science, intro to proof, 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
Robert Y. LewisFormal Proof and VerificationBrown University2023advanced, computer science, logic, 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
Martin DvorakProgramování a dokazování v Leanuonline2022Czech, functional programming, intro to proof, 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
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