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

P>Еще было что-то про ЭВМ, которая доказала некую теорему за 38 секунд. Правда, в публикации не уточнялось, сколько времени программу отлаживали, по которой ЭВМ работала.

Такие доказательства уже есть. Например, задачу доказательства свели к 10 тысячам частных случаев. Программа проверила все эти частные случаи — теорема доказана.