What is ForTheL?

This page contains a complete reference for the syntax of ForTheL. ForTheL (Formula Theory Language) is a controlled natural language for writing mathematical texts. It is the input language of the proof assistant Naproche which is currently developed at the University of Bonn, Germany, and since 2021 a component of the Isabelle prover platform. ForTheL comes in two variants: It has an ASCII dialect (FTL), which is the original plain text format of ForTheL, and a LaTeX dialect (TEX), which is an integration of ForTheL into LaTeX which allows to convert ForTheL texts easily to PDF. Check out their references via the links below.

ForTheL's ASCII dialect

A complete reference of the syntax of ForTheL's ASCII dialect:

FTL

ForTheL's LaTeX dialect

A complete reference of the syntax of ForTheL's LaTeX dialect:

TEX

Repository

The sources of the references, hosted on GitHub:

Repository

Changelog

A complete listing of all changes on ForTheL since the integration of Naproche into Isabelle:

Changelog