diff --git a/extras/latex/lstlean.tex b/extras/latex/lstlean.tex
index ca24aefcea..9e1a73fdd1 100644
--- a/extras/latex/lstlean.tex
+++ b/extras/latex/lstlean.tex
@@ -19,7 +19,7 @@ open, as, export, override, axiom, axioms, inductive, with, structure, record, u
 alias, help, environment, options, precedence, reserve,
 match, infix, infixl, infixr, notation, postfix, prefix,
 tactic_infix, tactic_infixl, tactic_infixr, tactic_notation, tactic_postfix, tactic_prefix,
-eval, check, coercion, end, reveal, this, suppose,
+eval, check, coercion, end, this, suppose,
 using, namespace, section, fields, find_decl,
 attribute, local, set_option, extends, include, omit, classes,
 instances, coercions, attributes, raw, migrate, replacing,
diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el
index 527b2a3cf4..5464e06fe1 100644
--- a/src/emacs/lean-syntax.el
+++ b/src/emacs/lean-syntax.el
@@ -16,7 +16,7 @@
     "structure" "record" "universe" "universes"
     "alias" "help" "precedence" "reserve" "declare_trace" "add_key_equivalence"
     "match" "infix" "infixl" "infixr" "notation" "postfix" "prefix" "instance"
-    "eval" "vm_eval" "check" "end" "reveal" "this" "suppose"
+    "eval" "vm_eval" "check" "end" "this" "suppose"
     "using" "using_well_founded" "namespace" "section" "fields"
     "attribute" "local" "set_option" "extends" "include" "omit" "classes" "class"
     "instances" "coercions" "attributes" "raw" "replacing"
diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 875c2be1d7..0e6a535998 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -577,17 +577,6 @@ static environment omit_cmd(parser & p) {
     return include_cmd_core(p, false);
 }
 
-
-static environment reveal_cmd(parser & p) {
-    buffer<name> ds;
-    name d          = p.check_constant_next("invalid 'reveal' command, constant expected");
-    ds.push_back(d);
-    while (p.curr_is_identifier()) {
-        ds.push_back(p.check_constant_next("invalid 'reveal' command, constant expected"));
-    }
-    return p.reveal_theorems(ds);
-}
-
 void register_decl_cmds(cmd_table & r) {
     add_cmd(r, cmd_info("universe",        "declare a universe level", universe_cmd));
     add_cmd(r, cmd_info("universes",       "declare universe levels", universes_cmd));
@@ -608,7 +597,6 @@ void register_decl_cmds(cmd_table & r) {
     add_cmd(r, cmd_info("theorem",         "add new theorem", definition_cmd, false));
     add_cmd(r, cmd_info("instance",        "add new instance", definition_cmd, false));
     add_cmd(r, cmd_info("example",         "add new example", definition_cmd, false));
-    add_cmd(r, cmd_info("reveal",          "reveal given theorems", reveal_cmd));
     add_cmd(r, cmd_info("include",         "force section parameter/variable to be included", include_cmd));
     add_cmd(r, cmd_info("attribute",       "set declaration attributes", attribute_cmd));
     add_cmd(r, cmd_info("@[",              "declaration attributes", compact_attribute_cmd));
diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp
index f694cd27b9..5e6a7e8f5b 100644
--- a/src/frontends/lean/definition_cmds.cpp
+++ b/src/frontends/lean/definition_cmds.cpp
@@ -345,7 +345,7 @@ static expr fix_rec_fn_name(expr const & e, name const & c_name, name const & c_
 
 static pair<environment, name>
 declare_definition(parser & p, environment const & env, def_cmd_kind kind, buffer<name> const & lp_names,
-                   name const & c_name, expr const & type, optional<expr> const & _val,
+                   name const & c_name, expr const & type, optional<expr> const & _val, task_result<expr> const & proof,
                    decl_modifiers const & modifiers, decl_attributes attrs, optional<std::string> const & doc_string,
                    pos_info const & pos) {
     auto env_n = mk_real_name(env, c_name, modifiers.m_is_private, pos);
@@ -357,7 +357,7 @@ declare_definition(parser & p, environment const & env, def_cmd_kind kind, buffe
     bool use_conv_opt = true;
     bool is_trusted   = !modifiers.m_is_meta;
     auto def          =
-        !val ? mk_axiom(c_real_name, to_list(lp_names), type) : (kind == Theorem ?
+        !val ? mk_theorem(c_real_name, to_list(lp_names), type, proof) : (kind == Theorem ?
         mk_theorem(c_real_name, to_list(lp_names), type, *val) :
         mk_definition(new_env, c_real_name, to_list(lp_names), type, *val, use_conv_opt, is_trusted));
     auto cdef         = check(p, new_env, c_name, def, pos);
@@ -764,9 +764,8 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
                     decl_env, p.get_options(), params_vec, new_fn, val,
                     elab.mctx(), elab.lctx(), p.get_parser_pos_provider(header_pos));
 
-            env_n = declare_definition(p, elab.env(), kind, lp_names, c_name, type, opt_val, modifiers, attrs,
+            env_n = declare_definition(p, elab.env(), kind, lp_names, c_name, type, opt_val, elab_task, modifiers, attrs,
                                        doc_string, header_pos);
-            p.add_delayed_theorem(delayed_theorem {false, decl_env, env_n.first.get(env_n.second), elab_task, {}});
         } else if (kind == Example) {
             std::vector<expr> params_vec(new_params.begin(), new_params.end());
             get_global_task_queue().submit<example_checking_task>(
@@ -789,7 +788,7 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
             }
             finalize_definition(elab, new_params, type, val, lp_names);
             opt_val = optional<expr>(val);
-            env_n = declare_definition(p, elab.env(), kind, lp_names, c_name, type, opt_val, modifiers, attrs, doc_string, header_pos);
+            env_n = declare_definition(p, elab.env(), kind, lp_names, c_name, type, opt_val, {}, modifiers, attrs, doc_string, header_pos);
         }
         environment new_env = env_n.first;
         name c_real_name    = env_n.second;
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 897d7066be..2a189828fe 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -183,7 +183,6 @@ parser::parser(environment const & env, io_state const & ios,
     if (s) {
         m_env                = s->m_env;
         m_ios.set_options(s->m_options);
-        m_delayed_thms       = s->m_delayed_thms;
         m_old_buckets_from_snapshot = s->m_sub_buckets;
         m_local_level_decls  = s->m_lds;
         m_local_decls        = s->m_eds;
@@ -2111,11 +2110,9 @@ void parser::process_imports() {
     unsigned fingerprint = 0;
     auto imports = parse_imports(fingerprint);
 
-    name_map<task_result<certified_declaration>> del_thms;
-
     for (auto & n : imports) {
         try {
-            m_env = import_module(m_env, m_file_name, n, del_thms, m_import_fn);
+            m_env = import_module(m_env, m_file_name, n, m_import_fn);
         } catch (exception & ex) {
             m_found_errors = true;
             parser_exception error((sstream() << "invalid import '" << n.m_name << "'").str(),
@@ -2127,13 +2124,6 @@ void parser::process_imports() {
         }
     }
 
-    del_thms.for_each([=] (name const & thm_name, task_result<certified_declaration> const & cdecl) {
-        delayed_theorem del_thm;
-        del_thm.m_imported = true;
-        del_thm.m_cert_decl = cdecl;
-        m_delayed_thms.insert(thm_name, del_thm);
-    });
-
     m_env = update_fingerprint(m_env, fingerprint);
     m_env = activate_export_decls(m_env, {}); // explicitly activate exports in root namespace
     m_env = replay_export_decls_core(m_env, m_ios);
@@ -2241,43 +2231,11 @@ bool parser::curr_is_command_like() const {
     }
 }
 
-static void replace_theorem(certified_declaration const & thm, environment & env, bool ignore_noncomputable) {
-    // TODO(gabriel): move somewhere else
-    env = env.replace(thm);
-    name const & thm_name = thm.get_declaration().get_name();
-    if (!ignore_noncomputable && !check_computable(env, thm_name)) {
-        throw exception(sstream() << "declaration '" << thm_name
-                        << "' was marked as a theorem, but it is a noncomputable definition");
-    }
-}
-
-environment parser::reveal_theorems(buffer<name> const & ds) {
-    environment env = m_env;
-    for (auto & d : ds) {
-        if (auto * dt = m_delayed_thms.find(d)) {
-            replace_theorem(dt->m_cert_decl.get(), env, m_ignore_noncomputable);
-        } else {
-            throw exception(sstream() << "not a delayed theorem: " << d);
-        }
-    }
-    return env;
-}
-
-environment parser::reveal_all_theorems() {
-    buffer<name> ds;
-    m_delayed_thms.for_each([&] (name const & d, delayed_theorem const &) { ds.push_back(d); });
-    return reveal_theorems(ds);
-}
-
-bool parser::is_delayed_theorem(name const & n) {
-    return m_delayed_thms.contains(n);
-}
-
 void parser::save_snapshot(scope_message_context & smc) {
     if (!m_snapshot_vector)
         return;
     if (m_snapshot_vector->empty() || m_snapshot_vector->back().m_pos != m_scanner.get_pos_info()) {
-        m_snapshot_vector->push_back(snapshot(m_env, smc.get_sub_buckets(), m_delayed_thms, m_local_level_decls, m_local_decls,
+        m_snapshot_vector->push_back(snapshot(m_env, smc.get_sub_buckets(), m_local_level_decls, m_local_decls,
                                               m_level_variables, m_variables, m_include_vars,
                                               m_ios.get_options(), m_imports_parsed, m_parser_scope_stack, m_scanner.get_pos_info()));
     }
@@ -2309,37 +2267,6 @@ message_builder parser::mk_message(message_severity severity) {
     return mk_message(pos(), severity);
 }
 
-class proof_checking_task : public module_task<certified_declaration> {
-    delayed_theorem m_del_thm;
-public:
-    proof_checking_task(delayed_theorem const & del_thm, pos_info const & pos) :
-            module_task(optional<pos_info>(pos), task_kind::elab), m_del_thm(del_thm) {}
-
-    void description(std::ostream & out) const override {
-        out << "checking " << m_del_thm.m_ax_decl.get_name() << " (" << get_module() << ")";
-    }
-
-    std::vector<generic_task_result> get_dependencies() override { return { m_del_thm.m_proof }; }
-
-    certified_declaration execute_core() override {
-        auto & ax_decl = m_del_thm.m_ax_decl;
-        auto thm_decl = mk_theorem(ax_decl.get_name(), ax_decl.get_univ_params(),
-                                   ax_decl.get_type(), m_del_thm.m_proof.get());
-        // TODO(gabriel): noncomputability check
-        return check(m_del_thm.m_decl_env, thm_decl);
-    }
-};
-
-void parser::add_delayed_theorem(delayed_theorem del_thm) {
-    del_thm.m_imported = false;
-    del_thm.m_cert_decl = get_global_task_queue().submit<proof_checking_task>(del_thm, m_last_cmd_pos);
-    if (m_stop_at) {
-        // TODO(gabriel): check whether the theorem covers the line we stop at
-        del_thm.m_proof.get();
-    }
-    m_delayed_thms.insert(del_thm.m_ax_decl.get_name(), del_thm);
-}
-
 bool parse_commands(environment & env, io_state & ios, char const * fname, optional<std::string> const & base_dir,
                     bool use_exceptions, unsigned num_threads) {
     st_task_queue tq;
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index d4e4fcc833..daaa8d84b5 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -53,19 +53,10 @@ struct parser_scope {
 };
 typedef list<parser_scope> parser_scope_stack;
 
-struct delayed_theorem {
-    bool m_imported;
-    environment m_decl_env;
-    declaration m_ax_decl;
-    task_result<expr> m_proof;
-    task_result<certified_declaration> m_cert_decl;
-};
-
 /** \brief Snapshot of the state of the Lean parser */
 struct snapshot {
     environment        m_env;
     name_set           m_sub_buckets;
-    name_map<delayed_theorem> m_delayed_thms;
     local_level_decls  m_lds;
     local_expr_decls   m_eds;
     name_set           m_lvars; // subset of m_lds that is tagged as level variable
@@ -75,11 +66,11 @@ struct snapshot {
     bool               m_imports_parsed;
     parser_scope_stack m_parser_scope_stack;
     pos_info           m_pos;
-    snapshot(environment const & env, name_set const & sub_buckets, name_map<delayed_theorem> delayed_thms, local_level_decls const & lds,
+    snapshot(environment const & env, name_set const & sub_buckets, local_level_decls const & lds,
              local_expr_decls const & eds, name_set const & lvars, name_set const & vars,
              name_set const & includes, options const & opts, bool imports_parsed, parser_scope_stack const & pss,
              pos_info const & pos):
-        m_env(env), m_sub_buckets(sub_buckets), m_delayed_thms(delayed_thms), m_lds(lds), m_eds(eds), m_lvars(lvars), m_vars(vars), m_include_vars(includes),
+        m_env(env), m_sub_buckets(sub_buckets), m_lds(lds), m_eds(eds), m_lvars(lvars), m_vars(vars), m_include_vars(includes),
         m_options(opts), m_imports_parsed(imports_parsed), m_parser_scope_stack(pss), m_pos(pos) {}
 };
 
@@ -157,9 +148,6 @@ class parser : public abstract_parser {
     // Docgen
     optional<std::string>  m_doc_string;
 
-    // delayed theorems
-    name_map<delayed_theorem> m_delayed_thms;
-
     void throw_parser_exception(char const * msg, pos_info p);
     void throw_nested_exception(throwable const & ex, pos_info p);
 
@@ -253,9 +241,6 @@ public:
     environment const & env() const { return m_env; }
     io_state const & ios() const { return m_ios; }
 
-    name_map<delayed_theorem> get_delayed_theorems() const { return m_delayed_thms; }
-    void add_delayed_theorem(delayed_theorem);
-
     message_builder mk_message(pos_info const & p, message_severity severity);
     message_builder mk_message(message_severity severity);
 
@@ -286,10 +271,6 @@ public:
     expr mk_app(expr fn, buffer<expr> const & args, pos_info const & p);
     expr mk_app(std::initializer_list<expr> const & args, pos_info const & p);
 
-    bool is_delayed_theorem(name const &);
-    environment reveal_theorems(buffer<name> const & ds);
-    environment reveal_all_theorems();
-
     /** \brief Read the next token. */
     void scan();
     /** \brief Return the current token */
diff --git a/src/frontends/lean/print_cmd.cpp b/src/frontends/lean/print_cmd.cpp
index 61ff9079fb..39611afafd 100644
--- a/src/frontends/lean/print_cmd.cpp
+++ b/src/frontends/lean/print_cmd.cpp
@@ -72,7 +72,7 @@ struct print_axioms_deps {
 static void print_axioms(parser & p, message_builder & out) {
     if (p.curr_is_identifier()) {
         name c = p.check_constant_next("invalid 'print axioms', constant expected");
-        auto env = p.reveal_all_theorems(); // FIXME
+        auto env = p.env();
         type_context tc(env, p.get_options());
         auto new_out = io_state_stream(env, p.ios(), tc, out.get_text_stream().get_channel());
         print_axioms_deps(env, new_out)(c);
@@ -80,7 +80,7 @@ static void print_axioms(parser & p, message_builder & out) {
         bool has_axioms = false;
         p.env().for_each_declaration([&](declaration const & d) {
                 name const & n = d.get_name();
-                if (!d.is_definition() && !p.env().is_builtin(n) && d.is_trusted() && !p.is_delayed_theorem(n)) {
+                if (!d.is_definition() && !p.env().is_builtin(n) && d.is_trusted()) {
                     out << n << " : " << d.get_type() << endl;
                     has_axioms = true;
                 }
@@ -216,7 +216,7 @@ static void print_definition(environment const & env, message_builder & out, nam
     declaration d = env.get(n);
     if (d.is_axiom())
         throw parser_error(sstream() << "invalid 'print definition', theorem '" << to_user_name(env, n)
-                           << "' is not available (suggestion: use command 'reveal " << to_user_name(env, n) << "')", pos);
+                           << "' is not available", pos);
     if (!d.is_definition())
         throw parser_error(sstream() << "invalid 'print definition', '" << to_user_name(env, n) << "' is not a definition", pos);
     options opts        = out.get_text_stream().get_options();
@@ -357,12 +357,6 @@ bool print_id_info(parser & p, message_builder & out, name const & id, bool show
                         print_constant(p, out, "eliminator", d);
                     } else if (is_quotient_decl(env, c)) {
                         print_constant(p, out, "builtin-quotient-type-constant", d);
-                    } else if (d.is_axiom() && p.is_delayed_theorem(c)) {
-                        buffer<name> ns; ns.push_back(c);
-                        auto revealed_env = p.reveal_theorems(ns);
-                        print_constant(p, out, "[delayed] theorem", revealed_env.get(c), show_value);
-                        if (show_value)
-                            print_definition(revealed_env, out, c, pos);
                     } else if (d.is_axiom()) {
                         print_constant(p, out, "axiom", d);
                     } else {
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index bdf9c03e9b..fb068a50da 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -99,7 +99,7 @@ void init_token_table(token_table & t) {
          {"renaming", 0}, {"extends", 0}, {nullptr, 0}};
 
     char const * commands[] =
-        {"theorem", "axiom", "axioms", "variable", "protected", "private", "reveal",
+        {"theorem", "axiom", "axioms", "variable", "protected", "private",
          "definition", "meta", "mutual", "example", "coercion", "noncomputable",
          "variables", "parameter", "parameters", "constant", "constants",
          "evaluate", "check", "eval", "vm_eval", "using_well_founded", "[whnf]",
diff --git a/src/kernel/declaration.cpp b/src/kernel/declaration.cpp
index affc5ded43..990c4135e0 100644
--- a/src/kernel/declaration.cpp
+++ b/src/kernel/declaration.cpp
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <util/task_queue.h>
 #include "kernel/declaration.h"
 #include "kernel/environment.h"
 #include "kernel/for_each_fn.h"
@@ -48,7 +49,7 @@ declaration::~declaration() { if (m_ptr) m_ptr->dec_ref(); }
 declaration & declaration::operator=(declaration const & s) { LEAN_COPY_REF(s); }
 declaration & declaration::operator=(declaration && s) { LEAN_MOVE_REF(s); }
 
-bool declaration::is_definition() const    { return static_cast<bool>(m_ptr->m_value); }
+bool declaration::is_definition() const    { return static_cast<bool>(m_ptr->m_value) || static_cast<bool>(m_ptr->m_proof); }
 bool declaration::is_constant_assumption() const { return !is_definition(); }
 bool declaration::is_axiom() const         { return is_constant_assumption() && m_ptr->m_theorem; }
 bool declaration::is_theorem() const       { return is_definition() && m_ptr->m_theorem; }
@@ -59,12 +60,23 @@ level_param_names const & declaration::get_univ_params() const { return m_ptr->m
 unsigned declaration::get_num_univ_params() const { return length(get_univ_params()); }
 expr const & declaration::get_type() const { return m_ptr->m_type; }
 
-expr const & declaration::get_value() const { lean_assert(is_definition()); return *(m_ptr->m_value); }
+task_result<expr> const & declaration::get_value_task() const {
+    lean_assert(is_definition());
+    return m_ptr->m_proof;
+}
+expr const & declaration::get_value() const {
+    lean_assert(is_definition());
+    if (m_ptr->m_proof) {
+        return m_ptr->m_proof.get();
+    } else {
+        return *(m_ptr->m_value);
+    }
+}
 reducibility_hints const & declaration::get_hints() const { return m_ptr->m_hints; }
 
 declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v,
                           reducibility_hints const & h, bool trusted) {
-    return declaration(new declaration::cell(n, params, t, false, v, h, trusted));
+    return declaration(new declaration::cell(n, params, t, v, h, trusted));
 }
 static unsigned get_max_height(environment const & env, expr const & v) {
     unsigned h = 0;
@@ -84,8 +96,11 @@ declaration mk_definition(environment const & env, name const & n, level_param_n
     unsigned h = get_max_height(env, v);
     return mk_definition(n, params, t, v, reducibility_hints::mk_regular(h+1, use_self_opt), trusted);
 }
+declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, task_result<expr> const & v) {
+    return declaration(new declaration::cell(n, params, t, v));
+}
 declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v) {
-    return declaration(new declaration::cell(n, params, t, true, v, reducibility_hints::mk_opaque(), true));
+    return mk_theorem(n, params, t, mk_pure_task_result(v, {}));
 }
 declaration mk_axiom(name const & n, level_param_names const & params, expr const & t) {
     return declaration(new declaration::cell(n, params, t, true, true));
diff --git a/src/kernel/declaration.h b/src/kernel/declaration.h
index edc9fc86cd..c674e1a3a1 100644
--- a/src/kernel/declaration.h
+++ b/src/kernel/declaration.h
@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include <string>
 #include <limits>
 #include "util/rc.h"
+#include "util/task_queue.h"
 #include "kernel/expr.h"
 
 namespace lean {
@@ -75,6 +76,7 @@ class declaration {
         expr               m_type;
         bool               m_theorem;
         optional<expr>     m_value;        // if none, then declaration is actually a postulate
+        task_result<expr>  m_proof;
         reducibility_hints m_hints;
         /* Definitions are trusted by default, and nested macros are expanded when kernel is instantiated with
            trust level 0. When this flag is false, then we do not expand nested macros. We say the
@@ -86,10 +88,13 @@ class declaration {
         cell(name const & n, level_param_names const & params, expr const & t, bool is_axiom, bool trusted):
             m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(is_axiom),
             m_hints(reducibility_hints::mk_opaque()), m_trusted(trusted) {}
-        cell(name const & n, level_param_names const & params, expr const & t, bool is_thm, expr const & v,
+        cell(name const & n, level_param_names const & params, expr const & t, expr const & v,
              reducibility_hints const & h, bool trusted):
-            m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(is_thm),
+            m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(false),
             m_value(v), m_hints(h), m_trusted(trusted) {}
+        cell(name const & n, level_param_names const & params, expr const & t, task_result<expr> const & v):
+            m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(true),
+            m_proof(v), m_hints(reducibility_hints::mk_opaque()), m_trusted(true) {}
     };
     cell * m_ptr;
     explicit declaration(cell * ptr);
@@ -127,6 +132,7 @@ public:
     unsigned get_num_univ_params() const;
     expr const & get_type() const;
 
+    task_result<expr> const & get_value_task() const;
     expr const & get_value() const;
 
     reducibility_hints const & get_hints() const;
@@ -135,7 +141,7 @@ public:
                                      reducibility_hints const & hints, bool trusted);
     friend declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t,
                                      expr const & v, bool use_conv_opt, bool trusted);
-    friend declaration mk_theorem(name const &, level_param_names const &, expr const &, expr const &);
+    friend declaration mk_theorem(name const &, level_param_names const &, expr const &, task_result<expr> const &);
     friend declaration mk_axiom(name const & n, level_param_names const & params, expr const & t);
     friend declaration mk_constant_assumption(name const & n, level_param_names const & params, expr const & t, bool trusted);
 };
@@ -149,6 +155,7 @@ declaration mk_definition(name const & n, level_param_names const & params, expr
 declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t, expr const & v,
                           bool use_conv_opt = true, bool trusted = true);
 declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v);
+declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, task_result<expr> const & v);
 declaration mk_axiom(name const & n, level_param_names const & params, expr const & t);
 declaration mk_constant_assumption(name const & n, level_param_names const & params, expr const & t, bool trusted = true);
 
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index 4b9ba6370a..cdd08be417 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -6,6 +6,8 @@ Author: Leonardo de Moura
 */
 #include <utility>
 #include <vector>
+#include <util/task_queue.h>
+#include <library/module_mgr.h>
 #include "util/interrupt.h"
 #include "util/lbool.h"
 #include "util/flet.h"
@@ -745,7 +747,7 @@ static void check_duplicated_params(environment const & env, declaration const &
     }
 }
 
-certified_declaration check(environment const & env, declaration const & d) {
+static void check_core(environment const & env, declaration const & d) {
     if (d.is_definition())
         check_no_mlocal(env, d.get_name(), d.get_value(), false);
     check_no_mlocal(env, d.get_name(), d.get_type(), true);
@@ -759,8 +761,66 @@ certified_declaration check(environment const & env, declaration const & d) {
         expr val_type = checker.check(d.get_value(), d.get_univ_params());
         if (!checker.is_def_eq(val_type, d.get_type())) {
             throw_kernel_exception(env, d.get_value(), [=](formatter const & fmt) {
+                return pp_def_type_mismatch(fmt, d.get_name(), d.get_type(), val_type, true);
+            });
+        }
+    }
+}
+
+class proof_checking_task : public module_task<expr> {
+    environment m_env;
+    declaration m_decl;
+public:
+    proof_checking_task(environment const & env, declaration const & d) :
+            module_task({}, task_kind::elab), m_env(env), m_decl(d) {
+        lean_assert(d.is_theorem());
+    }
+
+    void description(std::ostream & out) const override {
+        out << "type-checking " << m_decl.get_name();
+    }
+
+    std::vector<generic_task_result> get_dependencies() override {
+        return { m_decl.get_value_task() };
+    }
+
+    expr execute_core() override {
+        // TODO(gabriel): noncomputable check
+        bool memoize = true;
+        bool trusted_only = m_decl.is_trusted();
+        type_checker checker(m_env, memoize, trusted_only);
+        expr val_type = checker.check(m_decl.get_value(), m_decl.get_univ_params());
+        if (!checker.is_def_eq(val_type, m_decl.get_type())) {
+            throw_kernel_exception(m_env, m_decl.get_value(), [=](formatter const &fmt) {
+                return pp_def_type_mismatch(fmt, m_decl.get_name(), m_decl.get_type(), val_type, true);
+            });
+        }
+        return m_decl.get_value();
+    }
+};
+
+certified_declaration check(environment const & env, declaration const & d) {
+    if (d.is_definition())
+        check_no_mlocal(env, d.get_name(), d.get_value(), false);
+    check_no_mlocal(env, d.get_name(), d.get_type(), true);
+    check_name(env, d.get_name());
+    check_duplicated_params(env, d);
+    bool memoize = true; bool trusted_only = d.is_trusted();
+    type_checker checker(env, memoize, trusted_only);
+    expr sort = checker.check(d.get_type(), d.get_univ_params());
+    checker.ensure_sort(sort, d.get_type());
+    if (d.is_definition()) {
+        if (env.trust_lvl() != 0 && d.is_theorem()) {
+            auto checked_proof = get_global_task_queue().submit<proof_checking_task>(env, d);
+            return certified_declaration(env.get_id(),
+                                         mk_theorem(d.get_name(), d.get_univ_params(), d.get_type(), checked_proof));
+        } else {
+            expr val_type = checker.check(d.get_value(), d.get_univ_params());
+            if (!checker.is_def_eq(val_type, d.get_type())) {
+                throw_kernel_exception(env, d.get_value(), [=](formatter const &fmt) {
                     return pp_def_type_mismatch(fmt, d.get_name(), d.get_type(), val_type, true);
                 });
+            }
         }
     }
     return certified_declaration(env.get_id(), d);
diff --git a/src/library/module.cpp b/src/library/module.cpp
index 57d92c3c8c..d44da3a66a 100644
--- a/src/library/module.cpp
+++ b/src/library/module.cpp
@@ -182,6 +182,19 @@ deserializer & operator>>(deserializer & d, module_name & r) {
     return d;
 }
 
+LEAN_THREAD_PTR(std::vector<task_result<expr>>, g_export_delayed_proofs);
+class scoped_delayed_proofs {
+    std::vector<task_result<expr>> * m_old;
+public:
+    scoped_delayed_proofs(std::vector<task_result<expr>> & r) {
+        m_old = g_export_delayed_proofs;
+        g_export_delayed_proofs = &r;
+    }
+    ~scoped_delayed_proofs() {
+        g_export_delayed_proofs = m_old;
+    }
+};
+
 void export_module(std::ostream & out, environment const & env) {
     module_ext const & ext = get_extension(env);
 
@@ -219,6 +232,13 @@ void export_module(std::ostream & out, environment const & env) {
         s2.write_char(r[i]);
 }
 
+std::vector<task_result<expr>> export_module_delayed(std::ostream & out, environment const & env) {
+    std::vector<task_result<expr>> delayed_proofs;
+    scoped_delayed_proofs _(delayed_proofs);
+    export_module(out, env);
+    return delayed_proofs;
+}
+
 typedef std::unordered_map<std::string, module_object_reader> object_readers;
 static object_readers * g_object_readers = nullptr;
 static object_readers & get_object_readers() { return *g_object_readers; }
@@ -262,10 +282,21 @@ environment update_module_defs(environment const & env, declaration const & d) {
     }
 }
 
+static declaration theorem2axiom(declaration const & decl) {
+    lean_assert(decl.is_theorem());
+    return mk_axiom(decl.get_name(), decl.get_univ_params(), decl.get_type());
+}
+
 static environment export_decl(environment const & env, declaration const & d) {
     name n = d.get_name();
     return add(env, *g_decl_key, [=](environment const & env, serializer & s) {
-            s << env.get(n);
+            auto d = env.get(n);
+            if (g_export_delayed_proofs && d.is_theorem()) {
+                s << true << theorem2axiom(d) << static_cast<unsigned>(g_export_delayed_proofs->size());
+                g_export_delayed_proofs->push_back(d.get_value_task());
+            } else {
+                s << false << d;
+            }
         });
 }
 
@@ -354,85 +385,45 @@ struct import_helper {
     }
 };
 
-class theorem_import_task : public module_task<certified_declaration> {
-    environment m_decl_env;
-    declaration m_ax_decl;
-    task_result<expr> m_proof;
-public:
-    theorem_import_task(environment const & decl_env, declaration ax_decl, task_result<expr> const & proof) :
-            module_task(optional<pos_info>(), task_kind::elab),
-            m_decl_env(decl_env), m_ax_decl(ax_decl), m_proof(proof) {}
-
-    certified_declaration execute_core() override {
-        auto proof = m_proof.get();
-        auto decl = mk_theorem(m_ax_decl.get_name(), m_ax_decl.get_univ_params(),
-                               m_ax_decl.get_type(), proof);
-        return import_helper::certify_or_check(m_decl_env, decl);
-    }
-
-    void description(std::ostream & out) const override {
-        out << "importing theorem " << m_ax_decl.get_name();
-    }
-
-    bool is_tiny() const override { return m_decl_env.trust_lvl() != 0; }
-
-    std::vector<generic_task_result> get_dependencies() override {
-        return {m_proof};
-    }
-};
-
 static void import_module(environment & env, std::string const & module_file_name, module_name const & ref,
-                          name_map<task_result<certified_declaration>> & del_thms, module_loader const & mod_ldr) {
+                          module_loader const & mod_ldr) {
     auto res = mod_ldr(module_file_name, ref);
     if (get_extension(env).m_imported.contains(res.m_module_name)) return;
     std::istringstream in(res.m_obj_code, std::ios_base::binary);
     auto olean = parse_olean(in, res.m_module_name, false);
     for (auto & dep : olean.first) {
-        import_module(env, res.m_module_name, dep, del_thms, mod_ldr);
+        import_module(env, res.m_module_name, dep, mod_ldr);
     }
     auto ext = get_extension(env);
     ext.m_imported.insert(res.m_module_name);
     env = update(env, ext);
-    import_module(olean.second, res.m_module_name, env);
-    res.m_delayed_proofs.for_each([&] (name const & n, task_result<expr> const & delayed_proof) {
-        del_thms.insert(n, get_global_task_queue().submit<theorem_import_task>(
-                env, env.get(n), delayed_proof));
-    });
+    import_module(olean.second, res.m_module_name, env, res.m_delayed_proofs);
 }
 
 environment import_module(environment const & env0, std::string const & module_file_name,
                           module_name const & ref,
-                          name_map<task_result<certified_declaration>> & del_thms,
                           module_loader const & mod_ldr) {
     environment env = env0;
     module_ext ext = get_extension(env);
     ext.m_direct_imports = cons(ref, ext.m_direct_imports);
     env = update(env, ext);
-    import_module(env, module_file_name, ref, del_thms, mod_ldr);
+    import_module(env, module_file_name, ref, mod_ldr);
     return env;
 }
 
-environment import_module(environment const & env, std::string const & current_mod, module_name const & ref,
-                          module_loader const & mod_ldr) {
-    name_map<task_result<certified_declaration>> del_thms;
-    return import_module(env, current_mod, ref, del_thms, mod_ldr);
-}
-
-static declaration theorem2axiom(declaration const & decl) {
-    lean_assert(decl.is_theorem());
-    return mk_axiom(decl.get_name(), decl.get_univ_params(), decl.get_type());
-}
-
-static optional<name> import_decl(deserializer & d, environment & env) {
+static optional<name> import_decl(deserializer & d, environment & env,
+                                  std::vector<task_result<expr>> const & delayed_proofs) {
+    bool is_delayed; d >> is_delayed;
     declaration decl = read_declaration(d);
     decl = unfold_untrusted_macros(env, decl);
     if (decl.get_name() == get_sorry_name() && has_sorry(env)) {
         // TODO(gabriel): not sure why this is here
         return optional<name>();
     }
-    if (decl.is_theorem() && false) {  // TODO(gabriel): was proof already revealed?
-        decl = theorem2axiom(decl);
-        // TODO(gabriel): delay proofs
+    if (is_delayed) {
+        unsigned i; d >> i;
+        auto delayed_proof = delayed_proofs.at(i);
+        decl = mk_theorem(decl.get_name(), decl.get_univ_params(), decl.get_type(), delayed_proof);
     }
     env = import_helper::add_unchecked(env, decl);
     return optional<name>(decl.get_name());
@@ -443,7 +434,8 @@ static void import_universe(deserializer & d, environment & env) {
     env = env.add_universe(l);
 }
 
-void import_module(std::vector<char> const & olean_code, std::string const & file_name, environment & env) {
+void import_module(std::vector<char> const & olean_code, std::string const & file_name, environment & env,
+                   std::vector<task_result<expr>> const & delayed_proofs) {
     // TODO(gabriel): update extension
     std::string s(olean_code.data(), olean_code.size());
     std::istringstream in(s, std::ios_base::binary);
@@ -455,7 +447,7 @@ void import_module(std::vector<char> const & olean_code, std::string const & fil
         if (k == g_olean_end_file) {
             break;
         } else if (k == *g_decl_key) {
-            if (auto decl_name = import_decl(d, env))
+            if (auto decl_name = import_decl(d, env, delayed_proofs))
                 env = add_decl_olean(env, *decl_name, file_name);
         } else if (k == *g_glvl_key) {
             import_universe(d, env);
diff --git a/src/library/module.h b/src/library/module.h
index 756c28937c..f1d87acfad 100644
--- a/src/library/module.h
+++ b/src/library/module.h
@@ -30,7 +30,7 @@ struct module_name {
 struct loaded_module {
     std::string m_module_name;
     std::string m_obj_code;
-    name_map<task_result<expr>> m_delayed_proofs;
+    std::vector<task_result<expr>> m_delayed_proofs;
 };
 using module_loader = std::function<loaded_module(std::string const &, module_name const &)>;
 module_loader mk_olean_loader();
@@ -50,12 +50,6 @@ list<module_name> get_curr_module_imports(environment const & env);
     If \c keep_proofs is false, then the proof of the imported theorems is discarded after being
     checked. The idea is to save memory.
 */
-environment
-import_module(environment const & env,
-              std::string const & current_mod, module_name const & ref,
-              name_map<task_result<certified_declaration>> & del_thms,
-              module_loader const & mod_ldr);
-
 environment
 import_module(environment const & env,
               std::string const & current_mod, module_name const & ref,
@@ -74,10 +68,12 @@ environment add_transient_decl_pos_info(environment const & env, name const & de
 
 /** \brief Store/Export module using \c env to the output stream \c out. */
 void export_module(std::ostream & out, environment const & env);
+std::vector<task_result<expr>> export_module_delayed(std::ostream & out, environment const & env);
 
 std::pair<std::vector<module_name>, std::vector<char>> parse_olean(
         std::istream & in, std::string const & file_name, bool check_hash = true);
-void import_module(std::vector<char> const & olean_code, std::string const & file_name, environment & env);
+void import_module(std::vector<char> const & olean_code, std::string const & file_name, environment & env,
+                   std::vector<task_result<expr>> const & delayed_proofs);
 
 /** \brief A reader for importing data from a stream using deserializer \c d.
     There is one way to update the environment being constructed.
diff --git a/src/library/module_mgr.cpp b/src/library/module_mgr.cpp
index 54fbbed918..c8d0ef9aef 100644
--- a/src/library/module_mgr.cpp
+++ b/src/library/module_mgr.cpp
@@ -66,16 +66,10 @@ public:
                         std::get<1>(d).m_relative == import.m_relative) {
                     auto mod_info = std::get<2>(d);
 
-                    name_map<task_result<expr>> delayed_thms;
-                    mod_info.m_result.get().m_delayed_theorems.for_each(
-                            [&] (name const & thm_name, delayed_theorem const & del_thm) {
-                                if (!del_thm.m_imported) delayed_thms.insert(thm_name, del_thm.m_proof);
-                            });
-
                     return loaded_module {
                             mod_info.m_mod,
                             mod_info.m_result.get().m_obj_code,
-                            delayed_thms
+                            mod_info.m_result.get().m_obj_code_delayed_proofs,
                     };
                 }
             }
@@ -96,12 +90,12 @@ public:
 
         {
             std::ostringstream obj_code_buf(std::ios_base::binary);
-            export_module(obj_code_buf, p.env());
+            mod.m_obj_code_delayed_proofs =
+                    export_module_delayed(obj_code_buf, p.env());
             mod.m_obj_code = obj_code_buf.str();
         }
 
         mod.m_env = optional<environment>(p.env());
-        mod.m_delayed_theorems = p.get_delayed_theorems();
 
         mod.m_ok = parsed_ok; // TODO(gabriel): what should this be?
 
@@ -120,11 +114,9 @@ public:
     std::vector<generic_task_result> get_dependencies() override {
         if (auto res = m_mod.m_result.peek()) {
             std::vector<generic_task_result> deps;
-            res->m_delayed_theorems.for_each(
-                    [&] (name const &, delayed_theorem const & del_thm) {
-                        if (!del_thm.m_imported)
-                            deps.push_back(del_thm.m_cert_decl);
-                    });
+            res->m_env->for_each_declaration([&] (declaration const & d) {
+                if (d.is_theorem()) deps.push_back(d.get_value_task());
+            });
             return deps;
         } else {
             return {m_mod.m_result};
@@ -141,12 +133,6 @@ public:
         auto res = m_mod.m_result.get();
         auto env = *res.m_env;
 
-        res.m_delayed_theorems.for_each(
-                [&] (name const &, delayed_theorem const & del_thm) {
-                    if (!del_thm.m_imported)
-                        env = env.replace(del_thm.m_cert_decl.get());
-                });
-
         auto olean_fn = olean_of_lean(m_mod.m_mod);
         exclusive_file_lock output_lock(olean_fn);
         std::ofstream out(olean_fn, std::ios_base::binary);
diff --git a/src/library/module_mgr.h b/src/library/module_mgr.h
index 3c4fa6492a..ac716c0521 100644
--- a/src/library/module_mgr.h
+++ b/src/library/module_mgr.h
@@ -41,9 +41,11 @@ struct module_info {
 
     struct parse_result {
         optional<environment> m_env;
-        name_map<delayed_theorem> m_delayed_theorems;
-        std::string m_obj_code;
         bool m_ok = false;
+
+        std::string m_obj_code;
+        std::vector<task_result<expr>> m_obj_code_delayed_proofs;
+
         snapshot_vector m_snapshots;
     };
 
diff --git a/src/util/mt_task_queue.cpp b/src/util/mt_task_queue.cpp
index a96ce2ef23..8a7531f87a 100644
--- a/src/util/mt_task_queue.cpp
+++ b/src/util/mt_task_queue.cpp
@@ -205,8 +205,10 @@ void mt_task_queue::wait(generic_task_result const & t) {
             } else {
                 m_wake_up_worker.notify_one();
             }
+            t->m_task->m_has_finished.wait(lock);
+        } else {
+            t->m_task->m_has_finished.wait(lock);
         }
-        t->m_task->m_has_finished.wait(lock);
     }
     switch (t->m_state.load()) {
         case task_result_state::FAILED: std::rethrow_exception(t->m_ex);
diff --git a/src/util/task_queue.h b/src/util/task_queue.h
index adbd714441..541828d079 100644
--- a/src/util/task_queue.h
+++ b/src/util/task_queue.h
@@ -170,7 +170,7 @@ public:
     task_result<T> & operator=(task_result<T> const & t) { LEAN_COPY_REF(t); }
     task_result<T> & operator=(task_result<T> && t) { LEAN_MOVE_REF(t); }
 
-    T get() const;
+    T const & get() const;
 
     optional<T> peek() const {
         if (m_ptr->m_state.load() == task_result_state::FINISHED) {
@@ -219,7 +219,7 @@ public:
     }
 
     template <typename T>
-    T get_result(task_result<T> const & t) {
+    T const & get_result(task_result<T> const & t) {
         wait(t);
         lean_assert(t.get_ptr()->m_result);
         return *t.get_ptr()->m_result;
@@ -243,7 +243,7 @@ public:
 task_queue & get_global_task_queue();
 
 template <class T>
-T task_result<T>::get() const {
+T const & task_result<T>::get() const {
     return get_global_task_queue().get_result(*this);
 }
 
diff --git a/tests/lean/run/calc_heq_symm.lean b/tests/lean/run/calc_heq_symm.lean
index e6172a48e9..ab71da57e5 100644
--- a/tests/lean/run/calc_heq_symm.lean
+++ b/tests/lean/run/calc_heq_symm.lean
@@ -5,5 +5,4 @@ calc d  == c  : heq.symm H₃
     ... == a₂ : heq.symm H₁
     ... =  a₁ : eq.symm H₀
 
-reveal tst
 print definition tst
diff --git a/tests/lean/run/class2.lean b/tests/lean/run/class2.lean
index 11c764d7b5..e84b41b626 100644
--- a/tests/lean/run/class2.lean
+++ b/tests/lean/run/class2.lean
@@ -2,5 +2,4 @@ open tactic
 theorem H {A B : Type} (H1 : inhabited A) : inhabited (Prop × A × (B → num))
 := by apply_instance
 
-reveal H
 print H
diff --git a/tests/lean/run/class3.lean b/tests/lean/run/class3.lean
index ac7801fbdb..ac647a855d 100644
--- a/tests/lean/run/class3.lean
+++ b/tests/lean/run/class3.lean
@@ -10,5 +10,4 @@ section
 
 end
 
-reveal tst
 print tst