diff --git a/book/src/generated/lang-support.md b/book/src/generated/lang-support.md
index ba2bee71..9c478cc0 100644
--- a/book/src/generated/lang-support.md
+++ b/book/src/generated/lang-support.md
@@ -186,6 +186,7 @@
 | matlab | ✓ | ✓ | ✓ |  |  |  |
 | mermaid | ✓ |  |  |  |  |  |
 | meson | ✓ |  | ✓ |  |  | `mesonlsp` |
+| metamath | ✓ |  |  | ✓ |  | `mm-lsp-server` |
 | mint |  |  |  |  |  | `mint` |
 | miseconfig | ✓ | ✓ | ✓ |  |  | `taplo`, `tombi` |
 | mojo | ✓ | ✓ | ✓ |  |  | `pixi` |
diff --git a/languages.toml b/languages.toml
index c7225c59..d8b54f33 100644
--- a/languages.toml
+++ b/languages.toml
@@ -91,6 +91,8 @@ metals = { command = "metals", config = { "isHttpEnabled" = true, metals = { inl
 mesonlsp = { command = "mesonlsp", args = ["--lsp"] }
 mint = { command = "mint", args = ["tool", "ls"] }
 mojo-lsp-server = { command = "pixi", args = ["run", "mojo-lsp-server"] }
+mm0-rs = { command = "mm0-rs", args = [ "server" ] }
+mm-lsp-server = { command = "mm-lsp-server" }
 neocmakelsp = { command = "neocmakelsp", args = ["stdio"] }
 nginx-language-server = { command = "nginx-language-server" }
 nil = { command = "nil" }
@@ -172,6 +174,7 @@ vuels = { command = "vue-language-server", args = ["--stdio"], config = { typesc
 wgsl-analyzer = { command = "wgsl-analyzer" }
 wikitext-lsp = { command = "wikitext-lsp", args = ["--stdio"]}
 yaml-language-server = { command = "yaml-language-server", args = ["--stdio"] }
+yamma-server = { command = "yamma-server" }
 yls = { command = "yls", args = ["-vv"] }
 zls = { command = "zls" }
 zuban = { command = "zuban", args = ["server"] }
@@ -5608,3 +5611,27 @@ language-servers = ["varlink-language-server"]
 [[grammar]]
 name = "varlink"
 source = { git = "https://github.com/bachorp/tree-sitter-varlink", rev = "a80ecffda60b28612cbda652e38d97c1d8b90568" }
+
+[[language]]
+name = "metamath"
+scope = "source.metamath"
+file-types = [ "mm" ]
+injection-regex = "mm|metamath"
+roots = [ "set.mm" ]
+block-comment-tokens = { start = "$(", end = "$)" }
+indent = { tab-width = 2, unit = "  " }
+text-width = 80
+language-servers = [ "mm-lsp-server" ]
+
+[language.auto-pairs]
+"$" = "$"
+"(" = ")"
+"[" = "]"
+"{" = "}"
+"<" = ">"
+'"' = '"'
+"`" = "`"
+
+[[grammar]]
+name = "metamath"
+source = { git = "https://git.sr.ht/~m4dh0rs3/tree-sitter-metamath", rev = "d6a57b0ddb4feba4a88f8cbb2f497b718e0c5c1d" }
diff --git a/runtime/queries/metamath/highlights.scm b/runtime/queries/metamath/highlights.scm
new file mode 100644
index 00000000..c3be8b84
--- /dev/null
+++ b/runtime/queries/metamath/highlights.scm
@@ -0,0 +1,45 @@
+; Keywords and delimiters
+[ "$c" "$v" "$d" "$f" "$e" "$a" "$p" "$=" ] @keyword
+[ "${" "$}" ] @punctuation.bracket
+[ "$[" "$]" ] @keyword.import
+"$." @punctuation.delimiter
+
+; Markup (update grammar.js to support)
+; "####" @markup.heading.1
+; "#*#*" @markup.heading.2
+; "=-=-" @markup.heading.3
+; "-.-." @markup.heading.4
+
+; Builtin typecodes
+[ "|-" "wff" "setvar" "class" ] @type.builtin
+
+; Labels
+(floating_stmt (label) @function)
+(essential_stmt (label) @function)
+(axiom_stmt (label) @function)
+(provable_stmt (label) @function)
+
+; Types
+(typecode) @type
+
+; Variables and constants in declarations
+(constant_stmt (constant) @constant)
+(variable_stmt (variable) @variable)
+
+; Math symbols
+(mathsymbol) @variable
+
+; Proofs
+(uncompressed_proof (label) @function)
+(compressed_proof (label) @function)
+(compressed_proof_block) @string
+
+; Comments
+(comment) @comment.block
+
+; Parentheses in math expressions
+"(" @punctuation.bracket
+")" @punctuation.bracket
+
+; File includes
+(filename) @string.special.path
diff --git a/runtime/queries/metamath/locals.scm b/runtime/queries/metamath/locals.scm
new file mode 100644
index 00000000..8bc72333
--- /dev/null
+++ b/runtime/queries/metamath/locals.scm
@@ -0,0 +1,26 @@
+; Scopes
+(block) @local.scope
+(database) @local.scope
+
+; Definitions
+(floating_stmt
+  (label) @local.definition.variable)
+
+(essential_stmt
+  (label) @local.definition.variable)
+
+(axiom_stmt
+  (label) @local.definition.function)
+
+(provable_stmt
+  (label) @local.definition.function)
+
+(variable_stmt
+  (variable) @local.definition.variable)
+
+(constant_stmt
+  (constant) @local.definition.constant)
+
+; References in proofs
+(uncompressed_proof
+  (label) @local.reference)
diff --git a/runtime/queries/metamath/tags.scm b/runtime/queries/metamath/tags.scm
new file mode 100644
index 00000000..6c2edc68
--- /dev/null
+++ b/runtime/queries/metamath/tags.scm
@@ -0,0 +1,19 @@
+; Axioms
+(axiom_stmt
+  (label) @name) @definition.function
+
+; Provable theorems
+(provable_stmt
+  (label) @name) @definition.function
+
+; Floating hypotheses
+(floating_stmt
+  (label) @name) @definition.variable
+
+; Essential hypotheses
+(essential_stmt
+  (label) @name) @definition.variable
+
+; References in proofs
+(uncompressed_proof
+  (label) @name) @reference.call