diff --git a/src/emacs/lean-flycheck.el b/src/emacs/lean-flycheck.el
index 5aab24a92..09713c906 100644
--- a/src/emacs/lean-flycheck.el
+++ b/src/emacs/lean-flycheck.el
@@ -85,4 +85,18 @@ otherwise."
        (when (and (string= major-mode "lean-mode") col)
          (setf (flycheck-error-column ad-return-value) (1+ col))))))
 
+(defun lean-flycheck-delete-temporaries ()
+  "Delete temporaries files generated by flycheck."
+  (when (eq major-mode 'lean-mode)
+    (let* ((filename (buffer-file-name))
+           (tempname (format "%s_%s"
+                             flycheck-temp-prefix
+                             (file-name-nondirectory filename)))
+           (tempbase (file-name-base tempname))
+           (tempfile (expand-file-name tempbase
+                                       (file-name-directory filename)))
+           (exts     '(".ilean" ".d" ".clean" ".olean"))
+           (tempfiles (--map (concat tempfile it) exts)))
+      (mapc #'flycheck-safe-delete tempfiles))))
+
 (provide 'lean-flycheck)
diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el
index 175a97467..e2991f296 100644
--- a/src/emacs/lean-mode.el
+++ b/src/emacs/lean-mode.el
@@ -118,7 +118,9 @@ enabled and disabled respectively.")
 (defun lean-mode-setup ()
   "Default lean-mode setup"
   ;; Flycheck
-  (when lean-flycheck-use (lean-flycheck-turn-on))
+  (when lean-flycheck-use
+    (lean-flycheck-turn-on)
+    (add-hook 'flycheck-after-syntax-check-hook 'lean-flycheck-delete-temporaries nil t))
   ;; Draw a vertical line for rule-column
   (when (and lean-rule-column
              lean-show-rule-column-method)