diff --git a/data/courses.yaml b/data/courses.yaml
index b2276f4dc..1b62ef41c 100644
--- a/data/courses.yaml
+++ b/data/courses.yaml
@@ -624,3 +624,20 @@
     This course really works well, and it will probably continue for a long time.
     The idea to use controlled natural language tactics seems a lot more efficient than the native syntax to ensure students improve at pen and paper proofs.
   year: 2025
+- name: Functional Programming and Theorem Proving in Lean 4
+  instructor: Leni Aniva, Abdalrhman Mohamed
+  institution: Stanford University
+  website: https://web.stanford.edu/class/cs99/
+  tags: ['English', 'computer science', 'mathematics', 'functional programming', 'theorem proving', 'metaprogramming']
+  year: 2025
+  lean_version: 4
+  summary: >
+    This course gives a systematic introduction to Lean 4, first as a functional
+    programming language, and then a theorem prover. We explain the type
+    theoretic foundations of Lean and show examples of theorem proving and
+    tactics. The last part of the course covers Lean's compiler and
+    metaprogramming system. The course is intended for both mathematicians and
+    computer scientists. The contents covered include: Type Polymorphism,
+    Monads, CIC, Subtyping, Tactics, Logic, Sets, Computability, Termination,
+    Metaprogramming, Macros, Elaboration, Type Unification, and relevant works
+    in other proof assistants.