diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json
index e66d94478..368e93181 100644
--- a/vscode-lean4/package.json
+++ b/vscode-lean4/package.json
@@ -380,10 +380,10 @@
 				"configuration": "./language-configuration.json"
 			},
 			{
-				"id": "leanmarkdown",
+				"id": "lean4markdown",
 				"aliases": [],
 				"extensions": [
-					".leanmarkdown"
+					".lean4markdown"
 				],
 				"configuration": "./language-configuration.json"
 			}
@@ -395,9 +395,9 @@
 				"path": "./syntaxes/lean4.json"
 			},
 			{
-				"language": "leanmarkdown",
-				"scopeName": "source.lean.markdown",
-				"path": "./syntaxes/lean-markdown.json"
+				"language": "lean4markdown",
+				"scopeName": "source.lean4.markdown",
+				"path": "./syntaxes/lean4-markdown.json"
 			},
 			{
 				"scopeName": "markdown.lean4.codeblock",
diff --git a/vscode-lean4/syntaxes/lean-markdown.json b/vscode-lean4/syntaxes/lean4-markdown.json
similarity index 99%
rename from vscode-lean4/syntaxes/lean-markdown.json
rename to vscode-lean4/syntaxes/lean4-markdown.json
index b06bd7f93..691d98f76 100644
--- a/vscode-lean4/syntaxes/lean-markdown.json
+++ b/vscode-lean4/syntaxes/lean4-markdown.json
@@ -5,7 +5,7 @@
 	],
 	"version": "https://github.com/microsoft/vscode/blob/df3ae4adefbb780f5f686e58ac6a8d305a8c86dc/extensions/markdown-basics/syntaxes/markdown.tmLanguage.json",
 	"name": "Markdown",
-	"scopeName": "source.lean.markdown",
+	"scopeName": "source.lean4.markdown",
 	"patterns": [
 		{
 			"include": "#frontMatter"
diff --git a/vscode-lean4/syntaxes/lean4.json b/vscode-lean4/syntaxes/lean4.json
index 9db919821..cff18ecb3 100644
--- a/vscode-lean4/syntaxes/lean4.json
+++ b/vscode-lean4/syntaxes/lean4.json
@@ -62,27 +62,27 @@
       "begin": "--", "end": "$",
       "name": "comment.line.double-dash.lean4",
       "patterns": [
-        { "include": "source.lean.markdown" }
+        { "include": "source.lean4.markdown" }
       ]
     },
     "docComment": {
       "begin": "/--", "end": "-/", "name": "comment.block.documentation.lean4",
       "patterns": [
-        { "include": "source.lean.markdown" },
+        { "include": "source.lean4.markdown" },
         { "include": "#blockComment" }
       ]
     },
     "modDocComment": {
       "begin": "/-!", "end": "-/", "name": "comment.block.documentation.lean4",
       "patterns": [
-        { "include": "source.lean.markdown" },
+        { "include": "source.lean4.markdown" },
         { "include": "#blockComment" }
       ]
     },
     "blockComment": {
       "begin": "/-", "end": "-/", "name": "comment.block.lean4",
       "patterns": [
-        { "include": "source.lean.markdown" },
+        { "include": "source.lean4.markdown" },
         { "include": "#blockComment" }
       ]
     },