Brief Overview

goals and background The heart of the Interactive Formal Courseware Project is a plan to explore the value of formally-grounded explanation in improving students' understanding of mathematics, especially of computational discrete mathematics. By a formally-grounded explanation we mean one that ultimately can be reduced to a readable machine checked proof in a formal logic. The entire project rests on the results of over twenty-five years of research that produced a new generation of reasoning tools such as Nuprl (and other similar systems under construction worldwide [61][53][43][25][60]). Later (in section 3) we will briefly describe this research, but for the moment let us accept that these tools enable us to produce formal definitions, theorems and proofs covering most of the subjects taught in college level discrete mathematics. Let us also assume that this formal material can be read and understood by mathematically educated first and second-year college students in a large number of the nation's 2,000 four-year colleges and universities. The reader will be able to judge these matters by reading the proposal.

pedagogical issues What is the educational value of formally-grounded explanation, and what known pedagogical problems does it solve? The brief answer to the first question is that this novel courseware opens significant new opportunities for using computers in education, especially for bringing mature research software into learning via the Web. The brief answer to the second question is that we already have shown from experience with the first versions of this material that it solves known problems with traditional mathematical texts, that it helps overcome documented difficulties teaching mathematical problem solving, and that the specific courseware we are creating reinforces ties between mathematics and computing that are known to help teach the basic concepts of function, induction and proof that are fundamental and yet problematic to teach. The proposal takes up these answers in detail in section 4, here I elaborate on them briefly.

First let us consider the new opportunities. Notice that because explanation is so fundamental to education, every potential advantage in teaching it is heavily weighted. Whether we are talking about an English essay, a chemistry experiment, a legal argument or a mathematical demonstration, college students are taught to answer the question ``How do you know?'' They are taught to give evidence and to say what statements follow from others. This ability to provide evidence and evaluate arguments is critical to a liberal arts education or an engineering one.

The added value of formal explanation is that it can be manipulated by machines as well as people, it can be automatically linked to semantically related material, and it can be related to a foundational account of mathematics and computing. These are enormous advantages as will be clearer when we illustrate them in section 2. Computers help create these explanations and check them for errors and omissions, but they can perform numerous other functions for us-showing exactly what other concepts a given concept depends on, ``what depends on what'', and finding semantically related concepts.

The underlying foundation is also very significant [74][35][19], especially for connecting computing and mathematics. In programming, students understand that meaning is ultimately given in terms of simple computational procedures that people and machines follow in essentially the same way. This ``semantic agreement'' is the basis of all mathematical properties of programs from speed to correctness. This agreement then is the foundation of knowledge about programs, and it can be used to help teach about functions in mathematics.

The semantic paradigm for programming extends in principle to computational mathematics as well. For example, we can explain that numerical expressions, and are equal, , when both compute to the same number.

The second question of this section is what pedagogical problems the formally-grounded courseware solves. The answer will be clearer after we have examined the formal reference material more closely, but consider first the issue of standard mathematics textbooks. Most of them do not bear careful logical scrutiny, at best they contain small but annoying errors, at worst they contain major conceptual errors. Even the best of them suffer from errors and omissions of detail that students waste countless hours puzzling over. Reference books and textbooks alike exhibit the problem of locating key information, such as definitions, notations or theorems. Good texts have large indexes, but even they are tedious to use and often fail. The problem of missing motivation to proof steps leaves readers to wonder why a simpler justification they have in mind is inadequate. The courseware we produce alleviates these problems.

Studies [1] have shown that students have difficulty understanding the goal and subgoal structure in solutions to problems, especially those solutions given by induction. This is also clear from books dvoted entirely to proof [69][77][26] and studies in logic [39][51][65]. The proof structure we adopt is excellent for alleviating this difficulty as we show. Finally, we have already noted that relating functional programs to mathematical functions is known to help with the problem of teaching functions [1][42]. Our reference material is especially suited to relating computational and mathematical concepts, and we exploit this capability in our lessons.

technical experience Since 1975 we have been building proof development systems - computer systems that help people create formal proofs. The latest version is Nuprl 4. These have been built largely with NSF funding, and they are available without charge. Nuprl is essentially the first major theorem prover to treat proofs as mathematical objects; proofs are central to the system architecture, to the underlying logic, and to the proposal.

Nuprl is a successful research tool which has been used to generate libraries of highly readable formal mathematics in a variety of subjects [33][63]. Our research group at Cornell has extensive experience with this medium for communicating technical ideas. Nuprl has been used for hardware verification [48], for programming language semantics and as a programming logic [21][45][22], for supporting symbolic algebra [46], for building components of theorem provers [23], and for manipulating communication protocols.

We taught formal mathematics using Nuprl in three advanced courses. The idea was that the Nuprl libraries were the underlying reference material for the course. Out of this experience came the idea for formally-grounded courseware at the heart of this project.

obstacles to formalization overcome As a consequence of our technical accomplishments, we have overcome a number of commonly recognized obstacles to the use of formalisms to naturally express and teach mathematics.

• The use of normal-looking, flexible notations supports our habits of thought, which could be rendered ineffective by the need to mentally translate back from a clumsy formal notation (see section 2.2).

• The capacity to suppress detail in expressions is key to simplifying our reading of them. This is really a corollary to the previous point, since examination of the informal notations we use reveals a lot of elision.

• Formalization need not be complete to be useful, and indeed, formal and informal expressions can be mixed.

1. The level of detail at which students interact with the material is flexible, from high level summaries and guided readings down to an examination of every detail and every lemma required for a proof. We can collect information about how students use the system and gain quantifiable insights into learning behavior.

   Often students are frustrated because a step in an argument that was trivial to the author is not clear to them or because some critical fact was left implicit. Since these proofs are complete, all the details are present, but on demand.

2. Providing multiple readings of a proof or a library section allows the instructional staff to offer many different approaches to the same idea. So there are diverse entry points to match a diverse student body. Using CoNotes, students will be able to contribute their own commentary directly in the library or can annotate those we provide. This personalizes the course material and encourages collaborative learning.

3. The mechanisms of a tactic-style prover allow us to teach problem solving technique. The vocabulary of goals, subgoals, rules, tactics, and lemmas enables us to discretize and quantify some of the learning [66]. This discovery of tactics [34] and their refinement to tactic-tree proofs is not only a major advance in formal methods, it may also be a major contribution to pedagogy, as we intend to examine further.

4. Since Nuprl's formal language can express virtually any mathematical concept, we can begin to teach understanding as a process of making connections between topics. As we make accessible our research libraries through lessons, we will be able to relate such ideas as induction and recursion, algebraic structures and program modules, graphs and relations, etc. In addition to the connections mentioned with existing libraries, we could relate Boolean rings, the propositional calculus, digital circuits, monoids and polynomial rings.

impact and significance We know from direct experience and from the literature [40][39][73] that some of the fundamental concepts in mathematics, such as function, induction and proof are difficult to teach. These concepts are central in both continuous and discrete mathematics, and the function concept seems to be critical in understanding abstraction. These concepts are basic to the language of modern science and engineering. They are as important in computer science as they are in physics. Improvements in education of the kind we suggest will help the U.S. retain its technical leadership and may help open the sciences and engineering to a wider segment of the population.

The computer-aided instruction (CAI) tools now available are mainly limited to first order logic, algebra, and geometry in isolation and deal principally with techniques [5][3][11]. We propose a way to enhance deep understanding as well as technique and factual knowledge.