diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 965901054..e093c4aeb 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -691,6 +691,13 @@ auto pretty_fn::pp_notation_child(expr const & e, unsigned lbp, unsigned rbp) ->
     }
 }
 
+static bool add_extra_space(name const & tk) {
+    // TODO(Leo): this is a hard-coded temporary solution for deciding whether extra
+    // spaces should be added or not when pretty printing notation.
+    // We should implement a better solution in the future.
+    return tk != "," && tk != "(" && tk != ")";
+}
+
 auto pretty_fn::pp_notation(notation_entry const & entry, buffer<optional<expr>> & args) -> optional<result> {
     if (entry.is_numeral()) {
         return some(result(format(entry.get_num())));
@@ -703,7 +710,8 @@ auto pretty_fn::pp_notation(notation_entry const & entry, buffer<optional<expr>>
         unsigned i         = ts.size();
         unsigned last_rbp  = max_bp()-1;
         unsigned token_lbp = 0;
-        bool last  = true;
+        bool extra_space   = false;
+        bool last          = true;
         while (i > 0) {
             --i;
             format curr;
@@ -723,7 +731,10 @@ auto pretty_fn::pp_notation(notation_entry const & entry, buffer<optional<expr>>
                     args.pop_back();
                     result e_r   = pp_notation_child(e, token_lbp, a.rbp());
                     format e_fmt = e_r.fmt();
-                    curr = format(tk) + space() + e_fmt;
+                    curr = format(tk);
+                    if (add_extra_space(tk))
+                        curr = curr + space();
+                    curr = curr + e_fmt;
                     if (last)
                         last_rbp = a.rbp();
                     break;
@@ -764,6 +775,8 @@ auto pretty_fn::pp_notation(notation_entry const & entry, buffer<optional<expr>>
                     unsigned curr_lbp = token_lbp;
                     if (auto t = a.get_terminator()) {
                         curr = format(*t);
+                        if (add_extra_space(*t))
+                            curr = space() + curr;
                         curr_lbp = get_some_precedence(m_token_table, *t);
                     }
                     unsigned i       = rec_args.size();
@@ -774,7 +787,9 @@ auto pretty_fn::pp_notation(notation_entry const & entry, buffer<optional<expr>>
                         result arg_res = pp_notation_child(rec_args[i], curr_lbp, a.rbp());
                         if (i == 0)
                             sep_fmt = format(tk);
-                        curr = sep_fmt + space() + arg_res.fmt() + space() + curr;
+                        curr = sep_fmt + space() + arg_res.fmt() + curr;
+                        if (i > 0 && add_extra_space(a.get_sep()))
+                            curr = space() + curr;
                         curr_lbp = sep_lbp;
                     }
                     break;
@@ -836,8 +851,11 @@ auto pretty_fn::pp_notation(notation_entry const & entry, buffer<optional<expr>>
                 fmt = curr;
                 last = false;
             } else {
-                fmt = curr + space() + fmt;
+                if (extra_space)
+                    curr = curr + space();
+                fmt = curr + fmt;
             }
+            extra_space = add_extra_space(tk);
         }
         unsigned first_lbp = token_lbp;
         if (!entry.is_nud()) {
diff --git a/tests/lean/notation3.lean.expected.out b/tests/lean/notation3.lean.expected.out
index 9c3da25ea..23662a4fc 100644
--- a/tests/lean/notation3.lean.expected.out
+++ b/tests/lean/notation3.lean.expected.out
@@ -1,5 +1,5 @@
 notation3.lean:2:0: warning: imported file uses 'sorry'
-[ a , b , b  ] : list num
-( a , true , a = b , b  ) : num × Prop × Prop × num
-( a , b  ) : num × num
-[ 1 , 2 + 2 , 3  ] : list num
+[ a, b, b ] : list num
+(a, true, a = b, b) : num × Prop × Prop × num
+(a, b) : num × num
+[ 1, 2 + 2, 3 ] : list num
diff --git a/tests/lean/notation4.lean.expected.out b/tests/lean/notation4.lean.expected.out
index 93f054583..33ced8645 100644
--- a/tests/lean/notation4.lean.expected.out
+++ b/tests/lean/notation4.lean.expected.out
@@ -1,5 +1,5 @@
 notation4.lean:2:0: warning: imported file uses 'sorry'
-∃ (A : Type₁) (x y : A) , x = y : Prop
-∃ (x : num) , x = 0 : Prop
-Σ (x : num) , x = 10 : Type₁
-Σ (A : Type₁) , list A : Type₂
+∃ (A : Type₁) (x y : A), x = y : Prop
+∃ (x : num), x = 0 : Prop
+Σ (x : num), x = 10 : Type₁
+Σ (A : Type₁), list A : Type₂
diff --git a/tests/lean/t10.lean.expected.out b/tests/lean/t10.lean.expected.out
index de918b25c..c32b625e6 100644
--- a/tests/lean/t10.lean.expected.out
+++ b/tests/lean/t10.lean.expected.out
@@ -7,6 +7,6 @@ has type
   B
 but is expected to have type
   N
-[ x , y , z , x , y , y  ] : list
-[ x  ] : list
+[ x, y, z, x, y, y ] : list
+[ x ] : list
 [ ] : list
diff --git a/tests/lean/t11.lean.expected.out b/tests/lean/t11.lean.expected.out
index d6f8a97a8..43663bc41 100644
--- a/tests/lean/t11.lean.expected.out
+++ b/tests/lean/t11.lean.expected.out
@@ -1,3 +1,3 @@
-∃ (x : A) , p x : bool
-∃ (x y : A) , q x y : bool
+∃ (x : A), p x : bool
+∃ (x y : A), q x y : bool
 λ (x : A), x : A → A