diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 89c9ce7ba..28f04a938 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -643,6 +643,40 @@ environment local_cmd(parser & p) {
     }
 }
 
+static environment help_cmd(parser & p) {
+    flycheck_information info(p.regular_stream());
+    if (info.enabled()) {
+        p.display_information_pos(p.cmd_pos());
+        p.regular_stream() << "help result:\n";
+    }
+    if (p.curr_is_token_or_id(get_options_tk())) {
+        p.next();
+        for (auto odecl : get_option_declarations()) {
+            auto opt = odecl.second;
+            regular(p.env(), p.ios())
+                << "  " << opt.get_name() << " (" << opt.kind() << ") "
+                << opt.get_description() << " (default: " << opt.get_default_value() << ")" << endl;
+        }
+    } else if (p.curr_is_token_or_id(get_commands_tk())) {
+        p.next();
+        buffer<name> ns;
+        cmd_table const & cmds = p.cmds();
+        cmds.for_each([&](name const & n, cmd_info const &) {
+                ns.push_back(n);
+            });
+        std::sort(ns.begin(), ns.end());
+        for (name const & n : ns) {
+            regular(p.env(), p.ios())
+                << "  " << n << ": " << cmds.find(n)->get_descr() << endl;
+        };
+    } else {
+        p.regular_stream()
+            << "help options  : describe available options\n"
+            << "help commands : describe available commands\n";
+    }
+    return p.env();
+}
+
 void init_cmd_table(cmd_table & r) {
     add_cmd(r, cmd_info("open",          "create aliases for declarations, and use objects defined in other namespaces",
                         open_cmd));
@@ -659,6 +693,7 @@ void init_cmd_table(cmd_table & r) {
     add_cmd(r, cmd_info("eval",          "evaluate given expression", eval_cmd));
     add_cmd(r, cmd_info("find_decl",     "find definitions and/or theorems", find_cmd));
     add_cmd(r, cmd_info("local",         "define local attributes or notation", local_cmd));
+    add_cmd(r, cmd_info("help",          "brief description of available commands and options", help_cmd));
     add_cmd(r, cmd_info("#erase_cache",  "erase cached definition (for debugging purposes)", erase_cache_cmd));
     add_cmd(r, cmd_info("#projections",  "generate projections for inductive datatype (for debugging purposes)", projections_cmd));
     add_cmd(r, cmd_info("#telescope_eq", "(for debugging purposes)", telescope_eq_cmd));
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 9281629e5..d4d61e0bf 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -213,7 +213,7 @@ expr parser::mk_by(expr const & t, pos_info const & pos) {
 }
 
 void parser::updt_options() {
-    m_verbose = get_verbose(m_ios.get_options());
+    m_verbose     = get_verbose(m_ios.get_options());
     m_show_errors = get_parser_show_errors(m_ios.get_options());
 }
 
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index e861c0dc8..57277301b 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -165,7 +165,6 @@ class parser {
     tag get_tag(expr e);
     expr copy_with_new_pos(expr const & e, pos_info p);
 
-    cmd_table const & cmds() const { return get_cmd_table(env()); }
     parse_table const & nud() const { return get_nud_table(env()); }
     parse_table const & led() const { return get_led_table(env()); }
 
@@ -231,6 +230,8 @@ public:
            info_manager * im = nullptr, keep_theorem_mode tmode = keep_theorem_mode::All);
     ~parser();
 
+    cmd_table const & cmds() const { return get_cmd_table(env()); }
+
     void set_cache(definition_cache * c) { m_cache = c; }
     void cache_definition(name const & n, expr const & pre_type, expr const & pre_value,
                           level_param_names const & ls, expr const & type, expr const & value);
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 2f474c839..fe25e3415 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -93,7 +93,7 @@ void init_token_table(token_table & t) {
          "[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[semireducible]", "[quasireducible]",
          "[parsing-only]", "[multiple-instances]",
          "evaluate", "check", "eval", "[wf]", "[whnf]", "[all-transparent]", "[priority", "[unfold-c", "print",
-         "end", "namespace", "section", "prelude",
+         "end", "namespace", "section", "prelude", "help",
          "import", "inductive", "record", "structure", "module", "universe", "universes", "local",
          "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context",
          "exit", "set_option", "open", "export", "calc_subst", "calc_refl", "calc_trans", "calc_symm", "tactic_hint",
diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp
index 1b691239f..82a3bb4d5 100644
--- a/src/frontends/lean/tokens.cpp
+++ b/src/frontends/lean/tokens.cpp
@@ -58,6 +58,7 @@ static name * g_raw          = nullptr;
 static name * g_true         = nullptr;
 static name * g_false        = nullptr;
 static name * g_options      = nullptr;
+static name * g_commands     = nullptr;
 static name * g_instances    = nullptr;
 static name * g_classes      = nullptr;
 static name * g_coercions    = nullptr;
@@ -180,6 +181,7 @@ void initialize_tokens() {
     g_true         = new name("true");
     g_false        = new name("false");
     g_options      = new name("options");
+    g_commands     = new name("commands");
     g_instances    = new name("instances");
     g_classes      = new name("classes");
     g_coercions    = new name("coercions");
@@ -310,6 +312,7 @@ void finalize_tokens() {
     delete g_true;
     delete g_false;
     delete g_options;
+    delete g_commands;
     delete g_instances;
     delete g_classes;
     delete g_coercions;
@@ -426,6 +429,7 @@ name const & get_raw_tk() { return *g_raw; }
 name const & get_true_tk() { return *g_true; }
 name const & get_false_tk() { return *g_false; }
 name const & get_options_tk() { return *g_options; }
+name const & get_commands_tk() { return *g_commands; }
 name const & get_instances_tk() { return *g_instances; }
 name const & get_classes_tk() { return *g_classes; }
 name const & get_coercions_tk() { return *g_coercions; }
diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h
index 4fffd620f..f107aa3f9 100644
--- a/src/frontends/lean/tokens.h
+++ b/src/frontends/lean/tokens.h
@@ -60,6 +60,7 @@ name const & get_raw_tk();
 name const & get_true_tk();
 name const & get_false_tk();
 name const & get_options_tk();
+name const & get_commands_tk();
 name const & get_instances_tk();
 name const & get_classes_tk();
 name const & get_coercions_tk();
diff --git a/tests/lean/run/help_cmd.lean b/tests/lean/run/help_cmd.lean
new file mode 100644
index 000000000..40e247fee
--- /dev/null
+++ b/tests/lean/run/help_cmd.lean
@@ -0,0 +1,5 @@
+help options
+
+help commands
+
+print options