# Isabelle technology for the Archive of Formal Proofs with application to MMT

## TL;DR

This paper discusses the Isabelle technology underlying the Archive of Formal Proofs, highlighting improvements in scalability, performance, and integration, with applications like Isabelle/MMT converting proofs into semantic formats.

## Contribution

It provides an overview of Isabelle's architecture and recent enhancements, demonstrating its application to converting formal proofs into semantic representations.

## Key findings

- Enhanced Isabelle performance in AFP growth
- Introduction of prover session exports and headless PIDE
- Successful application to Isabelle/MMT for semantic conversion

## Abstract

This is an overview of the Isabelle technology behind the Archive of Formal Proofs (AFP). Interactive development and quasi-interactive build jobs impose significant demands of scalability on the logic (usually Isabelle/HOL), on Isabelle/ML for mathematical tool implementation, and on Isabelle/Scala for physical system integration --- all integrated in Isabelle/PIDE (the Prover IDE). Continuous growth of AFP has demanded continuous improvements of Isabelle performance. This is a report on the situation in Isabelle2019 (June 2019), with notable add-ons like prover session exports and headless PIDE for automated updates based on semantic information. An example application is Isabelle/MMT, which is able to turn all of Isabelle + AFP into OMDoc and RDF triples, but it is straight-forward to reuse the Isabelle technology for other applications.