diff --git a/.gitmodules b/.gitmodules
index 3442652a65a2..1ccbe43b86e5 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -190,6 +190,10 @@
 	path = helix-syntax/languages/tree-sitter-git-rebase
 	url = https://github.com/the-mikedavis/tree-sitter-git-rebase.git
 	shallow = true
+[submodule "helix-syntax/languages/tree-sitter-lean"]
+	path = helix-syntax/languages/tree-sitter-lean
+	url = https://github.com/Julian/tree-sitter-lean
+	shallow = true
 [submodule "helix-syntax/languages/tree-sitter-regex"]
 	path = helix-syntax/languages/tree-sitter-regex
 	url = https://github.com/tree-sitter/tree-sitter-regex.git
diff --git a/book/src/generated/lang-support.md b/book/src/generated/lang-support.md
index 8b599f6b4dc7..649f523d7e14 100644
--- a/book/src/generated/lang-support.md
+++ b/book/src/generated/lang-support.md
@@ -23,6 +23,7 @@
 | json | ✓ |  | ✓ |  |
 | julia | ✓ |  |  | `julia` |
 | latex | ✓ |  |  |  |
+| lean | ✓ |  |  | `lean` |
 | ledger | ✓ |  |  |  |
 | llvm | ✓ | ✓ | ✓ |  |
 | llvm-mir | ✓ | ✓ | ✓ |  |
diff --git a/helix-syntax/languages/tree-sitter-lean b/helix-syntax/languages/tree-sitter-lean
new file mode 160000
index 000000000000..d98426109258
--- /dev/null
+++ b/helix-syntax/languages/tree-sitter-lean
@@ -0,0 +1 @@
+Subproject commit d98426109258b266e1e92358c5f11716d2e8f638
diff --git a/languages.toml b/languages.toml
index 0a19bb0449d6..6b9237bb61e6 100644
--- a/languages.toml
+++ b/languages.toml
@@ -241,6 +241,17 @@ comment-token = "%"
 
 indent = { tab-width = 4, unit = "\t" }
 
+[[language]]
+name = "lean"
+scope = "source.lean"
+injection-regex = "lean"
+file-types = ["lean"]
+roots = [ "lakefile.lean" ]
+comment-token = "--"
+language-server = { command = "lean", args = [ "--server" ] }
+
+indent = { tab-width = 2, unit = "  " }
+
 [[language]]
 name = "julia"
 scope = "source.julia"
diff --git a/runtime/queries/lean/folds.scm b/runtime/queries/lean/folds.scm
new file mode 100644
index 000000000000..2c2bbb33ae23
--- /dev/null
+++ b/runtime/queries/lean/folds.scm
@@ -0,0 +1,15 @@
+[
+  (namespace)
+  (section)
+
+  (instance)
+  (def)
+  (theorem)
+  (example)
+
+  (product)
+  (array)
+  (list)
+
+  (string)
+] @fold
diff --git a/runtime/queries/lean/highlights.scm b/runtime/queries/lean/highlights.scm
new file mode 100644
index 000000000000..a64feb1d390d
--- /dev/null
+++ b/runtime/queries/lean/highlights.scm
@@ -0,0 +1,217 @@
+(open
+  namespace: (identifier) @namespace)
+(namespace
+  name: (identifier) @namespace)
+(section
+  name: (identifier) @namespace)
+
+;; Identifier naming conventions
+((identifier) @type
+ (#match? @type "^[A-Z]"))
+
+(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)
+
+(proj
+  name: (identifier) @field)
+
+(binders
+  type: (identifier) @type)
+
+["if" "then" "else"] @keyword.control.conditional
+
+["for" "in" "do"] @keyword.control.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_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) @constant.numeric.integer
+(float) @constant.numeric.float
+
+(comment) @comment
+(char) @character
+(string) @string
+(interpolated_string) @string
+; (escape_sequence) @string.escape
+
+; Reset highlighing in string interpolation
+(interpolation) @none
+
+(interpolation
+  "{" @punctuation.special
+  "}" @punctuation.special)
+
+["(" ")" "[" "]" "{" "}" "⟨" "⟩"] @punctuation.bracket
+
+["|" "," "." ":" ";"] @punctuation.delimiter
+
+(sorry) @error
+
+;; Error
+(ERROR) @error
+
+; Variables
+(identifier) @variable
diff --git a/runtime/queries/lean/injections.scm b/runtime/queries/lean/injections.scm
new file mode 100644
index 000000000000..030714f1ce17
--- /dev/null
+++ b/runtime/queries/lean/injections.scm
@@ -0,0 +1,2 @@
+((comment) @injection.content
+ (#set! injection.language "markdown"))
diff --git a/runtime/queries/lean/locals.scm b/runtime/queries/lean/locals.scm
new file mode 100644
index 000000000000..dd6c203631bf
--- /dev/null
+++ b/runtime/queries/lean/locals.scm
@@ -0,0 +1,5 @@
+[
+  (module)
+  (namespace)
+  (section)
+] @local.scope