In theory, proof assistants are a useful tool for validating mathematical claims. We will use simplicial topology as a case study to look at what goes into formalizing mathematics from pen and paper to the digital world. This is based on previous work with Stefan Friedl focused on formalizing stellar subdivisions of simplicial complexes. I will present a few anecdotal stories from our project that demonstrate some of the challenges involved. Topics include (but are not limited to) what changes when we introduce types to topology, decidability and computational complexity concerns, and what to do when the proof is left as an exercise for the reader.