Читал, что классик жанра не в состоянии изложить свои результаты мало-мальски связно, так что интересующиеся воспринимают эти результаты на рукомахательном уровне ;).
Есть пример классификации конечных простых групп. Она записана в виде кучи журнальных статей (и книг с предварительными результатами), там вполне могут быть мелкие ошибки, которые можно самостоятельно исправить при чтении. Есть серия книг с изложением этого доказательства, но она не окончена, объёмная (пусть и меньше исходных статей), и всё равно требует предварительных знаний. Формализацию этого без помощи ИИ я не могу представить. Причём сама теорема активно используется в научной деятельности, но большинство специалистов по конечным группам вряд ли читали доказательство полностью.
Проблема со всякими модными продвинутыми разделами математики в том, что чтобы их понять, надо слишком много учиться. У студентов и аспирантов времени нет, чтобы освоить и алгебраическую теорию чисел, и теорию схем, и всякие
-категории одновременно (в случае Вербицкого будут другие разделы). В результате появляется куча конспектов в интернете и обзоров на Архиве, где почти всё даётся без доказательств и рукомахательно, лишь бы дать какое-то представление о предмете и сформулировать содержательные результаты. Зато можно, поверив в эти результаты и имея научного руководителя, что-то доказывать самому. Пруфчекер в такой ситуации всего лишь поможет поверить и избавит от ошибок, но понимания не даст.
04.01.2026, 02:36 
, в Coq достаточно написать слово "рефлексивность". Потому что, прежде чем доказывать равенство, Coq вычислит обе части до упора и получит 
. В Metamath придётся доказывать шаг за шагом из аксиом Пеано. Однако, многим нравится.