Очередное разочарование и избавление от иллюзий (и это очень хорошо): оказывается, когда нам говорят "ну вот же, вот, посмотрите -- математики это доказали, вот статьи в авторитетных журналах" - в 99,98% случаев это никакие не доказательства - в смысле конструктивных подходов - потому что для этого требуется отдельно доказать, что придуманное кем-то там доказательство верное. Сейчас такое доказательство доказательства единственное: мнение экспертного сообщества, и тут политики всё больше и больше.

Причём сами математики не шибко-то стремятся использовать современные теорем-пруверы - потому что если таким образом формально попроверять их работы, то весьма вероятно oкажется, что многие из них отнюдь не настолько "доказаны", как считалось. А за такие работы платят весьма прилично.

Хороший пример -- разрекламированная по всему миру шумиха вокруг якобы решённой проблемы BB(5) про Усердных Бобров -- дескать, математики не только это доказали, но и формально верифицировали сам процесс доказательства!

Сайт проекта bbchallenge , их спонсоры prgm.dev , код бобров на github.

Да, но...

"Природа, вероятно, встроила в машины с пятью состояниями одну или несколько проблем, столь же иллюзорных, как гипотеза Гольдбаха. Или, другими словами, скорее всего, будут существовать безостановочные рекурсивные паттерны, которые мы не в состоянии распознать."
Аллен Брэди, BB(4)