А что, никто не дает компьютерам заданий доказывать теоремы в ZFC?
Может и дают. Не знаю, кому теперь интересно компьютерное повторение доказательства этой теоремы. Вот если бы её изначально удалось доказать компьютеру, это было бы интересно. Но тут ещё надо как-то "правильно" выбрать аксиоматику. Да и тупой перебор в лексикографическом порядке, конечно, тоже неинтересно, т.е. и выбор правильных эвристик имеет значение.
-- Вт июл 05, 2016 23:52:28 --А такого предположения никто здесь, кажется, не делал
Я исхожу из того, что фразу "нет оснований для уверенности в обратном" можно трактовать как предложение рассмотреть это в качестве предположения.
-- Вт июл 05, 2016 23:55:57 --Вытащить их из мозга великих математиков на сегодняшний день нет никакой практической возможности.
Ну да, разумеется, между "практической невозможностью сегодня" и "принципиальной невозможностью" лежит пропасть, которая позволяет надеяться, что первая когда-нибудь потеряет актуальность.