diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el
index fd14cb77e..56c0cddd4 100644
--- a/src/emacs/lean-mode.el
+++ b/src/emacs/lean-mode.el
@@ -227,5 +227,20 @@ Invokes `lean-mode-hook'.
   (eval-after-load 'flycheck
     '(lean-flycheck-init)))
 
+
+;; Lean Info Mode (for "*lean-info*" buffer)
+;; Automode List
+;;;###autoload
+(define-derived-mode lean-info-mode prog-mode "Lean-Info"
+  "Major mode for Lean Info Buffer"
+  :syntax-table lean-syntax-table
+  :group 'lean
+  (set (make-local-variable 'font-lock-defaults) lean-info-font-lock-defaults)
+  (set (make-local-variable 'indent-tabs-mode) nil)
+  (set 'compilation-mode-font-lock-keywords '())
+  (set-input-method "Lean")
+  (set (make-local-variable 'lisp-indent-function)
+       'common-lisp-indent-function))
+
 (provide 'lean-mode)
 ;;; lean-mode.el ends here
diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el
index 1a74e8628..00679c930 100644
--- a/src/emacs/lean-syntax.el
+++ b/src/emacs/lean-syntax.el
@@ -131,4 +131,22 @@
      ;; lean-keywords
      (, (concat "\\(" (regexp-opt lean-keywords 'words) "\\)")
         (1 'font-lock-keyword-face)))))
+
+;; Syntax Highlighting for Lean Info Mode
+(defconst lean-info-font-lock-defaults
+  (let ((new-entries
+         `(;; Please add more after this:
+           (,(rx word-start (group (+ wordchar)) word-end (+ white) ":")
+            (1 'font-lock-variable-name-face))
+           (,(rx white ":" white)
+            . 'font-lock-keyword-face)
+           (,(rx "⊢" white)
+            . 'font-lock-keyword-face)
+           (,(rx "[" (group "stale") "]")
+            (1 'font-lock-warning-face))
+           (,(rx line-start "No Goal" line-end)
+            . 'font-lock-constant-face)))
+        (inherited-entries (car lean-font-lock-defaults)))
+    `(,(-concat new-entries inherited-entries))))
+
 (provide 'lean-syntax)