Спасибо andrew-vdd. Из выступлений двух математиков о доказательстве в 2010 году.
Ю. В. Матиясевич:
'Уже сегодня компьютеры могут проверять формализованные доказательства нетривиальных теорем.
ПРЕДСКАЗАНИЕ Через 25 лет журналы (если они ещё будут существовать) не будут принимать к рассмотрению статьи, не сопровождаемые доказательствами, которые может проверить компьютер.'
Н. А. Вавилов:
'В отличие от любых доказательств, математическое знание КАК ТАКОВОЕ обладает ЧРЕЗВЫЧАЙНО высокой степенью надежности. Эта надежность, как и надежность естественно-научного и технического знания, гарантируется отнюдь не доказательствами индивидуальных результатов, а общей когерентностью математической и естественно-научной картины мира, индивидуальным и коллективным пониманием и прямым контактом с миром идей, которое формируется в процессе работы у каждого квалифицированного и понимающего специалиста.
Вот, что знают о доказательстве практикующие математики, но боятся сказать:
– Математическое доказательство, РАССМАТРИВАЕМОЕ КАК ТЕКСТ, не доказывает ничего, кроме факта существования доказательств.
– Ни одно СЕРЬЕЗНОЕ математическое доказательство не может быть полностью формализовано, т.е. записано в соответствии со стандартами, пропагандируемыми математической логикой.'