Interaction with Formal Mathematical Documents in Isabelle/PIDE
Abstract
Isabelle/PIDE has emerged over more than 10 years as the standard Prover IDE for interactive theorem proving in Isabelle. The well-established Archive of Formal Proofs (AFP) testifies the success of such applications of formalized mathematics in Isabelle/HOL. More recently, the scope of PIDE has widened towards languages that are not connected to logic and proof in Isabelle, but taken from a broader repertoire of mathematics on the computer. The present paper provides a general overview of the PIDE project and its underlying document model, with built-in parallel evaluation and asynchronous interaction. There is also some discussion of original aims and approaches, successes and failures, later changes to the plan, and ideas for the future.
Keywords
Cite
@article{arxiv.1905.01735,
title = {Interaction with Formal Mathematical Documents in Isabelle/PIDE},
author = {Makarius Wenzel},
journal= {arXiv preprint arXiv:1905.01735},
year = {2019}
}