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