I first survey recent progress in mechanistic interpretability of artificial neural networks, focusing on how symmetry and geometric structure emerge because they help with generalization. I then discuss how recent progress in AI-powered formal verification can help with the ultimate interpretability challenge: enabling neural-network-based AI systems to self-export their machine-learned algorithms and knowledge into formally verified code – much like a human can export the algorithms and knowledge learned by the biological neural network in their brain.