KAM tori for the planetary N-body problem with actual masses
In plain words
KAM theory proves that planetary systems have many stable quasi-periodic orbits, but only for planets far lighter than real ones. Proving the same with the actual masses of Jupiter and Saturn is open.
Precise statement
Planetary N-body problem (Sun plus planets with mass ratios $\mu$). Arnold (1963) and Fejoz (2004) proved positive-measure sets of KAM tori for $\mu$ below an unspecified tiny threshold. Prove existence of invariant tori near the observed orbits for the actual $\mu \sim 10^{-3}$ of the Sun-Jupiter-Saturn system, for example by computer-assisted KAM. Answer: a proof.
What would settle it
A computer-assisted KAM proof for the full (non-truncated) planar or spatial Sun-Jupiter-Saturn problem with real parameters.
Status in the literature
Unverified note
Computer-assisted KAM has been done for truncated secular models of Sun-Jupiter-Saturn (Locatelli and Giorgilli, 2000s); Capinski and Gidea (arXiv 2504.09273, 2025) gave a computer-assisted proof of Arnold diffusion in the planar full three-body problem.