problems with text The main application of Nuprl for this continuing study will be in creating the interactive lessons linked to the formal library. This unique material will solve a number of problems common to any technical subject, and in the future others might considerably extend the scope of what is proposed here. Let us consider the problems of reading mathematical texts.
From having read over 300 mathematical books and teaching mathematical
subjects to over a thousand undergraduates I can document these universal
problems that make reading mathematics difficult. First, many textbooks make mistakes because proofs are not checked; consistent use of definitions is not enforced, not all facts are clearly stated. Indeed, every discrete mathematics book that we studied made such errors. Second, there are
the many omissions: justifications of steps are left out
inadvertently at key places, steps themselves are left out, whole
proofs are left out thinking sometimes that they are ``just like the
case proved'' when they are not, cases in a case analysis are
forgotten and so forth. Each omission can cost readers many hours of
struggling. Third are the location problems or ``access to
resources,'' when it is hard to find a key definition, a lemma is cited
by name but it is hard to find, some previous remark is cited but not
located, sometimes a chain of definitions or theorems leads beyond the
particular book. Fourth is the problem of ambiguity, a statement is
made with several interpretations, an expression can be interpreted in
different ways or some implicit parameter has been
omitted.
Motivation for proof steps is missing, so a reader can
imagine a simpler method to apply, but no explanation is given for
this choice.
These problems are more exasperating than a ``boring lecture'' because the educational process depends on a student digesting course material in peace and quiet, experimenting in a workspace that includes the assembled material of lecture notes, books and his or her own writing and computing.
problems with subgoaling One of the principles of learning studied using computerized tutors is that ``solving a problem involves decomposing that problem into a set of goals and subgoals'' [67][4][3]. Empirical studies have confirmed that interfaces to computerized tutoring systems which made explicit the goal structures were superior to those that did not [65]. The Nuprl proof editor was designed to decompose a goal into subgoals based on a problem solving method (a rule or a tactic) (see 1.4). This editor works across all domains formalized in Nuprl. It has proven to be especially effective in teaching induction.