diff --git a/src/vim/syntax/lean.vim b/src/vim/syntax/lean.vim
index c87adf9ddd..a67965d8f1 100644
--- a/src/vim/syntax/lean.vim
+++ b/src/vim/syntax/lean.vim
@@ -61,6 +61,8 @@ syn region      leanEncl            matchgroup=leanDelim start="(" end=")" conta
 syn region      leanBracketEncl     matchgroup=leanDelim start="\[" end="\]" contains=ALLBUT,leanBrackErr keepend
 syn region      leanEncl            matchgroup=leanDelim start="{"  end="}" contains=ALLBUT,leanBraceErr,leanModifier keepend
 
+syn region      leanNotation        start=+`+    end=+`+
+
 syn keyword	leanTodo	containedin=leanComment TODO FIXME BUG FIX
 
 syn region      leanComment	start=+/-+ end=+-/+ contains=leanTodo
@@ -87,6 +89,8 @@ if version >= 508 || !exists("did_lean_syntax_inits")
   HiLink leanDelim              Keyword  " Delimiter is bad
   HiLink leanOp                 Keyword
 
+  HiLink leanNotation           String
+
   HiLink leanBraceError         Error
   HiLink leanParenError         Error
   HiLink leanBracketError       Error