diff --git a/src/emacs/lean-flycheck.el b/src/emacs/lean-flycheck.el
index 430456eb83..61f89639c3 100644
--- a/src/emacs/lean-flycheck.el
+++ b/src/emacs/lean-flycheck.el
@@ -77,9 +77,6 @@
      ;; If "*Flycheck errors" buffer is available, use its width
      (flycheck-error-window
       (window-body-width flycheck-error-window))
-     ;; If lean-flycheck-msg-width is set, use it
-     (lean-flycheck-msg-width
-      lean-flycheck-msg-width)
      ;; Can we split vertically?
      ((window-splittable-p window nil)
       body-width)
diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el
index ffa52b5223..3995e87af5 100644
--- a/src/emacs/lean-mode.el
+++ b/src/emacs/lean-mode.el
@@ -93,9 +93,6 @@
   (local-set-key lean-keybinding-lean-toggle-next-error    'lean-toggle-next-error)
   )
 
-(defun lean-define-key-binding (key cmd)
-  (local-set-key key `(lambda () (interactive) ,cmd)))
-
 (define-abbrev-table 'lean-abbrev-table
   '())
 
@@ -113,7 +110,6 @@
     ["Toggle next error display" lean-toggle-next-error       t]
     ["Find definition at point" lean-find-definition          t]
     "-----------------"
-    ["Run flycheck"         flycheck-compile                  (and lean-flycheck-use flycheck-mode)]
     ["List of errors"       flycheck-list-errors              (and lean-flycheck-use flycheck-mode)]
     "-----------------"
     ["Restart lean process" lean-server-restart               t]
diff --git a/src/emacs/lean-settings.el b/src/emacs/lean-settings.el
index d7e3578f9a..fd982d0c2e 100644
--- a/src/emacs/lean-settings.el
+++ b/src/emacs/lean-settings.el
@@ -64,23 +64,6 @@
   :group 'lean
   :type 'boolean)
 
-(defcustom lean-flycheck-max-messages-to-display 100
-  "Maximum number of flycheck messages to displaylean-flychecker checker name
-   (Restart required to be effective)"
-  :group 'lean
-  :type 'number)
-
-(defcustom lean-default-pp-width 120
-  "Width of Lean error/warning messages"
-  :group 'lean
-  :type 'number)
-
-(defcustom lean-flycheck-msg-width nil
-  "Width of Lean error/warning messages"
-  :group 'lean
-  :type '(choice (const   :tag "Let lean-mode automatically detect this" nil)
-                 (integer :tag "Specify the value and force lean-mode to use")))
-
 (defcustom lean-delete-trailing-whitespace nil
   "Set this variable to true to automatically delete trailing
 whitespace when a buffer is loaded from a file or when it is
@@ -88,12 +71,6 @@ written."
   :group 'lean
   :type 'boolean)
 
-(defcustom lean-debug-mode-line '(:eval (lean-debug-mode-line-status-text))
-  "Mode line lighter for Lean debug mode."
-  :group 'lean
-  :type 'sexp
-  :risky t)
-
 (defcustom lean-show-type-add-to-kill-ring nil
   "If it is non-nil, add the type information to the kill-ring so
 that user can yank(paste) it later. By default, it's
@@ -101,13 +78,6 @@ false (nil)."
   :group 'lean
   :type 'boolean)
 
-(defcustom lean-proofstate-display-style 'show-first-and-other-conclusions
-  "Choose how to display proof state in *lean-info* buffer."
-  :group 'lean
-  :type '(choice (const :tag "Show all goals" show-all)
-                 (const :tag "Show only the first" show-first)
-                 (const :tag "Show the first goal, and the conclusions of all other goals" show-first-and-other-conclusions)))
-
 (defcustom lean-keybinding-std-exe1 (kbd "C-c C-x")
   "Lean Keybinding for std-exe #1"
   :group 'lean-keybinding :type 'key-sequence)
@@ -117,12 +87,6 @@ false (nil)."
 (defcustom lean-keybinding-show-key (kbd "C-c C-k")
   "Lean Keybinding for show-key"
   :group 'lean-keybinding  :type 'key-sequence)
-(defcustom lean-keybinding-set-option (kbd "C-c C-o")
-  "Lean Keybinding for set-option"
-  :group 'lean-keybinding  :type 'key-sequence)
-(defcustom lean-keybinding-eval-cmd (kbd "C-c C-e")
-  "Lean Keybinding for eval-cmd"
-  :group 'lean-keybinding  :type 'key-sequence)
 (defcustom lean-keybinding-server-restart (kbd "C-c C-r")
   "Lean Keybinding for server-restart"
   :group 'lean-keybinding  :type 'key-sequence)