Т-34 85
Потому что вряд ли получится сформулировать теорему
Теорема формируется на таких языках в качестве типов. Доказательством служит программа данного типа.
Как раз формулировки этих теорем достаточно просты, вопрос в доказательствах, т.к. они там немного своеобразные, но привыкаешь быстро.
Так что оно сильно менее нереалистичное, чем ты себе представляешь.