This proposal is currently under review.
Due to the increasing use of complex hardware and software, formal methods are becoming more and more important for industry. A long term goal of this project is to bring formal methods into the mainstream of science and engineering. For formal methods to become widely used, there must be users, i.e. a culture of formal reasoning. People who have used formally based methods and tools in their university courses will be much more open to using such methods in their later work.
To encourage such a culture of formal reasoning we propose to begin a long term project to develop formal presentation of some interesting university level mathematics. This might be done by formalising some existing texts and/or by developing new syllabus material.
Experience of using formal proof systems in undergraduate education is limited, mostly to deductions in logic. We are proposing to present conventional mathematical subjects in a formal, machine checked, but still careful and explanatory manner. Students will be able to browse the formal definitions and proofs at a level of detail they choose, and will work their exercises using the formal proof tool.
It is clear that such a project must be built on significant advances in how to present formal mathematics: the language of textbooks and journals in mathematics and computing science is much more flexible and extensible than any official foundational logic. It is essential to capture some of this richness in formal methods if their use is to become common. Conversely, large scale experience in presenting real university level mathematics in a coherent way for educational use is excellent feedback for research on making the systems as user-friendly as possible.
We are rapidly moving towards an information society which will change both how and what we teach our students. In mathematics there is already a trend towards computations, but we expect a more radical change: a renaissance of proof in education. For the first time, the art of making proofs is on its way to become an engineering discipline because of the fundamental importance of correct hardware and software. For undergraduate students it is difficult to understand the rules by which proofs are made and even more difficult for them to develop their own proofs. The fulfilment of this project will give powerful tools to increase students' understanding of what a proof is and how to develop proofs.
As a starting point, we intend to use the interactive theorem provers Agda, Coq and LEGO. All of them are based on variations of Martin-L"of type theory. They have been used on a number of non-trivial large examples in programming, logic and computational algebra, but only by people with great knowledge both of the mathematics involved and the systems. An essential property of these systems, especially relevant for this project, is that they have explicit proof objects: it is possible to present proofs at various levels of detail, and the users can choose what to see. The systems are very flexible and theories based on classical as well as constructive logic can be expressed in them; we expect to use both approaches. Constructive logic is particularly suitable in some applications in computing science since proofs then have computational content: the proof objects can be seen as functional programs and can be directly evaluated in the systems.
The areas of mathematics we are considering include elementary algebra and various topics in discrete mathematics; at a later stage we want to develop elementary analysis. We also want to consider mathematics more specifically used in computing science, like automata theory, domain theory, and computational algebra; our systems are well suited for this because of their close connection to typed functional programming languages.
We are already using the systems in undergraduate teaching of formal logic. For instance, Agda has a window interface Alfa in which natural deduction can be expressed; it is used in big undergraduate courses. Other more informal parts of mathematics are usually much harder to develop on the computer; the experience we have of teaching in such areas is restricted to rather small examples, but is nevertheless very encouraging.
Part of this project involves investigating some basic and technical issues before any more extensive formalisation to be used in education is made. For instance, what notion of equality should be used? What notion of subtype should be used? Experimentation with different approaches is a necessary complement to theoretical investigations. This study will enable careful development of a library of the basics underlying university mathematics. Such a library can become the root of the large body of basic and more specialised topics that must exist in usable libraries before large scale use of formal mathematics becomes feasible. However, some parts of discrete mathematics can certainly be developed without any extensive libraries; hence, we expect to develop a shorter course in this area rather early in the project. Also, work has already started on using Coq in an elementary algebra course. We will work on the interfaces to make them easy to use for students. The proofs should be in a form that is as close as possible, in presentation, to proofs in a readable textbook. It is not clear if it is possible to use the same interface for the different areas of mathematics or if we have to use domain specific proof editors. There are already interfaces to the type theory systems, which translate proofs to natural language; we expect them to be very useful in education.
There are different possible deliverables, ranging from some smaller courses on specific subjects to a full scale implementation which can be used by almost any university teacher in an undergraduate curriculum in mathematics and computing science.