разве нельзя сказать, что компьютер уже готов заменить математиков, если можно просто нажать кнопку и он начнет извергать логические следствия из всех известных утверждений? Здесь-то и вступает в игру творческое начало. Придумать нечто новое легко. Используя нисходящий стиль программирования, вполне можно построить машину, которая будет строчить новые математические теоремы. Трудно создать нечто ценное.