diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index f2ab2cc327..80540a7fa7 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -317,7 +317,11 @@ static environment definition_cmd_core(parser & p, def_cmd_kind kind, bool is_op
     lean_assert(!(is_private && is_protected));
     auto n_pos = p.pos();
     unsigned start_line = n_pos.first;
-    name n     = p.check_id_next("invalid declaration, identifier expected");
+    name n;
+    if (kind == Example)
+        n = p.mk_fresh_name();
+    else
+        n = p.check_id_next("invalid declaration, identifier expected");
     decl_modifiers modifiers;
     name real_n; // real name for this declaration
     buffer<name> ls_buffer;
diff --git a/tests/lean/run/enum.lean b/tests/lean/run/enum.lean
index 906ae00df9..06c8b44767 100644
--- a/tests/lean/run/enum.lean
+++ b/tests/lean/run/enum.lean
@@ -10,7 +10,7 @@ namespace Three
   theorem disj (a : Three) : a = zero ∨ a = one ∨ a = two :=
   rec (or.inl rfl) (or.inr (or.inl rfl)) (or.inr (or.inr rfl)) a
 
-  example ex1 (a : Three) : a ≠ zero → a ≠ one → a = two :=
+  example (a : Three) : a ≠ zero → a ≠ one → a = two :=
   rec (λ h₁ h₂, absurd rfl h₁) (λ h₁ h₂, absurd rfl h₂) (λ h₁ h₂, rfl) a
 
 end Three
diff --git a/tests/lean/run/example1.lean b/tests/lean/run/example1.lean
index 4d713c290d..52a75a2070 100644
--- a/tests/lean/run/example1.lean
+++ b/tests/lean/run/example1.lean
@@ -8,7 +8,7 @@ namespace day
   definition next_weekday d :=
   rec_on d tuesday wednesday thursday friday monday monday monday
 
-  example test_next_weekday : next_weekday (next_weekday saturday) = tuesday :=
+  example : next_weekday (next_weekday saturday) = tuesday :=
   rfl
 
 end day