@InProceedings{2021BeautifulFormalizations,
author="De Lon, Adrian
and Koepke, Peter
and Lorenzen, Anton
and Marti, Adrian
and Schütz, Marcel
and Sturzenhecker, Erik",
editor="Kamareddine, Fairouz
and Sacerdoti Coen, Claudio",
title="Beautiful Formalizations in Isabelle/Naproche",
booktitle="Intelligent Computer Mathematics",
year="2021",
publisher="Springer International Publishing",
address="Cham",
pages="19--31",
abstract="We present short example formalizations of basic theorems from number theory, set theory, and lattice theory which ship with the new Naproche component in Isabelle 2021. The natural proof assistant Naproche accepts input texts in the mathematical controlled natural language ForTheL. Some ForTheL texts that proof-check in Naproche come close to ordinary mathematical writing. The formalization examples demonstrate the potential to write mathematics in a natural yet completely formal language and to delegate tedious organisatorial details and obvious proof steps to strong automated theorem proving so that mathematical ideas and the ``beauty'' of proofs become visible.",
isbn="978-3-030-81097-9"
}