Documentation and Formal Mathematics — Web Technology meets Proof Assistants

Carst Tankink

Promotor: prof.dr. J.H. Geuvers (RU)
Copromotor: dr. J.H. McKinna (RU)
Radboud Universiteit Nijmegen
Date: 17 December, 2013, 12:30
Thesis: PDF

Summary

This thesis describes work on a “Wiki for Formal Mathematics”, a web-based system that combines mathematics for proof assistants with informal descriptions of these mathematics in several ways:

• It describes how to create standalone pages for formal proofs by caching the proof assistant responses for easy and on-demand, but read-only, access by readers who might not have a proof assistant available or who do not want to wait for computations.
• Enriching the data structure used for stand-alone pages, we obtain an easy way for authors to reference formally defined ‘islands’ within proofs. The referenced islands are displayed inline when a reader visits the informal page.
• The data structure can be used to form the basis of a ‘modeless’ web editor that allows proof assistants and other tools to immediately calculate on document content, while being agnostic of the exact proof assistant providing feedback on the proof being written. The tools calculate their response as the user writes in the editor, that uses this to give additional information to the user.

The described techniques and workflows come together in a research prototype for the Wiki, which is evaluated through a use case of an existing formalization and its informal documentation: the formal proof of the Kepler conjecture (the Flyspeck project)