diff --git a/plugins/by-name/lean/default.nix b/plugins/by-name/lean/default.nix
index f35dae62..a2517903 100644
--- a/plugins/by-name/lean/default.nix
+++ b/plugins/by-name/lean/default.nix
@@ -3,8 +3,7 @@
   ...
 }:
 let
-  inherit (lib.nixvim) defaultNullOpts mkNullOrOption;
-  inherit (lib) types;
+  inherit (lib.nixvim) defaultNullOpts;
 in
 lib.nixvim.plugins.mkNeovimPlugin {
   name = "lean";
@@ -24,132 +23,7 @@ lib.nixvim.plugins.mkNeovimPlugin {
   ];
 
   settingsOptions = {
-    lsp = defaultNullOpts.mkNullable (types.submodule {
-      freeformType = types.attrsOf types.anything;
-      options = {
-        enable = defaultNullOpts.mkBool true ''
-          Whether to enable the Lean language server(s).
-
-          Set to `false` to disable, otherwise should be a table of options to pass to
-          `leanls`.
-
-          See https://github.com/neovim/nvim-lspconfig/blob/master/doc/server_configurations.md#leanls
-          for details.
-        '';
-
-        on_attach = mkNullOrOption types.str ''
-          The LSP handler.
-        '';
-
-        init_options = mkNullOrOption (with types; attrsOf anything) ''
-          The options to configure the lean language server.
-
-          See `Lean.Lsp.InitializationOptions` for details.
-        '';
-      };
-    }) { } "LSP settings.";
-    ft = {
-      default = defaultNullOpts.mkStr "lean" ''
-        The default filetype for Lean files.
-      '';
-      nomodifiable = mkNullOrOption (types.listOf types.str) ''
-        A list of patterns which will be used to protect any matching Lean file paths from being
-        accidentally modified (by marking the buffer as `nomodifiable`).
-
-        By default, this list includes the Lean standard libraries, as well as files within
-        dependency directories (e.g. `_target`)
-
-        Set this to an empty table to disable.
-      '';
-    };
-    abbreviations = {
-      enable = defaultNullOpts.mkBool true ''
-        Whether to enable expanding of unicode abbreviations.
-      '';
-      extra = defaultNullOpts.mkAttrsOf' {
-        type = types.str;
-        pluginDefault = { };
-        description = ''
-          Additional abbreviations.
-        '';
-        example = lib.literalExpression ''
-          ```nix
-          {
-            # Add a \wknight abbreviation to insert ♘
-            #
-            # Note that the backslash is implied, and that you of
-            # course may also use a snippet engine directly to do
-            # this if so desired.
-            wknight = "♘";
-          }
-        '';
-      };
-      leader = defaultNullOpts.mkStr "\\" ''
-        Change if you don't like the backslash.
-      '';
-    };
-    mappings = defaultNullOpts.mkBool false ''
-      Whether to enable suggested mappings.
-    '';
-    infoview = {
-      autoopen = defaultNullOpts.mkBool true ''
-        Automatically open an infoview on entering a Lean buffer.
-
-        Should be a function that will be called anytime a new Lean file is opened.
-        Return true to open an infoview, otherwise false.
-        Setting this to `true` is the same as `function() return true end`, i.e. autoopen for any
-        Lean file, or setting it to `false` is the same as `function() return false end`,
-        i.e. never autoopen.
-      '';
-      autopause = defaultNullOpts.mkBool false "Set whether a new pin is automatically paused.";
-      width = defaultNullOpts.mkPositiveInt 50 ''
-        Set infoview windows' starting width.
-      '';
-      height = defaultNullOpts.mkPositiveInt 20 ''
-        Set infoview windows' starting height.
-      '';
-      horizontal_position = defaultNullOpts.mkEnumFirstDefault [ "bottom" "top" ] ''
-        Put the infoview on the top or bottom when horizontal.
-      '';
-      separate_tab = defaultNullOpts.mkBool false ''
-        Always open the infoview window in a separate tabpage.
-        Might be useful if you are using a screen reader and don't want too many dynamic updates
-        in the terminal at the same time.
-
-        Note that `height` and `width` will be ignored in this case.
-      '';
-      indicators = defaultNullOpts.mkEnumFirstDefault [ "auto" "always" "never" ] ''
-        Show indicators for pin locations when entering an infoview window.
-      '';
-      show_processing = defaultNullOpts.mkBool true "";
-      show_no_info_message = defaultNullOpts.mkBool false "";
-      use_widgets = defaultNullOpts.mkBool true "Whether to use widgets.";
-      mappings = defaultNullOpts.mkAttrsOf types.str {
-        K = "click";
-        "<CR>" = "click";
-        gd = "go_to_def";
-        gD = "go_to_decl";
-        gy = "go_to_type";
-        I = "mouse_enter";
-        i = "mouse_leave";
-        "<Esc>" = "clear_all";
-        C = "clear_all";
-        "<LocalLeader><Tab>" = "goto_last_window";
-      } "Mappings.";
-    };
-    progress_bars = {
-      enable = defaultNullOpts.mkBool true ''
-        Whether to enable the progress bars.
-      '';
-      priority = defaultNullOpts.mkUnsignedInt 10 ''
-        Use a different priority for the signs.
-      '';
-    };
     stderr = {
-      enable = defaultNullOpts.mkBool true ''
-        Redirect Lean's stderr messages somewhere (to a buffer by default).
-      '';
-      height = defaultNullOpts.mkPositiveInt 5 "Height of the window.";
       on_lines = defaultNullOpts.mkLuaFn "nil" ''
         A callback which will be called with (multi-line) stderr output.
       '';