Interactive mathematical documents: creation and presentation
Lionel Elie Mamane
Promotor: prof.dr. J.H. Geuvers (RU)
Copromotor: dr. J.H. McKinna (RU)
Radboud Universiteit Nijmegen
Date: 23 September, 2013, 10:30
Thesis: PDF
Summary
This dissertation focuses on how to write mathematics in a way which is more reliable (by the use of Proof Assistants) and more readable (by the use of methods proposed). My contribution is technology for authoring documents that contain pieces of mathematics checked by a computer proof checker. These pieces of mathematics thus have to be fully formal.
Many of the current systems for authoring formal mathematics, which we call proof assistants, have been designed exclusively with regard to the development of fully formal mathematics in isolation. In particular, they are not designed for the placement of formal mathematics within a document, nor the parallel development of a document and the formal mathematics within. My central thesis is:
In order to achieve satisfactory integration of formal mathematics into documents, proof assistants themselves have to be adapted:
- Proof assistants have to be adapted as concrete systems, in how they interact with the rest of the ecosystem.
- The formal systems commonly used as core of proof assistants give rise to a notion of proof (namely “derivation in that formal system”) that serves the purpose of integration of formal mathematics into documents poorly.
Chapters 3 and 4 relate efforts to integrate formal mathematics into documents, using then-current proof assistants without adaptations or new features designed specifically for integration of formal mathematics into documents. They then discuss the shortcomings of these efforts. Chapter 5 deals essentially with adaptations that concern the proof assistant as a concrete program, that is adaptations that do not concern the theoretical underpinnings of the proof assistant, but e.g. adaptations about how the proof assistant is implemented or how it communicates with its environment. We discuss other candidates for notion of proof that serves the purpose of integration of formal mathematics into documents well. Chapter 6 tries to devise a formal system whose notion of proof is closer to the notion of proof that is good for integration of formal mathematics into documents, by capturing intensional aspects of proofs.
Interactive Mathematical Documents
The proof assistants have by now reached a certain level of maturity and capacity. But they mostly deal only with formal proofs and not with proof explanations.
- proof explanation
- A proof explanation is a document that conveys an intuition, a high-level understanding of the proven result or of the proof itself, an explanation of the techniques used in the proof, an explanation of the significance of the result, … or several of the preceding. It may or may not be a formal or informal proof by itself.
This dissertation studies the placement of formal mathematics within the more general, not purely mathematical, context of a document, such as a proof explanation, as well as more generally an article, book or course notes that also contain historical, didactic or explanatory remarks, examples of real life applications, acknowledgements of support, etc. Such a document containing (not necessarily exclusively) mathematics is a mathematical document.
This work studies the modes of integration of computer-checked formal mathematics into its literary context. The full accomplishment of the 19th and early 20th century program of rigorisation of mathematics needs such an integration. A typical mathematical journal is primarily meant to be read by humans, not by machines. In the absence of a satisfying integration of computer-checked formal mathematics into its literary context, it is thus far less likely that the mathematics contained in an article published in a mathematical journal are computer checked.
From our consideration of mathematics done in a proof assistant, thus on a computer, it follows naturally that we consider documents that are digital. As the document is digital, it can be interactive, that is it not only presents static information in a static design to the user, but also reacts to the user’s actions. This work treats specifically the interaction with the formal mathematical parts of the document; that is it treats interactive mathematical documents.
While my implementation work was primarily done with the Coq proof assistant, and a significant part of the work lied in dealing with specifics of Coq, the general principles of my work are not intimately linked to details of the design of the theoretical underpinnings of Coq. My work can thus in principle be adapted to other proof assistants.