diff --git a/src/emacs/lean-flycheck.el b/src/emacs/lean-flycheck.el
index 61f89639c3..4015202087 100644
--- a/src/emacs/lean-flycheck.el
+++ b/src/emacs/lean-flycheck.el
@@ -46,27 +46,8 @@
   (add-to-list 'flycheck-checkers 'lean-checker))
 
 (defun lean-flycheck-turn-on ()
-  (interactive)
-  (unless lean-flycheck-use
-    (when (called-interactively-p 'any)
-      (message "use flycheck in lean-mode"))
-    (setq lean-flycheck-use t))
   (flycheck-mode t))
 
-(defun lean-flycheck-turn-off ()
-  (interactive)
-  (when lean-flycheck-use
-    (when (called-interactively-p 'any)
-      (message "no flycheck in lean-mode")))
-  (flycheck-mode 0)
-  (setq lean-flycheck-use nil))
-
-(defun lean-flycheck-toggle-use ()
-  (interactive)
-  (if lean-flycheck-use
-      (lean-flycheck-turn-off)
-    (lean-flycheck-turn-on)))
-
 (defun lean-flycheck-error-list-buffer-width ()
   "Return the width of flycheck-error list buffer"
   (interactive)
diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el
index 3995e87af5..df97f3697c 100644
--- a/src/emacs/lean-mode.el
+++ b/src/emacs/lean-mode.el
@@ -19,6 +19,7 @@
 (require 'pcase)
 (require 'lean-require)
 (require 'eri)
+(require 'flycheck)
 (require 'lean-util)
 (require 'lean-settings)
 (require 'lean-input)
@@ -110,7 +111,7 @@
     ["Toggle next error display" lean-toggle-next-error       t]
     ["Find definition at point" lean-find-definition          t]
     "-----------------"
-    ["List of errors"       flycheck-list-errors              (and lean-flycheck-use flycheck-mode)]
+    ["List of errors"       flycheck-list-errors              flycheck-mode]
     "-----------------"
     ["Restart lean process" lean-server-restart               t]
     "-----------------"
@@ -147,9 +148,8 @@ enabled and disabled respectively.")
   (lean-server-ensure-alive)
   (setq mode-name '("Lean" (:eval (lean-server-status-string))))
   ;; Flycheck
-  (when lean-flycheck-use
-    (lean-flycheck-turn-on)
-    (setq-local flycheck-disabled-checkers '()))
+  (lean-flycheck-turn-on)
+  (setq-local flycheck-disabled-checkers '())
   ;; company-mode
   (when lean-company-use
     (company-lean-hook))
@@ -200,10 +200,8 @@ Invokes `lean-mode-hook'.
 (modify-coding-system-alist 'file "\\.hlean\\'" 'utf-8)
 
 ;; Flycheck init
-(when lean-flycheck-use
-  (require 'flycheck)
-  (eval-after-load 'flycheck
-    '(lean-flycheck-init)))
+(eval-after-load 'flycheck
+  '(lean-flycheck-init))
 
 (provide 'lean-mode)
 ;;; lean-mode.el ends here
diff --git a/src/emacs/lean-server.el b/src/emacs/lean-server.el
index fdc5a0f79e..33d9ce558f 100644
--- a/src/emacs/lean-server.el
+++ b/src/emacs/lean-server.el
@@ -223,9 +223,8 @@
 
 (defun lean-server-show-messages (&optional buf)
   (with-current-buffer (or buf (current-buffer))
-    (when flycheck-mode
-      (lean-server-update-task-overlays)
-      (flycheck-buffer))))
+    (lean-server-update-task-overlays)
+    (flycheck-buffer)))
 
 (defun lean-server-notify-messages-changed (sess)
   (dolist (buf (buffer-list))
@@ -263,9 +262,8 @@
   (interactive)
   (lean-server-stop)
   (lean-server-ensure-alive)
-  (when lean-flycheck-use
-    (flycheck-stop)
-    (flycheck-buffer)))
+  (flycheck-stop)
+  (flycheck-buffer))
 
 (defun lean-server-send-command (cmd params &optional cb error-cb)
   "Sends a command to the lean server for the current buffer, with a callback to be called upon completion"
diff --git a/src/emacs/lean-settings.el b/src/emacs/lean-settings.el
index fd982d0c2e..7049477151 100644
--- a/src/emacs/lean-settings.el
+++ b/src/emacs/lean-settings.el
@@ -59,11 +59,6 @@
   :group 'lean
   :type 'number)
 
-(defcustom lean-flycheck-use t
-  "Use flycheck for lean."
-  :group 'lean
-  :type 'boolean)
-
 (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