PROVERB is a system presenting machine-found proofs in natural language. It is embedded in the interactive proof development environment OMEGA. Settled between automated theorem proving (ATP) and natural language generation (NLG), PROVERB uses techniques of both these fields. In order to present proofs in a way as they can be found in mathematical textbooks, PROVERB first transforms and abstracts resolution proofs or natural deduction proofs to so-called assertion level proofs, which abstract from the basic calculus inference rules. Here, most justifications are in terms of the application of a definition, a lemma, or a theorem, which are collectively called assertions. Assertion level proofs are then verbalized in English using NLG techniques. First, a macroplanner determines the order and content of the information to be conveyed. Then, a microplanner plans the internal structure of the paragraphs and sentences. Finally, the surface sentences are produced by the system TAG-GEN. Furthermore, PROVERB allows for the automatic creation of a LaTeX document from the English proof.