In the 1970s van Benthem Jutting translated Landau’s book Grundlagen der Analysis into Automath. The type theory of Automath differs from modern type theories in significant ways. The most important difference is that Automath is λ-typed while most modern type theories are Π-typed. In this paper we define the notion of a faithful reproduction of an Automath signature. We describe how one can obtain a particular faithful reproduction of a signature corresponding to the Automath version of Landau’s book. We then consider what properties a Π-typed type theory must have in order for the faithful reproduction to be a correct signature. Based on this information, we can give different mappings of the reproduction into type theories such as ECC and, in particular, the system Coq.