# Interaction with Formal Mathematical Documents in Isabelle/PIDE

## TL;DR

This paper reviews the development and capabilities of Isabelle/PIDE, a versatile IDE for formal and mathematical documents, highlighting its architecture, features, and evolution over ten years.

## Contribution

It provides a comprehensive overview of PIDE's document model, parallel evaluation, and asynchronous interaction, including insights into its successes, challenges, and future directions.

## Key findings

- PIDE supports parallel evaluation and asynchronous interaction.
- It has been the standard IDE for Isabelle for over a decade.
- The paper discusses successes, failures, and future plans for 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.