Abstract

We discuss concepts and methods for creating expository texts that refer to formalized mathematics.