ну как, Воеводский очень беспокоился, вдруг где-то у него в доказательстве гипотезы Блоха дырка (а ведь они наверняка там есть, другой вопрос, уничтожают ли они доказательство), и вся жизнь прошла зря. вот тут мы имеем довольно выпуклый пример: про S⁶ существует множество доказательств, что на нём нет комплексных структур, а также построения этих комплексных структур на S⁶ в количестве наличествуют. если бы существовал chess-like помогатель, способный хотя бы эти дырки отчетливо обводить вокруг красным, дабы все видели: ага, ну это, более-или менее, очевидно; или - ой, а это мне не пришло в голову - совсем даже другие были бы порядки (реалистичности создания такого помогателя я не касаюсь за некомпетентностью, заметь - но мне кажется, что Воеводский движется в эту сторону).

случая Атьи это, вероятно, не касается (и очень жаль, если так), но в раскладах по типу "мемуара Дюлака" самое оно, по-моему (хотя он толстый вроде). нужен, конечно, именно assistant, а не checker.

по-простому, я бы не пожалел полчаса, чтобы прогнать через assistant утверждение, что точки некомпактного сепарабельного многообразия - это в точности подпространство максимального спектра с полем вычетов R (если я не ошибаюсь памятью, это ты выразил сомнения по поводу); не важно, что это задача из Милнора-Сташефа, ошибки бывают и у мастеров.

причем какие-то успехи в этом направлении есть, правда, не у Воеводского и про checker: например, теорема Фрейденталя формально проверена про гомотопические группы сфер, это, как мне всегда казалось, не вполне тривиальное геометрическое рассуждение.