diff --git a/+lang/lean/config.el b/+lang/lean/config.el
new file mode 100644
index 0000000..c8be573
--- /dev/null
+++ b/+lang/lean/config.el
@@ -0,0 +1,20 @@
+;;; config.el --- Lean Layer config File for Spacemacs
+;;
+;; Copyright (c) 2019 Vierkantor
+;;
+;; Based on Agda2 Layer for Spacemacs by
+;; Author: FreeSalad <freesalad@noreply.git>
+;; URL: https://github.com/syl20bnr/spacemacs
+;;
+;; This file is not part of GNU Emacs.
+;;
+;;; License: GPLv3
+
+;; (defvar agda-mode-path 'use-helper
+;;  "Indicates the location of the agda-mode package (the file
+;; `agda2.el') If `nil', it is assumed to be already available by
+;; Emacs. If `use-helper', the `agda-mode' executable is used to
+;; find its location.")
+
+(spacemacs|define-jump-handlers agda2-mode lean-find-definition)
+(spacemacs|defvar-company-backends lean-mode)
diff --git a/+lang/lean/packages.el b/+lang/lean/packages.el
new file mode 100644
index 0000000..9745d61
--- /dev/null
+++ b/+lang/lean/packages.el
@@ -0,0 +1,46 @@
+;;; packages.el --- Lean Layer packages File for Spacemacs
+;;
+;; Based on Agda Layer for Spacemacs by:
+;; Author: Oliver Charles <ollie@ocharles.org.uk>
+;; URL: https://github.com/syl20bnr/spacemacs
+;;
+;; This file is not part of GNU Emacs.
+;;
+;;; License: GPLv3
+
+(defconst lean-packages
+      '((lean-mode :location elpa)
+        company
+        company-lean
+        helm-lean
+        golden-ratio))
+
+(defun lean/post-init-company ()
+  (spacemacs|add-company-hook lean-mode)
+  (push 'company-capf company-backends-lean-mode))
+
+(defun lean/post-init-company-lean ())
+(defun lean/post-init-helm-lean ())
+
+(defun lean/init-lean-mode ()
+    (use-package lean-mode
+      :defer t
+      :config
+      (progn
+        (spacemacs/set-leader-keys-for-major-mode 'lean-mode
+	  " "   'company-complete
+          "."   'lean-toggle-show-goal
+          "d"   'helm-lean-definitions
+          "f"   'lean-toggle-next-error
+          "g"   'lean-find-definition
+          "k"   'quail-show-key
+          "l"   'lean-std-exe
+          "r"   'lean-hole
+          "xr"  'lean-server-restart
+          "xs"  'lean-server-switch-version))))
+
+(defun lean/pre-init-golden-ratio ()
+  (spacemacs|use-package-add-hook golden-ratio
+    :post-config
+    (add-to-list 'golden-ratio-exclude-buffer-names
+                 "*Lean information*")))