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

S>Хотелось бы 100% формализации мат. теорем. Есть Coq, вроде даже чувак с интернета хотел формализовать на нем доказательство Великой Теоремы, но это был труд на годы, не знаю закончил или нет.

Работа в этом направлении ведется. QED Manifesto

Может пока не очень активно.
По-моему, главная проблема в неудобстве существующих языков/средств.
Попробовал проследить доказательство первой теоремы из списка (иррациональность sqrt(2)), черт ногу сломит.
Кто активно занимаются, пишут в 4 раза больше времени уходит на формализацию, чем на доказательство.
Неудивительно, что это пока удел энтузиастов.
Вот когда наоборот среда формализации будет помогать поиску доказательств, тогда станет гораздо популярнее.