Naproche-SAD is a recent tool by Frerix and Koepke, based on the original *System for Automated Deduction* (SAD) by Paskevich and others. It processes the *Formal Theory Language* (ForTheL), which is designed to look like mathematical text, but it is restricted to a small subset of natural language.

The tool is implemented in Haskell as a plain function from input text to output messages. A file is like a chapter of mathematical text, with a nested tree-structure of elements and sub-elements (for signatures, axiomatizations, statements, proofs). Output messages inform about the translation of mathematical text to problems of first-order logic, and indicate success or failure of external proof checking; the latter is delegated to the *E Prover* by Stephan Schulz and can take several seconds for each proof obligation.

To integrate Naproche-SAD into PIDE, Frerix and Wenzel have reworked the Haskell program over 2 months in 2018, to turn the command-line tool into a service for reactive checking of ForTheL texts. Isabelle integration was done via the new Isabelle/Haskell library and some glue code in Isabelle/Scala to register ForTheL as auxiliary file-format (extension `.ftl`

).

The resulting Isabelle/Naproche application is available as multi-platform download. A running instance is shown in the screenshot: users can directly open ForTheL files (e.g. from `Documentation`

/ `Examples`

) and wait briefly to see output messages attached to the text in the usual IDE manner. Further edits produce a new version of the text, which is sent in total to Naproche-SAD again. The back-end is sufficiently smart to avoid redundant checking of unchanged sub-elements: it keeps a global state with results of old versions: this is easy to implement as the program keeps running until shutdown of Isabelle/PIDE.

(Cited from section 1.2 of the paper Interaction with Formal Mathematical Documents in Isabelle/PIDE.)