diff --git a/radix/packages/emacs-xyz.scm b/radix/packages/emacs-xyz.scm
new file mode 100644
index 0000000..0bcf98a
--- /dev/null
+++ b/radix/packages/emacs-xyz.scm
@@ -0,0 +1,32 @@
+(define-module (radix packages emacs-xyz)
+  #:use-module (guix packages)
+  #:use-module (guix git-download)
+  #:use-module (guix build-system emacs)
+  #:use-module ((guix licenses)
+                #:prefix license:)
+  #:use-module (gnu packages emacs-xyz))
+
+(define-public emacs-lean4-mode
+  (let ((commit "da7b63d854d010d621e2c82a53d6ae2d94dd53b0")
+        (revision "0"))
+    (package
+      (name "emacs-lean4-mode")
+      (version (git-version "0.0.0" revision commit))
+      (source (origin
+                (method git-fetch)
+                (uri (git-reference
+                      (url "https://github.com/leanprover/lean4-mode/")
+                      (commit commit)))
+                (file-name (git-file-name name version))
+                (sha256
+                 (base32 "1va1ini3cbsmdrbab17kiwbn2h6b0jc8lb3vabmmazsrq0hhk8sk"))))
+      (inputs (list emacs-flycheck
+                    emacs-lsp-mode
+                    emacs-magit))
+      (build-system emacs-build-system)
+      (synopsis "Lean4 Emacs mode")
+      (description "Lean4 Emacs mode for the interactive proof assistant Lean4")
+      (home-page "https://github.com/leanprover/lean4-mode")
+      (license license:asl2.0))))
+
+emacs-lean4-mode