Из того, что я видел в универе, все теоремы доказываются довольно формально. Имеется множество аксиом, на них строятся простые теоремы, из них, как из кирпичиков - более сложные и так далее. Мне кажется, что можно построить некий DSL, на котором теорема будет записываться аналогично программе на языке программирования - как множество формальных рассуждения. Есть стандартная библиотека (формально проверяемая чекером) известных математических фактов.
Формулируем теорему Ферма. Задача математика - построить цепочку доказательств из стандартной библиотеки, которая даст эту теорему и записать её на формальном языке, а чекер проверит. Если проверка проходит - теорема доказана.
// навеяно новостями, когда доказательства теорем занимают кучу места и их проверяют умные дядьки очень долго, хотя вроде бы процесс проверки доказательства довольно формальный и алгоритмизируемый.
Но раз так не делают - видимо я где то ошибаюсь. Хотелось бы знать - где.