diff --git a/src/emacs/lean-settings.el b/src/emacs/lean-settings.el
index b8864c07f..9a6dce42e 100644
--- a/src/emacs/lean-settings.el
+++ b/src/emacs/lean-settings.el
@@ -129,4 +129,9 @@ false (nil)."
   :group 'lean
   :type 'boolean)
 
+(defcustom lean-show-proofstate-in-minibuffer nil
+  "Set this variable to true to show proof state at minibuffer."
+  :group 'lean
+  :type 'boolean)
+
 (provide 'lean-settings)