natural isabelle

For the past year at the mathematical logic group of Bonn, I’ve been learning a lot about formal mathematics, and in particular, developing ideas with Peter Koepke to strengthen formal mathematics here in Bonn, and to expand on the developments concerning (controlled) natural language proof checking made during the Naproche project.

Last May we started, together with Peter Koepke and Regula Krapf, a voluntary formal mathematics work group, where we looked at the proof assistant Isabelle, and the student turn out was with 12 students  very motivating indeed! Six of them gave detailed presentations and six of them joined another five bachelor’s students for this semester’s internship in mathematical Logic,  under the title
“Natural Isabelle”.

In this project we are looking at Isabelle-formalised proofs and theory files, starting with the beginnings of set theory, rewriting them in the language Isar (Intelligible Semi-Automatic Reasoning) with an eye toward naturalising them, and we plan to write parsers in OCaml from a controlled natural language for mathematical proofs to the Isar language. I am personally delighted at the amount of interest this project has generated, and I can only say,

stay tuned for upcoming naturalised formal proofs!

The featured image is taken from the Isabelle website.