Есть сколько угодно "элементарных" теорем, с конкретными приложениями
"на практике", которые доказываются в две строчки (в контексте уже
имеющейся теории), но которые никто никогда не формализовал в системах
вроде Coq и наверное не формализует в обозримом будущем.

Там реализовывались целиком доказательства нетривиальных результатов
вроде печально известной комбинаторной теоремы о четырех красках или
теоремы Фейта-Томпсона из теории групп. Всё это требовало каких-то
нереальных усилий и долгой работы нескольких программистов,
и практического толку от этого нет.

Кажется, были какие-то более инженерные проекты вроде проверки
интегральных схем на корректность или разработки доказуемо
корректного компилятора. Это намного полезнее, но совсем про другое.

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