Ein Computer, der eigenständig Beweise führt – davon träumen Mathematiker. Neue Methoden der KI könnten die Zukunftsvision ein Stück näher bringen.