chore: add extensions.json to prevent pop-up about unnecessary extension

user_repo_source/.vscode/extensions.json

@@ -0,0 +1,15 @@
+// This file prevents VS Code from making unhelpful suggestions about extensions
+// during the initial setup of Mathematics In Lean.
+{
+	// See https://go.microsoft.com/fwlink/?LinkId=827846 to learn about workspace recommendations.
+	// Extension identifier format: ${publisher}.${name}. Example: vscode.csharp
+
+	// List of extensions which should be recommended for users of this workspace.
+	"recommendations": [
+		"leanprover.lean4"
+	],
+	// List of extensions recommended by VS Code that should not be recommended for users of this workspace.
+	"unwantedRecommendations": [
+		"ms-vscode-remote.remote-containers"
+	]
+}