Wie lassen sich Gleichungen automatisch beweisen? Wie kann ich die Korrektheit eines Java-Compilers nachweisen? Hatte Kepler wirklich Recht? Gibt es den automatischen Beweis, dass irgendwelche kuriosen Suchbaumalgorithmen die gewünschte Funktionalität haben? Dies sind einige der Fragestellungen, an denen Tobias Nipkow an der Universität von Manchester, am MIT, an der Universität von Cambridge und seit 1992 als Professor an der TUM gearbeitet hat und noch arbeitet. Das Forschungskolloquium anlässlich seines 60. Geburtstages präsentiert jüngste Ergebnisse zu automatischen und interaktiven Beweisen, dem Arbeitsgebiet von Tobias Nipkow.