2025

• Reaping the Benefits of Modularization in Flexiformal Mathematics by GF-based AST Transformations; CICM 2025, Brasília, Brazil.
  Slides

  PDF
• Managing Naproche Formalizations with sTeX and FLAMS; NatFoM, CICM 2025, Brasília, Brazil.
  Slides

  PDF
  Abstract

  Naproche is a proof assistant that accepts formalizations written in LaTeX. This allows the source files of those formalizations on the one hand to be passed to Naproche to be checked for logical correctness (the "logical level") and on the other hand to be passed to a TeX engine to be rendered as, e.g., PDF or HTML (the "presentational level"). However, this poses the challenge that several language features a Naproche formalization can make use of must be specified both on the logical and the presentational level. Examples of such language features are:

  • referencing formal statements across formalizations;
  • reusing symbolic notations across formalizations;
  • including formalizations into each other.

  Whereas the features listed above are already supported on the logical level of Naproche, they are currently all lacking proper support on the presentational level.

  In this talk, we will present how sTeX [2] (a LaTeX package to create semantically annotated documents) can be integrated into the Naproche ecosystem to provide presentational support for all three language features from the above list.

  Moreover, we will demonstrate how FLAMS [1] (a framework for managing semantically annotated documents) can be integrated in the Naproche workflow to manage and facilitate the build process of both PDF and HTML presentations of formalizations – which is also currently lacking proper support in the Naproche ecosystem.

  ---

  • [1] https://github.com/FlexiFormal/FLAMS
  • [2] https://github.com/slatex/stex

2024

• Reusing Learning Objects via Theory Morphisms; CICM 2024, Montreal, Quebec, Canada.
  Slides

  PDF

2023

• Foundational Libraries in Naproche; NatFoM, CICM 2023, Cambridge, UK.
  Slides

  PDF
  Abstract

  The latest release of the natural language proof assistant Naproche [1], developed at the university of Bonn, Germany, which ships as a component of the current sTeX release [2,3] comprises new foundational libraries about set and number theory.

  The Naproche ("Natural Proof Checking") proof assistant is being developed for a high degree of naturalness of accepted proof texts, written in the controlled natural language ForTheL ("Formula Theory Language"). ForTheL is designed to approximate the mathematical vernacular, while at the same time being a completely formal language which allows its translation into formal logics [4]. Naproche has a built-in softly typed ontology that can be regarded as a weak fragment of Kelley–Morse set theory. While this ontology can quite flexibly be extended by a user, it does not provide a sufficient basis on its own to formalize sophisticated mathematics. To overcome this issue, Naproche also provides three foundational libraries about set and number theory on top of its built-in ontology [5]:

  1. One library that provides basic set-theoretical notions and operations as well as the most commonly used Kelley–Morse axioms [6].
  2. One that extends the first library with more advanced notions from set theory like that of ordinal and cardinal numbers [7].
  3. One that extends the first library with a new (soft) type of natural numbers together with common arithmetical operations as well as some basic notions of number theory [8].

  Since these libraries are written in a LaTeX dialect of ForTheL they not only comprise a high degree of human readability but can also be converted directly to PDF. Moreover, their applicability as practically usable foundations for more advanced formalizations in Naproche is demonstrated by using them as a basis for formalizations of some well-known theorems from set and number theory that ship with Naproche, e.g. the Cantor-Schroeder-Bernstein theorem [9,10] and Furstenberg's proof of the infinitude of primes [11,12]. However, they also pose some serious problems yet that have to be addressed in future versions of Naproche:

  1. Modularity: Since Naproche lacks a mature module system for organizing formalizations, their reusability is currently fairly limited.
  2. Scalability: The proof checking abilities of Naproche do not scale well with the size of the libraries.
  3. Time redundancy: Currently Naproche has no mechanisms to provide persistent certificates of the correctness of its libraries so they are rechecked by the system every time they are imported to a ForTheL document.
  4. Abstract mathematical structures: Naproche's current abilities of handling abstract mathematical structures (such as groups or topological spaces) in contrast to "concrete" ones like "the" universe of sets or "the" structure of natural numbers are very limited. This demands for an extension of ForTheL that can handle such abstract structures using language constructs that do not differ remarkably from the mathematical vernacular.

  Hence, although Naproche appears as a promising basis for dealing with human-readable, formal mathematical libraries, there is much room for further improvement of its capabilities using methods developed in the 'intelligent computer mathematics' community.

  ---

  • [1] https://github.com/naproche/naproche
  • [2] https://isabelle.in.tum.de/website-Isabelle2022/
  • [3] De Lon, A., Koepke, P., Lorenzen, A., Marti, A., Schütz, M., Wenzel, M. (2021). The Isabelle/Naproche Natural Language Proof Assistant. In: Platzer, A., Sutcliffe, G. (eds) Automated Deduction – CADE 28. CADE 2021. Lecture Notes in Computer Science, vol 12699. Springer, Cham. https://doi.org/10.1007/978-3-030-79876-5_36
  • [4] De Lon, A., Koepke, P., Lorenzen, A., Marti, A., Schütz, M., Sturzenhecker, E. (2021). Beautiful Formalizations in Isabelle/Naproche. In: Kamareddine, F., Sacerdoti Coen, C. (eds) Intelligent Computer Mathematics. CICM 2021. Lecture Notes in Computer Science, vol 12833. Springer, Cham. https://doi.org/10.1007/978-3-030-81097-9_2
  • [5] Schütz, M., De Lon, A., Koepke, P. (2022). Setting up Set-Theoretical Foundations in Naproche. In: Work-in-progress papers presented at the 15th Conference on Intelligent Computer Mathematics, CICM 2022 (Informal Proceedings). https://www3.risc.jku.at/publications/download/risc_6584/proceedings-CICM2022-informal.pdf
  • [6] https://github.com/naproche/naproche/tree/master/examples/foundations
  • [7] https://github.com/naproche/naproche/tree/master/examples/set-theory
  • [8] https://github.com/naproche/naproche/tree/master/examples/arithmetic
  • [9] https://github.com/naproche/naproche/blob/master/examples/zermelo.ftl.tex
  • [10] Schröder, B.S.W. The fixed point property for ordered sets. In: Arab. J. Math. 1, 529–547 (2012). https://doi.org/10.1007/s40065-012-0049-7
  • [11] https://github.com/naproche/naproche/blob/master/examples/furstenberg.ftl.tex
  • [12] Furstenberg, H. (1955). On the Infinitude of Primes. In: American Mathematical Monthly 62 (1955): 353.

• Theory Morphisms in Computer-Supported Education; Doctoral Symposium, CICM 2023, Cambridge, UK.
  Slides

  PDF
  Abstract

  In my PhD thesis I propose to explore the capabilities of using theory morphisms to improve adaptive learning systems. Thereby I aim to adresses the problem of handling interrelations between mathematical theories in automated processes for managing education material.