Einer der größten Mathematiker der Gegenwart will das Beweisen gänzlich dem Computer anzuvertrauen. Dazu muss er nichts weniger als die Grundlagen seines Fachs neu fassen.