Abstract or Additional Information
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.