A choreography for an N-particle mechanical system is a periodic orbit of the N bodies which traces out a single closed curve in physical, three-dimensional space. The first choreographies for the gravitational 3 body problem were discovered by Lagrange. Here, three equal masses move around a common circle in the plane and at each instant the locations of the masses describe an equilateral triangle. Many additional choreographies were discovered in the 20th century through numerical simulations. The first, and perhaps the most famous is the figure eight of Moore, Chenciner, and Montgomery. When this remarkable orbit was discovered Marchal conjectured, based on symmetry considerations, that it must be in the continuation class of the equilateral triangle of Lagrange. Despite much theoretical progress, and many detailed numerical studies, a complete proof of the correctness of the conjecture has appeared only recently. After reviewing the problem and some of its history, I will discuss a proof of Marchal's conjecture which makes substantial use of the digital computer. The proof is constructive and based exploits standard tools from nonlinear analysis. In the end, the role of the computer is to produce a good enough approximation of the branch of choreographies and to check certain inequalities needed for the a-posteriori analysis. This is joint work with Renato Calleja, Carlos Garcia-Azpeitia, Olivier Henot, and J.P. Lessard.