Невозможность записать формализованное доказательство
очевидна,
А почему, собственно?
Очевидна она, ИМХО, настолько же, насколько очевидна невозможность написать программу уровня, э-э-э, Mozilla Firefox. Просто в силу того, что там байтов очень много будет.
Ну и что? Берётся язык достаточно высокого уровня - XUL, например, - и пишется гораздо короче.
Точно также, язык, на котором пишутся мат.доказательства, достаточно близок к формальному - но не низкоуровневому языку типа первых глав Бурбаки, а высокоуровневому.