Математическое доказательство: вчера, сегодня, завтра

Спасибо andrew-vdd. Из выступлений двух математиков о доказательстве в 2010 году.

Ю. В. Матиясевич:

'Уже сегодня компьютеры могут проверять формализованные доказательства нетривиальных теорем.

ПРЕДСКАЗАНИЕ Через 25 лет журналы (если они ещё будут существовать) не будут принимать к рассмотрению статьи, не сопровождаемые доказательствами, которые может проверить компьютер.'

Н. А. Вавилов:

'В отличие от любых доказательств, математическое знание КАК ТАКОВОЕ обладает ЧРЕЗВЫЧАЙНО высокой степенью надежности. Эта надежность, как и надежность естественно-научного и технического знания, гарантируется отнюдь не доказательствами индивидуальных результатов, а общей когерентностью математической и естественно-научной картины мира, индивидуальным и коллективным пониманием и прямым контактом с миром идей, которое формируется в процессе работы у каждого квалифицированного и понимающего специалиста.

Вот, что знают о доказательстве практикующие математики, но боятся сказать:

– Математическое доказательство, РАССМАТРИВАЕМОЕ КАК ТЕКСТ, не доказывает ничего, кроме факта существования доказательств.

– Ни одно СЕРЬЕЗНОЕ математическое доказательство не может быть полностью формализовано, т.е. записано в соответствии со стандартами, пропагандируемыми математической логикой.'

К теме: Изменчивая природа математического доказательства