The Songling system has exactly four limit cycles

Determining how many limit cycles a planar polynomial system of differential equations can have is a remarkably hard problem. One of the main difficulties is that the limit cycles can reside within areas of vastly different scales. This makes numerical explorations very hard to perform, requiring high precision computations, where the necessary precision is not known in advance. Using rigorous computations, we can dynamically determine the required precision, and localize all limit cycles of a given system. We prove that the Songling system of planar, quadratic polynomial differential equations has exactly four limit cycles. Furthermore, we give precise bounds for the positions of these limit cycles using rigorous computational methods based on interval arithmetic. The techniques presented here are applicable to the much wider class of real-analytic planar differential equations.