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

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

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