diff --git a/src/frontends/lean/scanner.cpp b/src/frontends/lean/scanner.cpp
index 74294e72e8..c2654e8caa 100644
--- a/src/frontends/lean/scanner.cpp
+++ b/src/frontends/lean/scanner.cpp
@@ -117,13 +117,20 @@ void scanner::check_not_eof(char const * error_msg) {
 static char const * g_end_error_str_msg = "unexpected end of string";
 static char const * g_end_error_char_msg = "unexpected end of character";
 
-unsigned scanner::hex_to_unsigned(char c) {
+optional<unsigned> scanner::try_hex_to_unsigned(char c) {
     if ('0' <= c && c <= '9')
-        return c - '0';
+        return optional<unsigned>(c - '0');
     else if ('a' <= c && c <= 'f')
-        return 10 + c - 'a';
+        return optional<unsigned>(10 + c - 'a');
     else if ('A' <= c && c <= 'F')
-        return 10 + c - 'A';
+        return optional<unsigned>(10 + c - 'A');
+    else
+        return optional<unsigned>();
+}
+
+unsigned scanner::hex_to_unsigned(char c) {
+    if (auto r = try_hex_to_unsigned(c))
+        return *r;
     else
         throw_exception("invalid hexadecimal digit");
 }
@@ -225,15 +232,38 @@ bool scanner::is_next_digit() {
         return false;
 }
 
+auto scanner::read_hex_number() -> token_kind {
+    lean_assert(curr() == 'x');
+    next();
+    m_num_val = 0;
+    bool found = false;
+    while (true) {
+        char c = curr();
+        if (auto d = try_hex_to_unsigned(c)) {
+            found = true;
+            m_num_val = 16 * m_num_val + *d;
+            next();
+        } else {
+            break;
+        }
+    }
+    if (!found)
+        throw exception("invalid hexadecimal numeral, hexadecimal digit expected");
+    return token_kind::Decimal;
+}
+
 auto scanner::read_number() -> token_kind {
     lean_assert('0' <= curr() && curr() <= '9');
     mpq q(1);
-    m_num_val = curr() - '0';
+    char c = curr();
     next();
-    bool is_decimal = false;
+    if (c == '0' && curr() == 'x')
+        return read_hex_number();
 
+    m_num_val = c - '0';
+    bool is_decimal = false;
     while (true) {
-        char c = curr();
+        c = curr();
         if ('0' <= c && c <= '9') {
             m_num_val = 10*m_num_val + (c - '0');
             if (is_decimal)
diff --git a/src/frontends/lean/scanner.h b/src/frontends/lean/scanner.h
index 012a45ec86..009f66b866 100644
--- a/src/frontends/lean/scanner.h
+++ b/src/frontends/lean/scanner.h
@@ -64,10 +64,12 @@ protected:
     void next_utf_core(char c, buffer<char> & cs);
     void next_utf(buffer<char> & cs);
 
+    optional<unsigned> try_hex_to_unsigned(char c);
     unsigned hex_to_unsigned(char c);
     char read_quoted_char(char const * error_msg);
     token_kind read_string();
     token_kind read_char();
+    token_kind read_hex_number();
     token_kind read_number();
     token_kind read_key_cmd_id();
     token_kind read_quoted_symbol();
diff --git a/tests/lean/hex_numeral.lean b/tests/lean/hex_numeral.lean
new file mode 100644
index 0000000000..53b7249c53
--- /dev/null
+++ b/tests/lean/hex_numeral.lean
@@ -0,0 +1,5 @@
+vm_eval (0xff : nat)
+vm_eval (0xffff : nat)
+vm_eval (0xaa : nat)
+vm_eval (0x10 : nat)
+vm_eval (0x10000 : nat)
diff --git a/tests/lean/hex_numeral.lean.expected.out b/tests/lean/hex_numeral.lean.expected.out
new file mode 100644
index 0000000000..29c2842dd1
--- /dev/null
+++ b/tests/lean/hex_numeral.lean.expected.out
@@ -0,0 +1,5 @@
+255
+65535
+170
+16
+65536