Selected formalization projects

Formalizations in Naproche are often carried out by students as part of a practical project or a thesis. On this page we present some of the larger formalizations projects in Naproche. Please note that some formalizations only run in the respective contemporary version of Naproche.

Selection of Wiedijk’s 100 theorems

In the summer semester of 2023 Peter Koepke, Mateusz Marcol, and Patrick Schäfer formalized some of Wiedijk’s 100 theorems and compiled them together with existing formalizations into a continuous document. The formalization is part of the examples that ship with Naproche in the Isabelle (September 2023) distribution. This work was presented at NatFoM 2023. You can also find the PDF version here and the LATEX source file here.

Initial chapters of Rudin’s Principles of Mathematical Analysis

In 2022 ten students formalized the first five chapters of Baby Rudin while staying as close to the original text as possible. The formalization is available here.

Set theory up to Silver’s theorem

In 2020 Jan Penquitt formalized set theory in Naproche up to Silver’s theorem about the continuum function at singular cardinals of uncountable cofinality. This formalization was also presented at the NatFoM workshop during CICM 2020.

Linear algebra and representation theory

In 2020 Erik Sturzenhecker formalized linear algebra and representation theory in Naproche.