diff --git a/init.example.el b/init.example.el
index fec33a81c..39303ef3f 100644
--- a/init.example.el
+++ b/init.example.el
@@ -118,6 +118,7 @@
        ;;julia             ; a better, faster MATLAB
        ;;kotlin            ; a better, slicker Java(Script)
        ;;latex             ; writing papers in Emacs has never been so fun
+       ;;lean
        ;;ledger            ; an accounting system in Emacs
        ;;lua               ; one-based indices? one-based indices
        markdown          ; writing docs for people to ignore
diff --git a/modules/lang/lean/config.el b/modules/lang/lean/config.el
new file mode 100644
index 000000000..3cff278d5
--- /dev/null
+++ b/modules/lang/lean/config.el
@@ -0,0 +1,36 @@
+;;; lang/lean/config.el -*- lexical-binding: t; -*-
+
+(after! lean-mode
+  (set-lookup-handlers! 'lean-mode
+    :definition #'lean-find-definition)
+  (sp-with-modes 'lean-mode
+    (sp-local-pair "/-" "-/")
+    (sp-local-pair "`" "`")
+    (sp-local-pair "{" "}")
+    (sp-local-pair "«" "»")
+    (sp-local-pair "⟨" "⟩")
+    (sp-local-pair "⟪" "⟫"))
+  (map! :map lean-mode-map
+        :localleader
+        "g" #'lean-toggle-show-goal
+        "n" #'lean-toggle-next-error
+        (:prefix ("s" . "server")
+          "r" #'lean-server-restart
+          "s" #'lean-server-stop
+          "v" #'lean-server-switch-version)
+        (:prefix ("p" . "leanpkg")
+          "t" #'lean-leanpkg-test
+          "b" #'lean-leanpkg-build
+          "c" #'lean-leanpkg-configure)
+        "f" #'lean-fill-placeholder
+        "h" #'lean-hole
+        "m" #'lean-message-boxes-toggle
+        "e" #'lean-execute))
+
+
+(use-package! company-lean
+  :init
+  (advice-add #'company-lean-hook :override #'ignore)
+  (set-company-backend! 'lean-mode 'company-lean)
+  :when (featurep! :completion company)
+  :after lean-mode)
diff --git a/modules/lang/lean/packages.el b/modules/lang/lean/packages.el
new file mode 100644
index 000000000..6061c61f6
--- /dev/null
+++ b/modules/lang/lean/packages.el
@@ -0,0 +1,7 @@
+;; -*- no-byte-compile: t; -*-
+;;; lang/lean/packages.el
+
+(package! lean-mode)
+
+(when (featurep! :completion company)
+  (package! company-lean))