Да, статья, безусловно, интересна и показательна. Уместная, точнее своевременная. К эпохе своевременна. Математика, как методологический инструмент точного познания мира стоит на рубеже очередной переформализации методов. Или революции в способах формализации своих методик работы. Во все известные нам (или большинству из нас) эпохи, начиная с античности, методики формализации процессов количествоенного описания процессов познания мира (включая инженерию во всех формах) испытывали последовательные стадии усложнения, насыщения и пресыщения усложнениями, затем наступал период упрощения путем введения более ёмких способов формализации и потом процесс повторялся. Кратко поясню на примерах развития способов математической нотации решений уравнений в античные времена, во время средневековья, в эпоху Возрождения и, наконец, в настоящее время, когда относительно универсальная нотация позволяет заменять огромадное множество вычислительных алгоритмов и дает возможность преподавать данные дисциплины в школах на всех континентах независимо от рас и национальностей. Лишь бы мозги да языки были в налиции. И глаза с руками. А ведь еще в середине тысячелетия простое квадратное уравнение описывалось , к примеру, итальянскими математиками словами и занимало это не полстрочки , а целую страницу порой. Так и теперь имеющаяся и очень изощренная нотация в пограничных областях познания уперлась в тупик суперусложнения. Необходим другой вариант описания решений (доказательств). Причем, безусловно, реализуемый в кибернетическом пространстве. До сих пор мы исчерпывали только ресурсы человеческого мышления, не отягченного компьютером. Этот вариант решений можно назвать алгоритмическим, хотя это название применимо и ко все предыдущим эпохам развития математики (как до, так и после Ал-Хорезми, введшего понятие алгоритма около тысячи лет назад). Ведь запись решения того же квадратного уравнения (или кубического) - тоже алгоритм, но очень легко реализуемый в уме. А вот классы задач, с которыми имеет дела и на которых обламывает зубы современная математика, уже не могут быть решены никаким, даже очень изощренным, человеческим умом. Нужно много умов, помноженных на компьютеры. И тут уже необходима максимально верифицируемая матодика выполнения "доказательств" и производства "выкладок" именно компьютерным путем. И только таким путем можно было бы решить до максимально возможных пределов ту задачу классификации групп, которую приводил в качестве примера автор. и тогда цепочка последовательных фолрму какого либо "доказательства" бУдет иметь вид цепочки последовательно примененных алгоритмов вычислений с приведенными многотысячелистовыми распечатками результатов и трассировок (по необходимости), если говорить упрощенно. Собственно говоря, я не сомневаюсь, что такие методики уже работают, только пока еще в зачаточном состоянии, если вспомнить для сравнения путь развития современной высшей математики (в смысле развития нотации и формализации обработки данных и процессов работы), начиная с Ньютона и математиков-механиков-астрономов 18-го века.
Словом, человечество ждет, конечно, счастливый конец, который оно благополучно минует на пути к сияющим вершинам познания на вечно далеком горизонте.
Пост Скриптум.
Вообщето я просто сказал то же, что и автор статьи, только выпендрился сказать покороче и понепонятнее. Ну, просто эмоции выплеснул, сам давно об этом думаю, а давно уже слыхал про вычислительные методики в математических доказательствах, в смысле существования класса задач, к которым только так и можно приступаться.
Ответить