I will present a formalization of the conjecture that every surprising computational phenomenon has a good explanation. I will then discuss preliminary work aimed at explaining the behavior of simple computational systems and draw on historical experience in mathematics to argue that explanations might not only always exist but also be efficiently discoverable. Finally, I will argue that finding explanations for complex behaviors in neural networks would be a major advance in AI alignment and one of the most important contributions mathematics could make to AI safety.