diff --git a/src/Lean/Declaration.lean b/src/Lean/Declaration.lean
index 4be29c4134..b764111dda 100644
--- a/src/Lean/Declaration.lean
+++ b/src/Lean/Declaration.lean
@@ -472,6 +472,10 @@ def isInductive : ConstantInfo → Bool
   | inductInfo _ => true
   | _            => false
 
+def isTheorem : ConstantInfo → Bool
+  | thmInfo _ => true
+  | _         => false
+
 def inductiveVal! : ConstantInfo → InductiveVal
   | .inductInfo val => val
   | _ => panic! "Expected a `ConstantInfo.inductInfo`."
diff --git a/src/Lean/Server/Completion.lean b/src/Lean/Server/Completion.lean
index bb0829f4b0..83a38dac54 100644
--- a/src/Lean/Server/Completion.lean
+++ b/src/Lean/Server/Completion.lean
@@ -207,6 +207,8 @@ private def getCompletionKindForDecl (constInfo : ConstantInfo) : M CompletionIt
       return CompletionItemKind.enum
     else
       return CompletionItemKind.struct
+  else if constInfo.isTheorem then
+    return CompletionItemKind.event
   else if (← isProjectionFn constInfo.name) then
     return CompletionItemKind.field
   else if (← whnf constInfo.type).isForall then
diff --git a/tests/lean/interactive/completion2.lean.expected.out b/tests/lean/interactive/completion2.lean.expected.out
index 6e34e10334..3f9aafd094 100644
--- a/tests/lean/interactive/completion2.lean.expected.out
+++ b/tests/lean/interactive/completion2.lean.expected.out
@@ -3,7 +3,7 @@
 {"items":
  [{"sortText": "0",
    "label": "ax1",
-   "kind": 3,
+   "kind": 23,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completion2.lean"},
@@ -11,7 +11,7 @@
     "id": {"const": {"declName": "Foo.Bla.ax1"}}}},
   {"sortText": "1",
    "label": "ex1",
-   "kind": 3,
+   "kind": 23,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completion2.lean"},
@@ -19,7 +19,7 @@
     "id": {"const": {"declName": "Foo.Bla.ex1"}}}},
   {"sortText": "2",
    "label": "ex2",
-   "kind": 3,
+   "kind": 23,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completion2.lean"},
@@ -27,7 +27,7 @@
     "id": {"const": {"declName": "Foo.Bla.ex2"}}}},
   {"sortText": "3",
    "label": "ex3",
-   "kind": 3,
+   "kind": 23,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completion2.lean"},
@@ -39,7 +39,7 @@
 {"items":
  [{"sortText": "0",
    "label": "ax1",
-   "kind": 3,
+   "kind": 23,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completion2.lean"},
@@ -47,7 +47,7 @@
     "id": {"const": {"declName": "Foo.Bla.ax1"}}}},
   {"sortText": "1",
    "label": "ex1",
-   "kind": 3,
+   "kind": 23,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completion2.lean"},
@@ -55,7 +55,7 @@
     "id": {"const": {"declName": "Foo.Bla.ex1"}}}},
   {"sortText": "2",
    "label": "ex2",
-   "kind": 3,
+   "kind": 23,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completion2.lean"},
@@ -63,7 +63,7 @@
     "id": {"const": {"declName": "Foo.Bla.ex2"}}}},
   {"sortText": "3",
    "label": "ex3",
-   "kind": 3,
+   "kind": 23,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completion2.lean"},
@@ -75,7 +75,7 @@
 {"items":
  [{"sortText": "0",
    "label": "ax1",
-   "kind": 3,
+   "kind": 23,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completion2.lean"},
@@ -83,7 +83,7 @@
     "id": {"const": {"declName": "Foo.Bla.ax1"}}}},
   {"sortText": "1",
    "label": "ex1",
-   "kind": 3,
+   "kind": 23,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completion2.lean"},
@@ -91,7 +91,7 @@
     "id": {"const": {"declName": "Foo.Bla.ex1"}}}},
   {"sortText": "2",
    "label": "ex2",
-   "kind": 3,
+   "kind": 23,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completion2.lean"},
@@ -99,7 +99,7 @@
     "id": {"const": {"declName": "Foo.Bla.ex2"}}}},
   {"sortText": "3",
    "label": "ex3",
-   "kind": 3,
+   "kind": 23,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completion2.lean"},
@@ -111,7 +111,7 @@
 {"items":
  [{"sortText": "0",
    "label": "ex1",
-   "kind": 3,
+   "kind": 23,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completion2.lean"},
@@ -119,7 +119,7 @@
     "id": {"const": {"declName": "Foo.Bla.ex1"}}}},
   {"sortText": "1",
    "label": "ex2",
-   "kind": 3,
+   "kind": 23,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completion2.lean"},
@@ -127,7 +127,7 @@
     "id": {"const": {"declName": "Foo.Bla.ex2"}}}},
   {"sortText": "2",
    "label": "ex3",
-   "kind": 3,
+   "kind": 23,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completion2.lean"},
diff --git a/tests/lean/interactive/completionFallback.lean.expected.out b/tests/lean/interactive/completionFallback.lean.expected.out
index 7cd2e288a0..0d524243dc 100644
--- a/tests/lean/interactive/completionFallback.lean.expected.out
+++ b/tests/lean/interactive/completionFallback.lean.expected.out
@@ -55,7 +55,7 @@
 {"items":
  [{"sortText": "0",
    "label": "ha",
-   "kind": 5,
+   "kind": 23,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionFallback.lean"},
@@ -63,7 +63,7 @@
     "id": {"const": {"declName": "CustomAnd.ha"}}}},
   {"sortText": "1",
    "label": "hb",
-   "kind": 5,
+   "kind": 23,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionFallback.lean"},
diff --git a/tests/lean/interactive/completionPrv.lean.expected.out b/tests/lean/interactive/completionPrv.lean.expected.out
index 6c62ec4e39..ac03b62acc 100644
--- a/tests/lean/interactive/completionPrv.lean.expected.out
+++ b/tests/lean/interactive/completionPrv.lean.expected.out
@@ -31,7 +31,7 @@
     "id": {"const": {"declName": "instToBoolBool"}}}},
   {"sortText": "2",
    "label": "BitVec.getElem_ofBoolListBE",
-   "kind": 3,
+   "kind": 23,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionPrv.lean"},
@@ -39,7 +39,7 @@
     "id": {"const": {"declName": "BitVec.getElem_ofBoolListBE"}}}},
   {"sortText": "3",
    "label": "BitVec.getLsbD_ofBoolListBE",
-   "kind": 3,
+   "kind": 23,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionPrv.lean"},
@@ -47,7 +47,7 @@
     "id": {"const": {"declName": "BitVec.getLsbD_ofBoolListBE"}}}},
   {"sortText": "4",
    "label": "BitVec.getMsbD_ofBoolListBE",
-   "kind": 3,
+   "kind": 23,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionPrv.lean"},
@@ -55,7 +55,7 @@
     "id": {"const": {"declName": "BitVec.getMsbD_ofBoolListBE"}}}},
   {"sortText": "5",
    "label": "BitVec.ofBool_and_ofBool",
-   "kind": 3,
+   "kind": 23,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionPrv.lean"},
@@ -63,7 +63,7 @@
     "id": {"const": {"declName": "BitVec.ofBool_and_ofBool"}}}},
   {"sortText": "6",
    "label": "BitVec.ofBool_or_ofBool",
-   "kind": 3,
+   "kind": 23,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionPrv.lean"},
@@ -71,7 +71,7 @@
     "id": {"const": {"declName": "BitVec.ofBool_or_ofBool"}}}},
   {"sortText": "7",
    "label": "BitVec.ofBool_xor_ofBool",
-   "kind": 3,
+   "kind": 23,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionPrv.lean"},
diff --git a/tests/lean/interactive/travellingCompletions.lean.expected.out b/tests/lean/interactive/travellingCompletions.lean.expected.out
index 46409f6f6b..15c1f442e7 100644
--- a/tests/lean/interactive/travellingCompletions.lean.expected.out
+++ b/tests/lean/interactive/travellingCompletions.lean.expected.out
@@ -39,7 +39,7 @@
 {"items":
  [{"sortText": "0",
    "label": "continuousAdd",
-   "kind": 3,
+   "kind": 23,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///travellingCompletions.lean"},
@@ -47,7 +47,7 @@
     "id": {"const": {"declName": "Prod.continuousAdd"}}}},
   {"sortText": "1",
    "label": "continuousSMul",
-   "kind": 3,
+   "kind": 23,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///travellingCompletions.lean"},