diff --git a/src/frontends/lean/scanner.cpp b/src/frontends/lean/scanner.cpp
index 402d72cdf..7d7181a62 100644
--- a/src/frontends/lean/scanner.cpp
+++ b/src/frontends/lean/scanner.cpp
@@ -150,18 +150,32 @@ auto scanner::read_quoted_symbol() -> token_kind {
     if (std::isdigit(curr()))
         throw_exception("first character of a quoted symbols cannot be a digit");
     m_buffer.clear();
+    bool start = true;
+    bool trailing_space = false;
     while (true) {
         check_not_eof("unexpected quoted identifier");
         char c = curr();
         next();
-        if (c == '`') {
-            m_name_val = name(m_buffer.c_str());
-            return token_kind::QuotedSymbol;
-        } else if (c != '\"' && c != '\n' && c != '\t') {
-            m_buffer += c;
-        } else {
-            // TODO(Leo): intra-token space
-            throw_exception("invalid quoted symbol, invalid character");
+        switch (c) {
+            case '`':
+                if (start)
+                    throw_exception("unexpected end of quoted symbol");
+                m_name_val = name(m_buffer.c_str());
+                return token_kind::QuotedSymbol;
+            case '\"':
+            case '\n':
+            case '\t':
+                throw_exception("invalid quoted symbol, invalid character");
+            case ' ':
+                if (!start)
+                    trailing_space = true;
+                m_buffer += c;
+                break;
+            default:
+                start = false;
+                if (trailing_space)
+                    throw_exception("unexpected space inside of quoted symbol");
+                m_buffer += c;
         }
     }
 }
diff --git a/tests/lean/bad_quoted_symbol.lean b/tests/lean/bad_quoted_symbol.lean
new file mode 100644
index 000000000..7723dd2c6
--- /dev/null
+++ b/tests/lean/bad_quoted_symbol.lean
@@ -0,0 +1,5 @@
+notation a ` \/ ` b := a ∨ b
+notation a `1\/` b := a ∨ b
+notation a ` \ / ` b := a ∨ b
+notation a ` ` b := a ∨ b
+notation `
diff --git a/tests/lean/bad_quoted_symbol.lean.expected.out b/tests/lean/bad_quoted_symbol.lean.expected.out
new file mode 100644
index 000000000..720e88dfe
--- /dev/null
+++ b/tests/lean/bad_quoted_symbol.lean.expected.out
@@ -0,0 +1,5 @@
+tests/lean/bad_quoted_symbol.lean:2:12: error: first character of a quoted symbols cannot be a digit
+tests/lean/bad_quoted_symbol.lean:3:16: error: unexpected space inside of quoted symbol
+tests/lean/bad_quoted_symbol.lean:4:14: error: unexpected end of quoted symbol
+tests/lean/bad_quoted_symbol.lean:5:10: error: invalid quoted symbol, invalid character
+tests/lean/bad_quoted_symbol.lean:5:10: error: invalid notation declaration, symbol expected