diff --git a/nvim/.config/nvim/after/ftplugin/lean.lua b/nvim/.config/nvim/after/ftplugin/lean.lua
new file mode 100644
index 0000000..5e8994c
--- /dev/null
+++ b/nvim/.config/nvim/after/ftplugin/lean.lua
@@ -0,0 +1,4 @@
+local lsp_utils     = require('lsp-utils')
+local leanls_config = lsp_utils.leanls_config()
+
+vim.lsp.start(leanls_config)
diff --git a/nvim/.config/nvim/lua/lsp-utils.lua b/nvim/.config/nvim/lua/lsp-utils.lua
index c2b3627..2ca1b63 100644
--- a/nvim/.config/nvim/lua/lsp-utils.lua
+++ b/nvim/.config/nvim/lua/lsp-utils.lua
@@ -201,6 +201,20 @@ function M.hls_config()
   }
 end
 
+function M.leanls_config()
+  local root_files     = { 'lakefile.lean', 'lean-toolchain', 'leanpkg.toml' }
+  local root_directory = get_root_directory(root_files)
+
+  return {
+    name                = "leanls",
+    cmd                 = { 'lake', 'serve', '--' },
+    capabilities        = default_capabilities,
+    root_dir            = root_directory,
+    filetypes           = { 'lean' },
+    single_file_support = true,
+  }
+end
+
 function M.pursls_config()
   local root_files     = { 'bower.json', 'psc-package.json', 'spago.dhall' }
   local root_directory = get_root_directory(root_files)
diff --git a/nvim/.config/nvim/lua/treesitter.lua b/nvim/.config/nvim/lua/treesitter.lua
index 03f932e..4c4116e 100644
--- a/nvim/.config/nvim/lua/treesitter.lua
+++ b/nvim/.config/nvim/lua/treesitter.lua
@@ -17,5 +17,13 @@ require'nvim-treesitter.configs'.setup {
   },
 }
 
+require "nvim-treesitter.parsers".get_parser_configs().lean = {
+  filetype     = "lean",
+  install_info = {
+    url   = "~/GitSources/tree-sitter-lean",
+    files = {"src/parser.c", "src/scanner.cc"},
+  },
+}
+
 vim.keymap.set('o', '<Leader>m', ':<C-U>lua require(\'tsht\').nodes()<CR>', { noremap=false, unique=true, silent=true })
 vim.keymap.set('x', '<Leader>m', ':lua require(\'tsht\').nodes()<CR>' , { noremap=true , unique=true, silent=true })
diff --git a/nvim/.config/nvim/queries/lean/folds.scm b/nvim/.config/nvim/queries/lean/folds.scm
new file mode 100644
index 0000000..2c2bbb3
--- /dev/null
+++ b/nvim/.config/nvim/queries/lean/folds.scm
@@ -0,0 +1,15 @@
+[
+  (namespace)
+  (section)
+
+  (instance)
+  (def)
+  (theorem)
+  (example)
+
+  (product)
+  (array)
+  (list)
+
+  (string)
+] @fold
diff --git a/nvim/.config/nvim/queries/lean/highlights.scm b/nvim/.config/nvim/queries/lean/highlights.scm
new file mode 100644
index 0000000..5ede057
--- /dev/null
+++ b/nvim/.config/nvim/queries/lean/highlights.scm
@@ -0,0 +1,216 @@
+(open
+  namespace: (identifier) @namespace)
+(namespace
+  name: (identifier) @namespace)
+(section
+  name: (identifier) @namespace)
+
+(arrow) @type
+(product) @type
+
+;; Declarations
+
+[
+  "abbrev"
+  "def"
+  "theorem"
+  "constant"
+  "instance"
+  "axiom"
+  "example"
+  "inductive"
+  "structure"
+  "class"
+
+  "deriving"
+
+  "section"
+  "namespace"
+] @keyword
+
+(attributes
+  (identifier) @function)
+
+(abbrev
+  name: (identifier) @type)
+(def
+  name: (identifier) @function)
+(theorem
+  name: (identifier) @function)
+(constant
+  name: (identifier) @type)
+(instance
+  name: (identifier) @function)
+(instance
+  type: (identifier) @type)
+(axiom
+  name: (identifier) @function)
+(structure
+  name: (identifier) @type)
+(structure
+  extends: (identifier) @type)
+
+(where_decl
+  type: (identifier) @type)
+
+(implicit_binder
+    type: (identifier) @type)
+(explicit_binder
+    type: (identifier) @type)
+
+(proj
+  name: (identifier) @field)
+
+(binders
+  type: (identifier) @type)
+
+["if" "then" "else"] @conditional
+
+["for" "in" "do"] @repeat
+
+(import) @include
+
+; Tokens
+
+[
+  "!"
+  "$"
+  "%"
+  "&&"
+  "*"
+  "*>"
+  "+"
+  "++"
+  "-"
+  "/"
+  "::"
+  ":="
+  "<"
+  "<$>"
+  "<*"
+  "<*>"
+  "<="
+  "<|"
+  "<|>"
+  "="
+  "=="
+  "=>"
+  ">"
+  ">"
+  ">="
+  ">>"
+  ">>="
+  "@"
+  "^"
+  "|>"
+  "|>."
+  "||"
+  "←"
+  "→"
+  "↔"
+  "∘"
+  "∧"
+  "∨"
+  "≠"
+  "≤"
+  "≥"
+] @operator
+
+[
+  "@&"
+] @operator
+
+[
+  "attribute"
+  "by"
+  "end"
+  "export"
+  "extends"
+  "fun"
+  "let"
+  "have"
+  "match"
+  "open"
+  "return"
+  "universe"
+  "variable"
+  "where"
+  "with"
+  "λ"
+  (hash_command)
+  (prelude)
+  (sorry)
+] @keyword
+
+[
+  "prefix"
+  "infix"
+  "infixl"
+  "infixr"
+  "postfix"
+  "notation"
+  "macro"
+  "macro_rules"
+  "syntax"
+  "elab"
+  "builtin_initialize"
+] @keyword
+
+[
+  "noncomputable"
+  "partial"
+  "private"
+  "protected"
+  "unsafe"
+] @keyword
+
+[
+  "apply"
+  "exact"
+  "rewrite"
+  "rw"
+  "simp"
+  (trivial)
+] @keyword
+
+[
+  "catch"
+  "finally"
+  "try"
+] @exception
+
+((apply
+  name: (identifier) @exception)
+ (#match? @exception "throw"))
+
+[
+  "unless"
+  "mut"
+] @keyword
+
+[(true) (false)] @boolean
+
+(number) @number
+(float) @float
+
+(comment) @comment
+(char) @character
+(string) @string
+(interpolated_string) @string
+(quoted_char) @string.escape
+
+; Reset highlighing in string interpolation
+(interpolation) @none
+
+(interpolation
+  "{" @punctuation.special
+  "}" @punctuation.special)
+
+["(" ")" "[" "]" "{" "}" "⟨" "⟩"] @punctuation.bracket
+
+["|" "," "." ":" ";"] @punctuation.delimiter
+
+(sorry) @error
+
+;; Error
+(ERROR) @error
diff --git a/nvim/.config/nvim/queries/lean/injections.scm b/nvim/.config/nvim/queries/lean/injections.scm
new file mode 100644
index 0000000..5078159
--- /dev/null
+++ b/nvim/.config/nvim/queries/lean/injections.scm
@@ -0,0 +1,2 @@
+((comment) @markdown
+  (#offset! @markdown 0 3 0 -2))
diff --git a/nvim/.config/nvim/queries/lean/locals.scm b/nvim/.config/nvim/queries/lean/locals.scm
new file mode 100644
index 0000000..c3109e8
--- /dev/null
+++ b/nvim/.config/nvim/queries/lean/locals.scm
@@ -0,0 +1,3 @@
+(module) @scope
+(namespace) @scope
+(section) @scope