Als Thomas Hales 1998 die seit 400 Jahren offene keplersche Vermutung bewies – es ist unmöglich, gleich große Kugeln dichter zu packen, als die Orangenhändler das seit jeher tun –, war zunächst der Jubel groß. Dann kam die Ernüchterung: Der Beweis erstreckte sich nicht nur über mehrere hundert Seiten, sondern war auch so chaotisch formuliert, dass die größten Meister der Mathematik sich außerstande sahen, seine Richtigkeit zu beurteilen.

Die naheliegende Forderung, das ganze Zeug doch einmal ordentlich aufzuschreiben, lehnte Hales zunächst ab. Nochmals mehrere Jahre mit der Bestätigung eines aus seiner Sicht bereits erbrachten Resultats zuzubringen? Da hätte er Besseres zu tun. Aber dann fand er sich doch immerhin bereit, die knechtische Arbeit an einen Computer zu delegieren. Das geht zwar nicht unbedingt schneller: Es ist überaus mühsam, eine Aussage und ihren Beweis so zu formalisieren, dass eine eigens dafür geschriebene Software, ein »Beweisassistent«, jeden einzelnen gedanklichen Schritt auf gewisse Grundaxiome zurückführen und damit verifizieren kann. Aber es verschafft dem ganzen Werk, sei es für Menschen durchschaubar oder auch nicht, den ersehnten Nachweis der Korrektheit. In diesem Fall dauerte es mehr als ein Jahrzehnt: Erst am 14. August 2014 meldete das Projekt Flyspeck (»Fliegenschiss«) Vollzug.

Damit ging, zumindest für diesen Einzelfall, ein Traum des großen Mathematikers David Hilbert in Erfüllung ...