Человек и машина

«— Он выработал в себе ценнейшую способность понимать в общих чертах, не вникая в частности. Между прочим, это — основное отличие человека от машины. Ей, дуре, надо все растолковать до малейшей подробности. А человеку можно сказать: «Разберись в ситуации и поступай соответственно».

(И. Грекова. Пороги, гл. 13, конец.)

Это надо взять на заметку, объясняя студентам необходимость в формальных доказательствах. Человек обладает удивительным даром «непрерывного», «интегрального» мышления, он конструирует идеальные образы (чем отличается не только от машины, но и от животного). «Всё сочинено, но еще ничего не написано» (апокрифическая моцартовская, якобы, фраза) – вот этого ни машина, ни зверь не умеют. И перед записью доказательства теоремы в голове часто вертятся некие зрительные образы (даже если теорема не имеет никакого отношения к геометрии). Но если вы хотите препоручить доказательство компьютеру (программе-пруверу), то ему,» дураку», надо всё по полочкам разложить, дать четкие инструкции в виде правил вывода. И тогда он сделает всё намного быстрее человека.

Ну, и, разумеется, формализация доказательства имеет и чисто математический смысл, так как если мы хотим что-то доказывать о доказательствах («объяснять объяснения»), то доказательство должно стать строго определенным математическим объектом, ибо ничего нельзя математически доказать по поводу того, что математически не определено.