Two masses attracting each other through gravity — the Sun and a single planet — is a problem Newton solved completely in 1687. The orbits are conic sections: ellipses, parabolas, or hyperbolas. The solution is explicit, exact, and beautiful.
Add a third mass, and everything breaks.
The gravitational three-body problem asks: given three masses with known positions and velocities at some instant, predict their motion for all future time. Despite more than 300 years of effort by the greatest mathematicians in history, no general closed-form solution exists.
The equations are deceptively simple: each body accelerates toward the other two, inversely proportional to the square of the distance. The two-body version has 10 conserved quantities (energy, momentum, angular momentum, Laplace-Runge-Lenz vector) that make it exactly solvable. The three-body problem has only 10 as well — but now there are 18 degrees of freedom instead of 12. The system is not integrable: there are not enough conservation laws to pin down the motion.
The two-body problem is integrable: the relative motion reduces to a single body in a central potential, and Kepler's laws give the complete solution. With three bodies, the relative distances $r_{12}$, $r_{13}$, $r_{23}$ are coupled — changing one affects the other two. The resulting dynamics is chaotic: tiny changes in initial conditions lead to vastly different trajectories.
Poincaré proved in 1890 that the three-body problem has no analytic first integral beyond the classical ones (energy, momentum, angular momentum). This means there is no formula, however complicated, that gives the positions as explicit functions of time for general initial conditions.
When two bodies collide ($r_{ij} \to 0$), the force diverges and the equations break down. Painlevé proved in 1897 that for three bodies, these collisions are the only singularities — if no collision occurs, the solution extends smoothly. Sundman then proved in 1912 that even collisions can be regularized, giving a convergent power series valid for all time — but the series converges so slowly (~$10^{10^8}$ terms) that it is useless in practice.
The three-body problem is the simplest problem in physics that cannot be solved exactly, and the birthplace of the mathematical theory of chaos.
The three-body problem is not an academic curiosity. It appears everywhere that gravity operates — which is to say, everywhere in the universe.
Every space mission beyond Earth orbit is a three-body problem (or worse). The trajectories of spacecraft near Lagrange points (like the James Webb Space Telescope at L2) are governed by the Sun-Earth-spacecraft three-body dynamics. Low-energy transfer orbits exploit three-body chaos to reach destinations with minimal fuel.
Most stars in the galaxy are in binary or triple systems. Understanding the long-term stability of planetary orbits in multi-star systems — whether habitable planets can survive — requires solving variants of the three-body problem. The Kozai-Lidov mechanism, a purely three-body effect, explains the existence of hot Jupiters and influences the merger rate of compact binaries.
Three-body interactions in dense star clusters produce the merging black hole binaries detected by LIGO. The rate and properties of these mergers depend on three-body scattering cross sections — a computational three-body problem at its core.
Poincaré's study of the three-body problem in the 1890s led directly to the discovery of sensitive dependence on initial conditions, homoclinic orbits, and the foundations of what we now call chaos theory and dynamical systems. The three-body problem is not just a problem in celestial mechanics — it is the origin story of an entire branch of mathematics.
In 1998, Stephen Smale listed 18 problems for the 21st century. Problem 6 asks: Is the number of relative equilibria (central configurations) of the $N$-body problem always finite? For $N = 3$, finiteness is known (Euler and Lagrange found all five). For general $N$, this remains one of the major open problems in mathematical dynamics.
Newton solves the two-body problem. The Principia gives the complete solution for two gravitating bodies. Newton attempts the three-body Sun-Earth-Moon system but cannot find a general solution.
Euler's collinear solutions. Three special configurations where all three bodies lie on a line and rotate rigidly.
Lagrange's equilateral solutions. Two configurations where the three bodies form an equilateral triangle and rotate rigidly. Together with Euler's, these are all five central configurations for $N = 3$.
Poincaré and the birth of chaos. In his prize-winning memoir, Poincaré proves the three-body problem has no analytic integral beyond the classical ones. He discovers homoclinic orbits and sensitive dependence on initial conditions — the mathematical foundations of chaos theory.
Painlevé's theorem. The only singularities of the three-body problem are collisions. No "pseudocollisions" (bodies escaping to infinity in finite time) can occur for $N = 3$.
Sundman's convergent series. A power series solution valid for all time, regularizing collisions via a time transformation. Theoretically complete but practically useless: convergence requires ~$10^{10^8}$ terms.
Levi-Civita regularization. A coordinate transformation that removes the collision singularity, making the flow smooth through binary collisions. The foundation of all modern regularization techniques.
Non-collision singularities exist. Xia constructs a 5-body configuration where bodies escape to infinity in finite time without any collision. Painlevé's theorem fails for $N \geq 5$. The case $N = 4$ remains open.
The figure-eight choreography. Chenciner and Montgomery prove the existence of a remarkable periodic orbit where three equal masses chase each other along a figure-eight curve. The first new qualitative solution in over a century.
Thousands of new orbits. Šuvakov and Dmitrašinović discover over 1,000 new periodic three-body orbits by systematic numerical search, classified by topological type (braid word).
Marchal's conjecture proved. The figure-eight choreography belongs to the continuation family of the Lagrange equilateral solution, settling a 25-year-old conjecture.
10,000+ new 3D orbits. Systematic computation discovers 10,059 new three-dimensional periodic orbits, including 21 choreographies and 273 "piano-trio" orbits. About 20% are linearly stable.
The three-body problem is experiencing a renaissance. Computational power has revealed tens of thousands of periodic orbits. Topological methods classify solutions by their braid type. Variational techniques prove existence of new orbit families. And the fundamental question — a practical, exact representation of the general solution — remains open.
Periodic orbits. Computational search has exploded the catalog from Euler and Lagrange's five solutions (1767–1772) to over 10,000 known periodic orbits. These are classified by topological braid type and symmetry group. The existence of each orbit family can often be proved rigorously using variational methods.
Practical computation. Modern $N$-body integrators (Hermite, Bulirsch-Stoer, ARCHAIN) can track three-body trajectories to high precision for long times. But these are numerical solutions — they give numbers, not structure. The question of an exact, finite, practical representation remains open.
Smale's 6th Problem. The finiteness of central configurations for general $N$ is still unresolved. For $N = 4$, finiteness was proved by Hampton and Moeckel (2006). For $N = 5$, it remains one of the hardest open problems in algebraic celestial mechanics.
Formal verification. No prior project has formalized any substantial result about the three-body problem in a proof assistant. The closest work is formalization of basic ODE theory (Picard-Lindelöf) in Isabelle and Lean.
We have constructed an exact, finite, practical representation of the gravitational three-body problem — and extended it to general $N$. The representation is formalized in Lean 4 and published with priority timestamps.
The key idea: Newton's equations, projected onto Fourier modes (Galerkin method), become an algebraic system whose solution depends analytically on initial conditions. This gives a generating function $G(z; \mathbf{v}_0)$ that encodes the entire orbit family in finitely many coefficients:
The coefficients $\boldsymbol{\Lambda}_n$ are the Latent — a finite set of numbers that exactly encodes the trajectory. Padé resummation of the generating function gives geometric convergence: the error decreases exponentially with the number of coefficients.
Lean 4 kernel: 15 files in the NBody domain covering Galerkin
equations, virial theorem, Nekhoroshev stability, grade bounds, CC finiteness
(Smale's 6th for $N = 3$), cluster analysis, and scattering density.
NBodyVirial & NBodyNekhoroshev: Quality Level 1 (publication-ready).
Zero axioms, zero sorry, 55–65% A-grade theorems.
Smale6CCFiniteness: CC finiteness for $N = 3$ formalized.
Active work on extending to general $N$.
Correspondence: Active mathematical correspondence with
Richard Montgomery (UC Santa Cruz), co-discoverer of the figure-eight choreography
and one of the foremost experts on the three-body problem.
Sundman proved in 1912 that a convergent series solution exists — but with $\sim 10^{10^8}$ terms, it's a theoretical curiosity. Modern numerical integrators give approximate orbits but no structural insight. Our representation is both exact (it converges to the true solution) and finite (a fixed number of coefficients to any desired accuracy). This is possible because Padé approximation exploits the analyticity of the generating function, converting Sundman's slow power series into a rapidly converging rational form.
The practical consequence: a three-body orbit to 6-digit accuracy requires ~72 real numbers. Not a formula. Not an infinite series. A finite object you can store, transmit, and manipulate — the way we store images with JPEG or audio with MP3, but for gravitational dynamics.