diff --git a/modules/lang/lean/README.org b/modules/lang/lean/README.org
index e12c17632..515fa316a 100644
--- a/modules/lang/lean/README.org
+++ b/modules/lang/lean/README.org
@@ -4,16 +4,24 @@
 #+since:    21.12.0 (#1759)
 
 * Description :unfold:
-This module adds support for the [[https://leanprover.github.io/about/][Lean programming language]] to Doom Emacs.
+This module adds support for the [[https://leanprover.github.io/about/][Lean programming language]] to Doom Emacs. It
+supports Lean 4 by default (powered by [[doom-package:nael]]), with optional support
+for Lean 3 behind a [[doom-module:+v3]] flag.
 
 ** Maintainers
 /This module has no dedicated maintainers./ [[doom-contrib-maintainer:][Become a maintainer?]]
 
 ** Module flags
-/This module has no flags./
+- +lsp ::
+  Enable LSP support for ~nael-mode~ (Lean 4). Requires [[doom-module::tools lsp]] and
+  an LSP server (e.g. [[https://github.com/leanprover/lean4/tree/master/src/lake][Lake]]). There no LSP support for Lean 3.
+- +v3 ::
+  Include Lean 3 support, powered by [[doom-package:lean-mode]].
 
 ** Packages
-- [[doom-package:lean-mode]]
+- [[doom-package:lean-mode]] if [[doom-module:+v3]]
+- [[doom-package:nael]]
+- [[doom-package:nael-lsp]] if [[doom-module:+lsp]] + [[doom-module::tools lsp -eglot]]
 
 ** TODO Hacks
 #+begin_quote
@@ -31,6 +39,11 @@ This module adds support for the [[https://leanprover.github.io/about/][Lean pro
  󱌣 /This module's prerequisites are not documented./ [[doom-contrib-module:][Document them?]]
 #+end_quote
 
+- Lean 4 requires the ~lean4~ executable (and ~lake~ if LSP support is wanted) in
+  your ~$PATH~.
+- Lean 3 requires the ~lean3~ and ~leanpkg~ executables.
+- For LSP support,
+
 * TODO Usage
 #+begin_quote
  󱌣 This module has no usage documentation yet. [[doom-contrib-module:][Write some?]]
diff --git a/modules/lang/lean/config.el b/modules/lang/lean/config.el
index 70c984e2e..36700a23d 100644
--- a/modules/lang/lean/config.el
+++ b/modules/lang/lean/config.el
@@ -1,6 +1,9 @@
 ;;; lang/lean/config.el -*- lexical-binding: t; -*-
 
-(after! lean-mode
+(use-package! lean-mode  ; lean 3 support
+  :when (modulep! +v3)
+  :defer t
+  :config
   (set-lookup-handlers! 'lean-mode
     :definition #'lean-find-definition)
   (sp-with-modes 'lean-mode
@@ -26,3 +29,43 @@
         "h" #'lean-hole
         "m" #'lean-message-boxes-toggle
         "e" #'lean-execute))
+
+
+(use-package! nael  ; lean 4 support
+  :defer t
+  :init
+  (add-hook 'nael-mode-hook #'abbrev-mode)
+  (after! org-src
+    (add-to-list 'org-src-lang-modes '("lean" . nael)))
+  (after! markdown-mode
+    (add-to-list 'markdown-code-lang-modes '("lean" . nael-mode)))
+  :config
+  (sp-with-modes 'nael-mode
+    (sp-local-pair "/-" "-/")
+    (sp-local-pair "`" "`")
+    (sp-local-pair "{" "}")
+    (sp-local-pair "«" "»")
+    (sp-local-pair "⟨" "⟩")
+    (sp-local-pair "⟪" "⟫"))
+  (when (modulep! +lsp)
+    (if (modulep! :tools lsp +eglot)
+        (setq nael-prepare-lsp nil)
+      (setq nael-prepare-eglot nil))
+    (add-hook 'nael-mode-local-vars-hook #'lsp! 'append))
+  (map! :map lean-mode-map
+        :localleader
+        "a" #'nael-abbrev-help
+        "b" #'project-build     ; REVIEW: redundant with '<leader> p'?
+        "e" #'eldoc-doc-buffer  ; REVIEW: redundant with +lookup/documentation?
+        (: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))
diff --git a/modules/lang/lean/packages.el b/modules/lang/lean/packages.el
index d4d415a96..93e177ac1 100644
--- a/modules/lang/lean/packages.el
+++ b/modules/lang/lean/packages.el
@@ -1,4 +1,10 @@
 ;; -*- no-byte-compile: t; -*-
 ;;; lang/lean/packages.el
 
-(package! lean-mode :pin "99d6a34dc5b12f6e996e9217fa9f6fe4a6af037a")
+(when (modulep! +v3)
+  (package! lean-mode :pin "99d6a34dc5b12f6e996e9217fa9f6fe4a6af037a"))
+
+(package! nael :pin "101726eb47fc2562f49e9e7c1de4fc959229ca0c")
+(when (and (modulep! +lsp)
+           (modulep! :tools lsp -eglot))
+  (package! nael-lsp :pin "101726eb47fc2562f49e9e7c1de4fc959229ca0c"))