Аналогия здесь точная, однако точность ее распространяется только на ход доказательства, но отнюдь не на степень его сложности. В математике доказательство непротиворечивости конечной формулы чрезвычайно сложно.

Вейль напоминает, что Гильберт изложил свою теорию доказательства, сложившуюся у него около 1922 г., в работах «Новое обоснование математики» и «Логические основы математики». В первой из этих работ он формулирует расщепление математики на формальную математику и «метаматематику». Развитие общей математической науки, поясняет Гильберт, осуществляется, с одной стороны, посредством получения (с помощью формального вывода) новых доказуемых формул из аксиом, а с другой стороны (с помощью содержательного вывода), посредством присоединения новых аксиом и доказательства непротиворечивости.

При этом Гильберт обращает внимание на то, что аксиомы и доказуемые предложения не являются истинами в абсолютном смысле. Абсолютными истинами, по его мнению, следует скорее считать воззрения на доказуемость и непротиворечивость систем формул, порождаемые его теорией доказательства (то есть «метаматематикой»).

Таким образом, у Гильберта — лидера крайнего «формализма» — математика расчленилась на математику формальную («формальную теорию») и «метаматематику» («теорию доказательства»). Математика изучает формальную систему в целом. Метаматематику, относящуюся к какой-либо конкретной формальной системе, американский исследователь Клини впоследствии назвал «метатеорией» (см. 9, 60). В отличие от формальной теории «метатеория», по словам Клини, «принадлежит интуитивной, неформальной математике... Утверждения метатеории должны быть понимаемы. Ее выводы должны убеждать. Они должны состоять в интуитивных умозаключениях, а не в применении установленных правил, как выводы в формальной теории» (9, 61). Для нее невозможна полная абстракция от смысла, составляющая условие строгой формализации теории. Применяемые в ней методы «используют только интуитивно представляемые предметы и осуществимые процессы» (9, 61). Для самого определения формальной математики необходима математика интуитивная (см. 9, 61).