And also that, among others, the four-colour theorem's only known proof is a computerized check of hundreds of cases. Will this increasingly be the case? Is this the way mathematics is going? Will any sufficiently difficult problem from now on require a computational step? Does that mean that mathematicians until now were using the non-computational subset of mathematics?