diff --git a/Projects/MathlibDemo/leanweb-config.json b/Projects/MathlibDemo/leanweb-config.json
index 95b3e57b..69683955 100644
--- a/Projects/MathlibDemo/leanweb-config.json
+++ b/Projects/MathlibDemo/leanweb-config.json
@@ -1,5 +1,5 @@
 {
-  "name": "Latest Mathlib",
+  "name": "_LeanVers_ with Mathlib",
   "default": true,
   "hidden": false,
   "examples": [
diff --git a/Projects/Stable/lean-toolchain b/Projects/Stable/lean-toolchain
index 7638861c..14791d72 100644
--- a/Projects/Stable/lean-toolchain
+++ b/Projects/Stable/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:stable
+leanprover/lean4:v4.29.0
diff --git a/Projects/Stable/leanweb-config.json b/Projects/Stable/leanweb-config.json
index 167b9282..fc3e4cd2 100644
--- a/Projects/Stable/leanweb-config.json
+++ b/Projects/Stable/leanweb-config.json
@@ -1,4 +1,4 @@
 {
-  "name": "Stable Lean",
+  "name": "_LeanVers_",
   "hidden": false
 }
diff --git a/client/src/api/project-types.ts b/client/src/api/project-types.ts
index d5362b55..c66d7ed7 100644
--- a/client/src/api/project-types.ts
+++ b/client/src/api/project-types.ts
@@ -16,6 +16,8 @@ export type LeanWebProjectConfig = {
   hidden: boolean
   /** The default project. There must be exactly one project marked as default */
   default: boolean
+  /** Sort order: the default project always comes first, followed by projects in decreasing sort order. (No sort order is treated as 0.)  */
+  sortOrder: number
   /** A list of examples which are added under the menu `Examples` */
   examples: LeanWebExample[]
 }
diff --git a/client/src/store/project-atoms.ts b/client/src/store/project-atoms.ts
index 4a4385c1..5063895a 100644
--- a/client/src/store/project-atoms.ts
+++ b/client/src/store/project-atoms.ts
@@ -12,10 +12,19 @@ const projectsQueryAtom = atomWithQuery<LeanWebProject[]>(() => ({
   },
 }))
 
-/** Sort alphabetically while the `default` project always comes first */
+/**
+ * Sort alphabetically while the `default` project always comes first, then
+ * order by descending sortOrder (nullish treated as 0), then order by name.
+ */
 function sortProjects(p: LeanWebProject, q: LeanWebProject): number {
   if (p.config.default) return -1
   if (q.config.default) return 1
+
+  // Secondary sort: sortOrder field
+  const n = q.config.sortOrder - p.config.sortOrder
+  if (n !== 0) return n
+
+  // Fallback: names
   return p.config.name.localeCompare(q.config.name)
 }
 
diff --git a/cypress/e2e/encoding.cy.ts b/cypress/e2e/encoding.cy.ts
index 05456080..e4c97492 100644
--- a/cypress/e2e/encoding.cy.ts
+++ b/cypress/e2e/encoding.cy.ts
@@ -15,7 +15,7 @@ describe("", () => {
     cy.get("div.view-lines").type(payload);
 
     // change project
-    cy.get("nav>*>select[name='leanVersion']").select("Stable Lean");
+    cy.get("nav>*>select[name='leanVersion']").select("Stable");
     cy.url().should("include", "project=Stable");
 
     cy.contains("div.view-line", payload).should("exist");
diff --git a/cypress/e2e/settings.cy.ts b/cypress/e2e/settings.cy.ts
index 282b38ac..aa2cfcb5 100644
--- a/cypress/e2e/settings.cy.ts
+++ b/cypress/e2e/settings.cy.ts
@@ -56,3 +56,19 @@ describe("The Settings can be changed for", () => {
       });
   });
 });
+
+describe("The version selection menu", () => {
+  it("displays a versioned name for the MathlibDemo project", () => {
+    cy.visit("/");
+    cy.get("nav>*>select[name='leanVersion'] option[value='MathlibDemo']")
+      .invoke("text")
+      .should("match", /^Lean v4\.[0-9]+\.[0-9]+(-rc[0-9]+)? with Mathlib/);
+  });
+
+  it("displays a versioned name for the Stable project", () => {
+    cy.visit("/");
+    cy.get("nav>*>select[name='leanVersion'] option[value='Stable']")
+      .invoke("text")
+      .should("match", /^Lean v4\./);
+  });
+});
diff --git a/cypress/e2e/spec.cy.ts b/cypress/e2e/spec.cy.ts
index c95eb75d..75283922 100644
--- a/cypress/e2e/spec.cy.ts
+++ b/cypress/e2e/spec.cy.ts
@@ -18,7 +18,11 @@ describe("The Editor", () => {
     cy.iframe().contains("Stable.lean").should("exist");
     cy.get(".dropdown>.nav-link>.fa-bars").click();
     cy.contains(".nav-link", "Lean Info").click();
-    cy.containsAll(".modal", ["leanprover/lean4:stable", "(no dependencies)"])
+    cy.containsAll(".modal", [
+      "Stable",
+      "leanprover/lean4:",
+      "(no dependencies)",
+    ])
       .find(".modal-close")
       .click();
   });
diff --git a/doc/Projects.md b/doc/Projects.md
index 7d72ea1c..56ec1a59 100644
--- a/doc/Projects.md
+++ b/doc/Projects.md
@@ -40,6 +40,7 @@ The file `leanweb-config.json` takes the following form:
   "name": "Display name",
   "default": false,
   "hidden": false,
+  "sortOrder": 0,
   "examples": [
     { "file": "MathlibDemo/Bijection.lean", "name": "Example's display name" },
     ...
@@ -47,12 +48,22 @@ The file `leanweb-config.json` takes the following form:
 }
 ```
 
-- `name`: The display name of the project as shown in the dropdown menu
+- `name`: The display name of the project as shown in the dropdown menu. The substrings `_Vers_` and
+  `_LeanVers_` in the project name will be replaced by indicators of which version is being used:
+  - If the toolchain is in a recognized format (a regular release like `v4.30.0-rc1` or nightly
+    release like `2026-04-04`), then `_Vers_` will be replaced by the version number (e.g.
+    `v4.30.0-rc1`) and `_LeanVers_` will be replaced by "Lean" followed by the version number (e.g.
+    `Lean v4.30.0-rc1`)
+  - If the toolchain is not in a recognized format, both `_Vers_` and `_LeanVers_` will be replaced
+    by "Lean".
 - `default`: There must be exactly one project with this set to `true`. This is the project loaded
   by default and when no project is specified in the url.
 - `hidden`: If set to `true`, then the project does not appear in the dropdown and can
   only be accessed via direct link.
-- `examples`: list of examples. The path is relativ to the project's directory, e.g. `{PROJECTS_BASE_PATH}/{PROJECT_FOLDER}/{EXAMPLE_PATH.lean}`
+- `sortOrder`(non-negative number): sort order of the projects in the dropdown. The default always
+  comes first, then projects with higher `sortOrder` value. Ties are resolved alphabetically.
+- `examples`: list of examples. The path is relativ to the project's directory, e.g. 
+  `{PROJECTS_BASE_PATH}/{PROJECT_FOLDER}/{EXAMPLE_PATH.lean}`
 
 ## automatic builds
 
diff --git a/package-lock.json b/package-lock.json
index dab2fb78..57c760b1 100644
--- a/package-lock.json
+++ b/package-lock.json
@@ -12868,9 +12868,9 @@
       }
     },
     "node_modules/zod": {
-      "version": "4.3.6",
-      "resolved": "https://registry.npmjs.org/zod/-/zod-4.3.6.tgz",
-      "integrity": "sha512-rftlrkhHZOcjDwkGlnUtZZkvaPHCsDATp4pGpuOOMDaTdDDXF91wuVDJoWoPsKX/3YPQ5fHuF3STjcYyKr+Qhg==",
+      "version": "4.4.3",
+      "resolved": "https://registry.npmjs.org/zod/-/zod-4.4.3.tgz",
+      "integrity": "sha512-ytENFjIJFl2UwYglde2jchW2Hwm4GJFLDiSXWdTrJQBIN9Fcyp7n4DhxJEiWNAJMV1/BqWfW/kkg71UDcHJyTQ==",
       "license": "MIT",
       "funding": {
         "url": "https://github.com/sponsors/colinhacks"
@@ -12896,7 +12896,8 @@
         "ip-anonymize": "^0.1.0",
         "memfs": "^4.51.1",
         "nocache": "^4.0.0",
-        "ws": "^8.18.3"
+        "ws": "^8.18.3",
+        "zod": "^4.4.3"
       },
       "bin": {
         "server": "index.mjs"
diff --git a/server/index.mjs b/server/index.mjs
index b0f63c8d..d36bf266 100755
--- a/server/index.mjs
+++ b/server/index.mjs
@@ -12,6 +12,8 @@ import * as rpc from "vscode-ws-jsonrpc";
 import * as jsonrpcserver from "vscode-ws-jsonrpc/server";
 import { WebSocketServer } from "ws";
 
+import { zLeanWebProjectConfig } from "./types.mjs";
+
 let socketCounter = 0;
 
 function logStats() {
@@ -59,11 +61,24 @@ app.use("/api/projects", async (req, res) => {
 
       const projectDir = path.join(PROJECTS_BASE_PATH, entry.name);
       const configPath = path.join(projectDir, "leanweb-config.json");
+      const toolchainPath = path.join(projectDir, "lean-toolchain");
 
       let config = null;
       try {
         const raw = await fs.promises.readFile(configPath, "utf-8");
-        config = JSON.parse(raw);
+        const toolchain = (
+          await fs.promises.readFile(toolchainPath, "utf-8")
+        ).trim();
+
+        config = zLeanWebProjectConfig.parse(JSON.parse(raw));
+        config.name = config.name.replaceAll(
+          "_LeanVers_",
+          toolchainToName(toolchain, true),
+        );
+        config.name = config.name.replaceAll(
+          "_Vers_",
+          toolchainToName(toolchain, false),
+        );
       } catch (err) {
         console.debug(err);
         // File missing or invalid JSON — keep config as null
@@ -73,10 +88,11 @@ app.use("/api/projects", async (req, res) => {
         projects.push({
           folder: entry.name,
           config: {
-            name: String(config.name), // TODO: ensure this is not null
-            hidden: Boolean(config.hidden) ?? false,
-            default: Boolean(config.default) ?? false,
-            examples: config.examples ?? [], // TODO: validate
+            name: config.name,
+            hidden: config.hidden ?? false,
+            default: config.default ?? false,
+            examples: config.examples ?? [],
+            sortOrder: config.sortOrder ?? 0,
           },
         });
       }
@@ -455,3 +471,11 @@ function hasWorkingBwrap() {
   const test = cp.spawnSync("bwrap", ["--version"], { stdio: "ignore" });
   return test.status === 0;
 }
+
+function toolchainToName(toolchain, prefixLean) {
+  const nightly = toolchain.match(/^leanprover\/lean4\:nightly-(.*)$/);
+  if (nightly) return prefixLean ? `Lean ${nightly[1]}` : nightly[1];
+  const release = toolchain.match(/^leanprover\/lean4\:(.*)$/);
+  if (release) return prefixLean ? `Lean ${release[1]}` : release[1];
+  return "Lean";
+}
diff --git a/server/package.json b/server/package.json
index 480d71e4..56b8f836 100644
--- a/server/package.json
+++ b/server/package.json
@@ -15,7 +15,8 @@
     "ip-anonymize": "^0.1.0",
     "memfs": "^4.51.1",
     "nocache": "^4.0.0",
-    "ws": "^8.18.3"
+    "ws": "^8.18.3",
+    "zod": "^4.4.3"
   },
   "devDependencies": {
     "@types/node": "^24.10.1",
diff --git a/server/types.mjs b/server/types.mjs
new file mode 100644
index 00000000..e889a9fe
--- /dev/null
+++ b/server/types.mjs
@@ -0,0 +1,14 @@
+import { z } from "zod";
+
+export const zLeanWebExample = z.object({
+  file: z.string(),
+  name: z.string(),
+});
+
+export const zLeanWebProjectConfig = z.object({
+  name: z.string(),
+  hidden: z.boolean().optional(),
+  default: z.boolean().optional(),
+  sortOrder: z.number().min(0).optional(),
+  examples: z.array(zLeanWebExample).optional(),
+});