What do we learn by formalizing differential topology?

Differential topology is known to sometimes rely on geometrical or topological intuitions that seem pretty far from the level of precision required when explaining mathematics to a computer. For this reason, I chose to explain enough differential topology to computers to prove a famous surprising geometrical construction: you can turn a sphere inside out. In this talk I will explain what kind of abstractions and lemmas were useful to bridge the gap between intuition and formal proofs. This is joint work with Floris van Doorn and Oliver Nash.