diff --git a/doc/todo.md b/doc/todo.md
index c0b3b3baf..761ebd492 100644
--- a/doc/todo.md
+++ b/doc/todo.md
@@ -10,7 +10,7 @@ To Do List
    - We design our own configuration language.
    - We use an off-the-shelf embedded language such as [Lua](http://www.lua.org).
    - We use Lean itself.
-- Module for reading OpenTheory proofs.
+- Module for reading [OpenTheory](http://www.gilith.com/research/opentheory/) proofs.
 - Higher-Order unification and matching.
 - Rewriter (and Rewriter Combinators).
 - MCSat framework.