I will give an overview of the current state of ODE theory in Mathlib and a mirrored theory for integral curves on manifolds. I will share some insights from the ongoing formalisation of the smoothness theorem for flows of ODEs, as well as some exciting developments in AI-assisted autoformalisation and library management.