diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 775037d3b..b7a7c3192 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -268,7 +268,7 @@ class parser::imp {
     }
 
     [[ noreturn ]] void not_implemented_yet() {
-        // TODO
+        // TODO(Leo)
         throw parser_error("not implemented yet", pos());
     }
 
@@ -901,7 +901,7 @@ class parser::imp {
     }
 
     expr parse_string() {
-        // TODO
+        // TODO(Leo)
         not_implemented_yet();
     }
 
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 3d4c292f0..7eda10c28 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -321,7 +321,7 @@ class pp_fn {
             head = is_forall ? g_forall_fmt : g_exists_fmt;
         format sep  = comma();
         expr domain0 = nested[0].second;
-        // TODO: the following code is very similar to pp_abstraction
+        // TODO(Leo): the following code is very similar to pp_abstraction
         if (std::all_of(nested.begin() + 1, nested.end(), [&](std::pair<name, expr> const & p) { return p.second == domain0; })) {
             // Domain of all binders is the same
             format names    = pp_bnames(nested.begin(), nested.end(), false);
diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp
index 74b02124c..db0685d2d 100644
--- a/src/kernel/builtin.cpp
+++ b/src/kernel/builtin.cpp
@@ -203,7 +203,7 @@ void import_basic(environment & env) {
 
     // forall : Pi (A : Type u), (A -> Bool) -> Bool
     env.add_definition(forall_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Eq(P, Fun({x, A}, True))));
-    // TODO: introduce epsilon
+    // TODO(Leo): introduce epsilon
     env.add_definition(exists_fn_name, q_type, Fun({{A,TypeU}, {P, A_pred}}, Not(Forall(A, Fun({x, A}, Not(P(x)))))));
 
     // homogeneous equality