“Hilbert and Isabelle” in Spektrum der Wissenschaft (March 2019)

The current print edition of Spektrum der Wissenschaft 3.19 includes an article Mathematische Unterhaltungen: Hilbert und Isabelle (by Christoph Pöppe, in German). It recounts the prize-winning project by a group of young students from Bremen, with many explanations about the overall problem and the approach in formalization.

This project is notable as an ambitious proof formalization by genuine end-users of Isabelle, without any previous connections to the providers of the tool. Only after the first public appearance, I have occasionally had a chat with some of the authors, either personally or via email; likewise some of my colleagues.