Я недавно подумал, что математика спущена с того, что люди могут доказывать приятным им образом.
То есть, например, если автопруверы станут удобны и от этого популярны, то доказать приятным образом м.б. станет легко совсем другие вещи, и математика (ну типа выбор основных сюжетов) сильно изменится.
Это напоминает об одном сюжете из научной фантастики, где пришельцы появляются, и герой говорит: вот сейчас мы начнем с чисел Фибоначчи [это как бы нечто независимое от языкового барьера]; но если вычислительные средства сильно отличаются, то это может быть и совсем неправильный ход мысли.