From 34b72d54940aa81d38ac4a0ec3d30d34580b2b0f Mon Sep 17 00:00:00 2001
From: remix7531 <131352678+remix7531@users.noreply.github.com>
Date: Wed, 15 Apr 2026 08:17:14 +0000
Subject: [PATCH 1/3] maintainers: add remix7531

---
 maintainers/maintainer-list.nix | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/maintainers/maintainer-list.nix b/maintainers/maintainer-list.nix
index 410e5fe28876..07ec3ecdfb61 100644
--- a/maintainers/maintainer-list.nix
+++ b/maintainers/maintainer-list.nix
@@ -22861,6 +22861,12 @@
     githubId = 4196789;
     name = "Nathan Ringo";
   };
+  remix7531 = {
+    email = "remix7531@mailbox.org";
+    github = "remix7531";
+    githubId = 131352678;
+    name = "remix7531";
+  };
   remko = {
     github = "remko";
     githubId = 12300;

From 6372d3a69b66eedf690e0868a9409bd9072bf4ba Mon Sep 17 00:00:00 2001
From: remix7531 <131352678+remix7531@users.noreply.github.com>
Date: Wed, 15 Apr 2026 08:17:34 +0000
Subject: [PATCH 2/3] python3Packages.leanclient: init at 0.9.4

---
 .../python-modules/leanclient/default.nix     | 46 +++++++++++++++++++
 pkgs/top-level/python-packages.nix            |  2 +
 2 files changed, 48 insertions(+)
 create mode 100644 pkgs/development/python-modules/leanclient/default.nix

diff --git a/pkgs/development/python-modules/leanclient/default.nix b/pkgs/development/python-modules/leanclient/default.nix
new file mode 100644
index 000000000000..8193c41d1585
--- /dev/null
+++ b/pkgs/development/python-modules/leanclient/default.nix
@@ -0,0 +1,46 @@
+{
+  lib,
+  buildPythonPackage,
+  fetchFromGitHub,
+
+  # build-system
+  hatchling,
+
+  # dependencies
+  orjson,
+  psutil,
+  tqdm,
+}:
+
+buildPythonPackage (finalAttrs: {
+  pname = "leanclient";
+  version = "0.9.4";
+  pyproject = true;
+
+  src = fetchFromGitHub {
+    owner = "oOo0oOo";
+    repo = "leanclient";
+    tag = "v${finalAttrs.version}";
+    hash = "sha256-BmIvjFhhlXnyDZWNUZAq41TA+Q5v9UW63rljoeYl44Q=";
+  };
+
+  build-system = [ hatchling ];
+
+  dependencies = [
+    orjson
+    psutil
+    tqdm
+  ];
+
+  # Tests require a real Lean toolchain
+  doCheck = false;
+
+  pythonImportsCheck = [ "leanclient" ];
+
+  meta = {
+    description = "Python client for the Lean theorem prover LSP";
+    homepage = "https://github.com/oOo0oOo/leanclient";
+    license = lib.licenses.mit;
+    maintainers = with lib.maintainers; [ remix7531 ];
+  };
+})
diff --git a/pkgs/top-level/python-packages.nix b/pkgs/top-level/python-packages.nix
index 46a8625b989f..09467bc2aa23 100644
--- a/pkgs/top-level/python-packages.nix
+++ b/pkgs/top-level/python-packages.nix
@@ -8585,6 +8585,8 @@ self: super: with self; {
 
   leanblueprint = callPackage ../development/python-modules/leanblueprint { };
 
+  leanclient = callPackage ../development/python-modules/leanclient { };
+
   leaone-ble = callPackage ../development/python-modules/leaone-ble { };
 
   leather = callPackage ../development/python-modules/leather { };

From c48719595fd5dbf9655f07f9f008042f2724405e Mon Sep 17 00:00:00 2001
From: remix7531 <131352678+remix7531@users.noreply.github.com>
Date: Wed, 15 Apr 2026 08:17:39 +0000
Subject: [PATCH 3/3] lean-lsp-mcp: init at 0.26.1

---
 pkgs/by-name/le/lean-lsp-mcp/package.nix | 47 ++++++++++++++++++++++++
 1 file changed, 47 insertions(+)
 create mode 100644 pkgs/by-name/le/lean-lsp-mcp/package.nix

diff --git a/pkgs/by-name/le/lean-lsp-mcp/package.nix b/pkgs/by-name/le/lean-lsp-mcp/package.nix
new file mode 100644
index 000000000000..c1d2d46c1cd9
--- /dev/null
+++ b/pkgs/by-name/le/lean-lsp-mcp/package.nix
@@ -0,0 +1,47 @@
+{
+  lib,
+  python3Packages,
+  fetchFromGitHub,
+}:
+
+python3Packages.buildPythonApplication (finalAttrs: {
+  pname = "lean-lsp-mcp";
+  version = "0.26.1";
+  pyproject = true;
+
+  __structuredAttrs = true;
+
+  src = fetchFromGitHub {
+    owner = "oOo0oOo";
+    repo = "lean-lsp-mcp";
+    tag = "v${finalAttrs.version}";
+    hash = "sha256-OHbD6HujkXsqe8XpNr1bn+Pel2tbkX7tBapCcUe234o=";
+  };
+
+  build-system = with python3Packages; [ setuptools ];
+
+  dependencies = with python3Packages; [
+    leanclient
+    mcp
+    orjson
+    certifi
+  ];
+
+  pythonRelaxDeps = [
+    "mcp"
+    "leanclient"
+  ];
+
+  # Tests require a real Lean toolchain
+  doCheck = false;
+
+  pythonImportsCheck = [ "lean_lsp_mcp" ];
+
+  meta = {
+    description = "MCP server for the Lean theorem prover via the Lean LSP";
+    homepage = "https://github.com/oOo0oOo/lean-lsp-mcp";
+    license = lib.licenses.mit;
+    maintainers = with lib.maintainers; [ remix7531 ];
+    mainProgram = "lean-lsp-mcp";
+  };
+})