diff --git a/src/frontends/lean/server.cpp b/src/frontends/lean/server.cpp
index cdde81485..9880d1356 100644
--- a/src/frontends/lean/server.cpp
+++ b/src/frontends/lean/server.cpp
@@ -648,17 +648,27 @@ void server::find_pattern(unsigned line_num, std::string const & pattern) {
     opts = join(opts, m_ios.get_options());
     m_out << std::endl;
     unsigned max_errors = get_fuzzy_match_max_errors(pattern.size());
+    std::vector<pair<name, name>> exact_matches;
     std::vector<pair<std::string, name>> selected;
     bitap_fuzzy_search matcher(pattern, max_errors);
     env.for_each_declaration([&](declaration const & d) {
             if (auto it = exact_prefix_match(env, pattern, d)) {
-                display_decl(*it, d.get_name(), env, opts);
+                exact_matches.emplace_back(*it, d.get_name());
             } else {
                 std::string text = d.get_name().to_string();
                 if (matcher.match(text))
                     selected.emplace_back(text, d.get_name());
             }
         });
+    if (!exact_matches.empty()) {
+        std::sort(exact_matches.begin(), exact_matches.end(),
+                  [](pair<name, name> const & p1, pair<name, name> const & p2) {
+                      return p1.first.size() < p2.first.size();
+                  });
+        for (pair<name, name> const & p : exact_matches) {
+            display_decl(p.first, p.second, env, opts);
+        }
+    }
     unsigned sz = selected.size();
     if (sz == 1) {
         display_decl(selected[0].second, env, opts);
diff --git a/tests/lean/interactive/findp.input b/tests/lean/interactive/findp.input
new file mode 100644
index 000000000..c5ef3178b
--- /dev/null
+++ b/tests/lean/interactive/findp.input
@@ -0,0 +1,4 @@
+VISIT findp.lean
+WAIT
+FINDP 7
+false
\ No newline at end of file
diff --git a/tests/lean/interactive/findp.input.expected.out b/tests/lean/interactive/findp.input.expected.out
new file mode 100644
index 000000000..58d75f863
--- /dev/null
+++ b/tests/lean/interactive/findp.input.expected.out
@@ -0,0 +1,11 @@
+-- BEGINWAIT
+-- ENDWAIT
+-- BEGINFINDP STALE
+false|Prop
+false.rec|∀ (C : Prop), false → C
+false_elim|false → ?c
+not_false_trivial|not false
+true_ne_false|not (eq true false)
+p_ne_false|?p → ne ?p false
+eq_false_elim|eq ?a false → not ?a
+-- ENDFINDP
diff --git a/tests/lean/interactive/findp.lean b/tests/lean/interactive/findp.lean
new file mode 100644
index 000000000..d69089c24
--- /dev/null
+++ b/tests/lean/interactive/findp.lean
@@ -0,0 +1,5 @@
+import logic.core.eq algebra.relation
+
+check proof_irrel
+
+check false