One thing that quickly becomes clear when attempting to formalize recent mathematical discoveries in a computer proof assistant is how much "invisible mathematics" is obscured in a proof on paper. This talk will attempt to present a taxonomy of the various forms of invisible mathematics that have been made visible by attempts to formalize higher category theory. We then describe specific challenges inherent to large-scale formalization projects that are exacerbated by invisible mathematics.