Alles beginnt im Jahr 1611. Damals vermutet Johannes Kepler, Kugeln staple man am platzsparendsten in Pyramidenform. 1998 legt der US-Amerikaner Hales den Beweis vor. Darin zeigt er: Die kubisch flächenzentrierte Kugelpackung ist tatsächlich eine von wenigen dichtestmöglichen. Kepler hätte demnach Recht. Nur: Außer Hales kann niemand den aus 300 Seiten undurchdringlichen Texts und Formeln sowie 40.000 Zeilen Computercode bestehenden Beweis nachvollziehen, auch nicht ein hochkarätiges Gutachtergremium, das sich drei Jahre lang damit auseinandersetzt.

Kein Mensch kann den Beweis verstehen - aber vielleicht Computer? Thomas Hales gibt nicht auf. Er übersetzt sein Werk in eine computerlesbare Form. Zusammen mit einem Team investiert er 20 Personenjahre in "Project Flyspeck", zu deutsch: "Projekt Fliegendreck", bis ein Cloud-Rechenzentrum im Sommer 2014 endlich das Ergebnis liefert. "Formal Proof" heißt die Methode. Sie könnte der reinen Mathematik in Zukunft öfter assistieren und menschliche Gutachter überflüssig machen.