diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp
index ad0937d95d..3a89b85478 100644
--- a/src/frontends/lean/info_manager.cpp
+++ b/src/frontends/lean/info_manager.cpp
@@ -473,6 +473,28 @@ struct info_manager::imp {
         }
     }
 
+    optional<pair<environment, options>> get_closest_env_opts(unsigned linenum) {
+        lock_guard<mutex> lc(m_mutex);
+        auto it = m_env_info.begin();
+        if (it == m_env_info.end())
+            return optional<pair<environment, options>>();
+        if (it->m_line > linenum)
+            return optional<pair<environment, options>>(it->m_env, it->m_options);
+        while (true) {
+            lean_assert(it != m_env_info.end() && it->m_line <= linenum);
+            auto next = it;
+            next++;
+            if (next == m_env_info.end() || next->m_line > linenum)
+                return optional<pair<environment, options>>(mk_pair(it->m_env, it->m_options));
+            it = next;
+        }
+    }
+
+    unsigned get_processed_upto() {
+        lock_guard<mutex> lc(m_mutex);
+        return m_processed_upto;
+    }
+
     void clear() {
         lock_guard<mutex> lc(m_mutex);
         if (m_block_new_info)
@@ -508,9 +530,15 @@ void info_manager::clear() { m_ptr->clear(); }
 optional<pair<environment, options>> info_manager::get_final_env_opts() const {
     return m_ptr->get_final_env_opts();
 }
+optional<pair<environment, options>> info_manager::get_closest_env_opts(unsigned linenum) const {
+    return m_ptr->get_closest_env_opts(linenum);
+}
 void info_manager::display(environment const & env, io_state const & ios, unsigned line) const {
     m_ptr->display(env, ios, line);
 }
+unsigned info_manager::get_processed_upto() const {
+    return m_ptr->m_processed_upto;
+}
 void info_manager::block_new_info(bool f) {
     m_ptr->block_new_info(f);
 }
diff --git a/src/frontends/lean/info_manager.h b/src/frontends/lean/info_manager.h
index 5119334245..3b0ea59776 100644
--- a/src/frontends/lean/info_manager.h
+++ b/src/frontends/lean/info_manager.h
@@ -35,8 +35,10 @@ public:
     bool is_invalidated(unsigned l) const;
     void save_environment_options(unsigned l, environment const & env, options const & o);
     optional<pair<environment, options>> get_final_env_opts() const;
+    optional<pair<environment, options>> get_closest_env_opts(unsigned linenum) const;
     void clear();
     void display(environment const & env, io_state const & ios, unsigned line) const;
     void block_new_info(bool f);
+    unsigned get_processed_upto() const;
 };
 }
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index aab2c6da78..3466e03711 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1235,6 +1235,7 @@ bool parser::parse_commands() {
             display_warning_pos(pos());
             regular_stream() << " imported file uses 'sorry'" << endl;
         }
+        commit_info(1);
         while (!done) {
             protected_call([&]() {
                     check_interrupted();
diff --git a/src/frontends/lean/server.cpp b/src/frontends/lean/server.cpp
index 23a9c9b890..441c526b19 100644
--- a/src/frontends/lean/server.cpp
+++ b/src/frontends/lean/server.cpp
@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "util/sstream.h"
 #include "util/exception.h"
 #include "util/sexpr/option_declarations.h"
+#include "library/aliases.h"
 #include "frontends/lean/server.h"
 #include "frontends/lean/parser.h"
 
@@ -255,6 +256,7 @@ static std::string g_options("OPTIONS");
 static std::string g_show("SHOW");
 static std::string g_valid("VALID");
 static std::string g_sleep("SLEEP");
+static std::string g_findp("FINDP");
 
 static bool is_command(std::string const & cmd, std::string const & line) {
     return line.compare(0, cmd.size(), cmd) == 0;
@@ -404,6 +406,94 @@ void server::show(bool valid) {
     m_out << "-- ENDSHOW" << std::endl;
 }
 
+static name string_to_name(std::string const & str) {
+    name result;
+    std::string id_part;
+    for (unsigned i = 0; i < str.size(); i++) {
+        if (str[i] == '.') {
+            result = name(result, id_part.c_str());
+            id_part.clear();
+        } else {
+            id_part.push_back(str[i]);
+        }
+    }
+    return name(result, id_part.c_str());
+}
+
+// Return true iff the last part of p is a prefix of the last part of n
+static bool is_last_prefix_of(name const & p, name const & n) {
+    if (p.is_string() && n.is_string()) {
+        char const * it1 = p.get_string();
+        char const * it2 = n.get_string();
+        if (!it1 || !it2)
+            return false;
+        while (*it1 && *it2 && *it1 == *it2) {
+            ++it1;
+            ++it2;
+        }
+        return *it1 == 0;
+    } else {
+        return false;
+    }
+}
+
+// Auxiliary function for find_prefix
+// 1) If p is atomic, then we just check if p is a prefix of the last component of n.
+// 2) Otherwise, we check if p.get_prefix() == n.get_prefix(), and
+//    p.get_string() is a prefix of n.get_string()
+static bool is_findp_prefix_of(name const & p, name const & n) {
+    if (p.is_atomic())
+        return is_last_prefix_of(p, n);
+    else
+        return p.get_prefix() == n.get_prefix() && is_last_prefix_of(p, n);
+}
+
+void server::display_decl(name const & short_name, name const & long_name, environment const & env, options const & o) {
+    declaration const & d = env.get(long_name);
+    io_state_stream out   = regular(env, m_ios).update_options(o);
+    out << short_name << "|" << mk_pair(flatten(out.get_formatter()(d.get_type())), o) << "\n";
+}
+
+void server::find_prefix(unsigned linenum, std::string const & prefix) {
+    check_file();
+    m_out << "-- BEGINFINDP";
+    unsigned upto = m_file->infom().get_processed_upto();
+    optional<pair<environment, options>> env_opts = m_file->infom().get_closest_env_opts(linenum);
+    if (!env_opts) {
+        m_out << " NAY" << std::endl;
+        m_out << "-- ENDFINDP" << std::endl;
+        return;
+    }
+    if (upto < linenum)
+        m_out << " STALE";
+    environment const & env = env_opts->first;
+    options opts            = env_opts->second;
+    opts = join(opts, m_ios.get_options());
+    m_out << std::endl;
+    name p = string_to_name(prefix);
+    name_set already_added;
+    for_each_expr_alias(env, [&](name const & n, list<name> const & ds) {
+            if (is_findp_prefix_of(p, n)) {
+                unsigned num = length(ds);
+                if (num == 1) {
+                    display_decl(n, head(ds), env, opts);
+                    already_added.insert(car(ds));
+                } else if (num > 1) {
+                    m_out << n << "\n";
+                    for (name const & d : ds) {
+                        display_decl(d, d, env, opts);
+                        already_added.insert(d);
+                    }
+                }
+            }
+        });
+    env.for_each_declaration([&](declaration const & d) {
+            if (!already_added.contains(d.get_name()) && is_findp_prefix_of(p, d.get_name()))
+                display_decl(d.get_name(), d.get_name(), env, opts);
+        });
+    m_out << "-- ENDFINDP" << std::endl;
+}
+
 bool server::operator()(std::istream & in) {
     for (std::string line; std::getline(in, line);) {
         try {
@@ -452,6 +542,10 @@ bool server::operator()(std::istream & in) {
                 unsigned ms = get_linenum(line, g_sleep);
                 chrono::milliseconds d(ms);
                 this_thread::sleep_for(d);
+            } else if (is_command(g_findp, line)) {
+                unsigned linenum = get_linenum(line, g_findp);
+                read_line(in, line);
+                find_prefix(linenum, line);
             } else {
                 throw exception(sstream() << "unexpected command line: " << line);
             }
diff --git a/src/frontends/lean/server.h b/src/frontends/lean/server.h
index 2c587aefcf..5698679a1c 100644
--- a/src/frontends/lean/server.h
+++ b/src/frontends/lean/server.h
@@ -82,6 +82,8 @@ class server {
     void set_option(std::string const & line);
     void eval_core(environment const & env, options const & o, std::string const & line);
     void eval(std::string const & line);
+    void display_decl(name const & short_name, name const & long_name, environment const & env, options const & o);
+    void find_prefix(unsigned linenum, std::string const & prefix);
     unsigned find(unsigned linenum);
     void read_line(std::istream & in, std::string & line);
     void interrupt_worker();
diff --git a/src/library/aliases.cpp b/src/library/aliases.cpp
index 57034eb15a..a11794764d 100644
--- a/src/library/aliases.cpp
+++ b/src/library/aliases.cpp
@@ -88,6 +88,10 @@ struct aliases_ext : public environment_extension {
         m_scopes = tail(m_scopes);
     }
 
+    void for_each_expr_alias(std::function<void(name const &, list<name> const &)> const & fn) {
+        m_state.m_aliases.for_each(fn);
+    }
+
     static environment using_namespace(environment const & env, io_state const &, name const &) {
         // do nothing, aliases are treated in a special way in the frontend.
         return env;
@@ -204,6 +208,11 @@ environment add_aliases(environment const & env, name const & prefix, name const
     return update(env, ext);
 }
 
+void for_each_expr_alias(environment const & env, std::function<void(name const &, list<name> const &)> const & fn) {
+    aliases_ext ext = get_extension(env);
+    ext.for_each_expr_alias(fn);
+}
+
 static int add_expr_alias(lua_State * L) {
     return push_environment(L, add_expr_alias(to_environment(L, 1), to_name_ext(L, 2), to_name_ext(L, 3)));
 }
diff --git a/src/library/aliases.h b/src/library/aliases.h
index 9f845f92d7..1d310f6c38 100644
--- a/src/library/aliases.h
+++ b/src/library/aliases.h
@@ -50,5 +50,7 @@ optional<name> get_level_alias(environment const & env, name const & n);
 environment add_aliases(environment const & env, name const & prefix, name const & new_prefix,
                         unsigned num_exceptions = 0, name const * exceptions = nullptr);
 
+void for_each_expr_alias(environment const & env, std::function<void(name const &, list<name> const &)> const & fn);
+
 void open_aliases(lua_State * L);
 }