When formalizing a mathematical development with an interactive prover, it is helpful if the user can interface with a library (to avoid starting from scratch) and with automated provers (to avoid needing to give full details explicitly). We will consider an example of a development in Mizar, leading to some discussion of how one can interact with Mizar’s library and how automated theorem provers can help construct Mizar proofs. With this example in mind, we discuss criteria for three aspects of formalization to work in harmony: formal mathematical developments, working with a global library of theorems and denitions and making use of automation.