Да есть давно уже программы для проверки (и частичного вывода) доказательств. Толку от них практически нет и в разумном будущем не предвидится, всё сколько-нибудь нетривиальное в них очень сложно формализуется.

Разговор про доказательство теорем компьютером -- такая же банальщина, как и про основания математики. И мнение человека со стороны тут примерно так же ценно (т.е. никого не ебёт).