diff --git a/src/emacs/lean-flycheck.el b/src/emacs/lean-flycheck.el
index 495d157b5..d81731929 100644
--- a/src/emacs/lean-flycheck.el
+++ b/src/emacs/lean-flycheck.el
@@ -4,29 +4,65 @@
 ;; Author: Soonho Kong
 ;;
 
-(when lean-use-flycheck
-  (require 'flycheck)
-  (setq-local lean-lmake-name "lmake")
-  (setq-local lean-lmake-options "--flycheck")
-  (eval
-   `(flycheck-define-checker lean-checker-file
-      "A Lean syntax checker (file)."
-      :command (,(lean-get-executable lean-lmake-name) ,lean-lmake-options source-inplace)
-      :error-patterns
-      ((error line-start "FLYCHECK_BEGIN ERROR\n"
-              (file-name) ":" line ":" column  ": error: "
-              (minimal-match
-               (message (one-or-more (one-or-more not-newline) "\n") ))
-              "FLYCHECK_END" line-end)
-       (warning line-start "FLYCHECK_BEGIN WARNING\n"
-                (file-name) ":" line ":" column  ": warning "
+(defvar-local lean-flycheck-initialized nil
+  "Return true if lean-flycheck has been initialized")
+(defvar-local lean-flycheck-lmake-name "lmake"
+  "lmake name")
+(defvar-local lean-flycheck-lmake-options "--flycheck"
+  "flycheck option for lean")
+
+(defun lean-flycheck-init ()
+  "Initialize lean-flychek checker"
+  (unless lean-flycheck-initialized
+    (require 'flycheck)
+    (eval
+     `(flycheck-define-checker lean-checker-file
+        "A Lean syntax checker (file)."
+        :command (,(lean-get-executable lean-flycheck-lmake-name)
+                  ,lean-flycheck-lmake-options
+                  source-inplace)
+        :error-patterns
+        ((error line-start "FLYCHECK_BEGIN ERROR\n"
+                (file-name) ":" line ":" column  ": error: "
                 (minimal-match
                  (message (one-or-more (one-or-more not-newline) "\n") ))
-                "FLYCHECK_END" line-end))
-      :modes (lean-mode)
-      :predicate
-      (lambda () (and buffer-file-name
-                 (string= "lean" (file-name-extension buffer-file-name))))))
-  (add-to-list 'flycheck-checkers 'lean-checker-file)
-  (add-hook 'lean-mode-hook '(lambda () (flycheck-mode t))))
+                "FLYCHECK_END" line-end)
+         (warning line-start "FLYCHECK_BEGIN WARNING\n"
+                  (file-name) ":" line ":" column  ": warning "
+                  (minimal-match
+                   (message (one-or-more (one-or-more not-newline) "\n") ))
+                  "FLYCHECK_END" line-end))
+        :modes (lean-mode)
+        :predicate
+        (lambda () (and buffer-file-name
+                   (string= "lean" (file-name-extension buffer-file-name))))))
+    (add-to-list 'flycheck-checkers 'lean-checker-file)
+    (setq lean-flycheck-initialized t)))
+
+(defun lean-flycheck-turn-on ()
+  (interactive)
+  (unless lean-flycheck-use
+    (when (interactive-p)
+      (message "use flycheck in lean-mode"))
+    (setq lean-flycheck-use t))
+  (lean-flycheck-init)
+  (flycheck-mode t))
+
+(defun lean-flycheck-turn-off ()
+  (interactive)
+  (when lean-flycheck-use
+    (when (interactive-p)
+      (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)))
+
+(add-hook 'lean-mode-hook '(lambda ()
+             (when lean-flycheck-use (lean-flycheck-turn-on))))
+
 (provide 'lean-flycheck)
diff --git a/src/emacs/lean-settings.el b/src/emacs/lean-settings.el
index 2e2c18209..14b9f4c37 100644
--- a/src/emacs/lean-settings.el
+++ b/src/emacs/lean-settings.el
@@ -30,7 +30,7 @@
   :group 'lean
   :type 'string)
 
-(defcustom lean-use-flycheck t
+(defcustom lean-flycheck-use t
   "Use flycheck for lean."
   :group 'lean
   :type 'boolean)