Здравствуйте, lpd, Вы писали:

vsb>>Кстати интересно. А вообще реально хотя бы то, что студентам преподают, засунуть в формализацию? Вроде как все доказательства довольно формальны и дело только за тем, чтобы написать формальный язык описания доказательства и сделать, так сказать, базу этих самых теорем и доказательств. По ней можно и учебники генерировать автоматически.

lpd>Есть труды Бурбаки. Только я не вижу в этом смысла, т.к. за излишняя формализация отдаляет от читателя смысл математики. Доказательство теоремы — это прежде всего выявление высокоуровневых взаимосвязей между абстрактными понятиями, а не посторение строгой логической цепочки.

Смысл хотя бы в том, чтобы проверка и принятие доказательств новых теорем занимала миллисекунды, а не годы, как это иногда бывает. Заодно всех ферма-фриков можно отсечь, например.

Здравствуйте, lpd, Вы писали:

vsb>>Кстати интересно. А вообще реально хотя бы то, что студентам преподают, засунуть в формализацию? Вроде как все доказательства довольно формальны и дело только за тем, чтобы написать формальный язык описания доказательства и сделать, так сказать, базу этих самых теорем и доказательств. По ней можно и учебники генерировать автоматически.

lpd>Есть труды Бурбаки. Только я не вижу в этом смысла, т.к. за излишняя формализация отдаляет от читателя смысл математики. Доказательство теоремы — это прежде всего выявление высокоуровневых взаимосвязей между абстрактными понятиями, а не посторение строгой логической цепочки.

Смысл хотя бы в том, чтобы проверка и принятие доказательств новых теорем занимала миллисекунды, а не годы, как это иногда бывает. Заодно всех ферма-фриков можно отсечь, например (а может быть и найти жемчужину, мало ли).