The Isabelle/Naproche Natural Language Proof Assistant
Adrian De Lon, Peter Koepke, Anton Lorenzen, Adrian Marti, Marcel Schütz, Makarius Wenzel · Lecture notes in computer science · 2021
Abstract "Image missing" is an emerging natural proof assistant that accepts input in the controlled natural language ForTheL. "Image missing" is included in the current version of the Isabelle/PIDE which allows comfortable editing and asynchronous proof-checking of ForTheL texts. The dialect of ForTheL can be typeset by "Image missing" into documents that approximate the language and appearance of ordinary mathematical texts.