I will be concerned with the optimal distribution of points on the n-dimensional unit sphere. Here optimal means that the points should be as far apart as possible. I will give a computer assisted proof that a distribution of 10 points on the three-dimensional sphere which is connected to the Petersen graph is optimal. One aspect I want to highlight is how to transform numerical, inaccurate computer results into a rigorous proof which one can verify and understand without computer.

Joint work with Christine Bachoc, http://arxiv.org/abs/0708.3947