Invariant tori in the Sun-Jupiter Saturn system

We discuss the applicability of Kolmogorov’s theorem on existence of invariant tori to the real Sun–Jupiter–Saturn system. Using computer algebra, we construct a Kolmogorov’s normal form defined in a neighborhood of the actual orbit in the phase space, giving a sharp evidence of the convergence of the algorithm. If not a rigorous proof, we consider our calculation as a strong indication that Kolmogorov’s theorem applies to the motion of the two biggest planets of our solar system.