diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index 63c24f37a..9eca80e33 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -333,6 +333,7 @@ int main(int argc, char ** argv) {
         }
         if (ok && server && default_k == input_kind::Lean) {
             signal(SIGINT, on_ctrl_c);
+            ios.set_option(lean::name("pp", "beta"), true);
             lean::server Sv(env, ios, num_threads);
             if (!Sv(std::cin))
                 ok = false;
diff --git a/tests/lean/run/ppbeta.lean b/tests/lean/run/ppbeta.lean
new file mode 100644
index 000000000..c7a905fb2
--- /dev/null
+++ b/tests/lean/run/ppbeta.lean
@@ -0,0 +1,10 @@
+import data.int
+open [coercions] int
+open [coercions] nat
+
+definition lt (a b : int) := int.le (int.add a 1) b
+infix `<`     := lt
+infixl `+`:65 := int.add
+
+theorem lt_add_succ2 (a : int) (n : nat) : a < a + nat.succ n :=
+int.le_intro (show a + 1 + n = a + nat.succ n, from sorry)