В 20 веке появилась и распространилась идея о соответствии между компьютерными программами и математическими доказательствами. Благодаря ей, стало возможно повышать строгость как в программировании ("well-typed programs cannot go wrong"), так и в математике. Появились исполняемые машиной доказательства и программы с формально доказанными свойствами.
Эта идея, в основном, вдохновляет людей, занимающихся логикой, метаматематикой и теоретической информатикой. Есть проблемы с принятием её ценности как работающими программистами, так и работающими математиками.
Если с программистами давно все понятно ("сложно", "думать впрок не аджайл", "релиз горит", "квартальной премии лишают"), то математики, казалось, бы гораздо более умные люди, гораздо более способные к абстрактному мышлению и менее вовлеченные в мирскую суету.
Тем не менее, от средств механизации проверки доказательств математики бегут, как черт от ладана. "Вы ничего не понимаете в математике", "неудобно", "математика устроена не так" и тому подобные отговорки. Можно подумать, что математикам чужда механизация как таковая, потому что им исторически хватало карандаша и бумаги, или мела и доски, или даже палки и песка.
Однако же, любой математик сейчас самостоятельно занимается типографской подготовкой своих манускриптов в латехе. Ни одному математику сейчас и в голову не придет дать своим коллегам почитать перепутанную стопку бумаги, исписанную неразборчивым почерком с помарками. Механизация типографского набора в математике это данность на протяжении десятилетий.
Почему бы математическому сообществу не согласиться, что неприлично заставлять рецензента не только ломать глаза о почерк, но и проверять за автора его логические выкладки? Почему бы не передать и этот труд машине, оперирующей хорошо изученным формализмом? Чего бояться-то?
Я думаю, что в ближайшие несколько десятилетий благодаря механизации математики некоторых лауреатов крупных математических премий признают, нет, не шарлатанами (зачем так оскорблять уважаемых людей, да еще с высокими градусами), а кем-то вроде злостных неплательщиков налогов. В тюрьму их, конечно не посадят, а просто заставят выплатить их долг с процентами. Например, их ученикам придется стать самыми ярыми механизаторами математики, чтобы другим был ПРИМЕР.
Красиво набранная в латехе статья всегда производит хорошее впечатление на рецензента. Если выкладки так симпатично выглядят на странице, разве могут в них быть какие-то ошибки? Тем более, упаси св. Гротендик, подтасовки? Очевидно, что не могут. Джентльмен джентльмену верит на слово.