...Так-то мне это просто сильно интересно, поэтому в любом случае продолжу впроголодь развивать парадигму топологически-ориентированного программирования на базе гомотопической теории типов. Мой подход пока хотя и учебный, но чисто технически/архитектурно потенциал его несравненно выше существующих пруф-ассистантов и теорем-пруверов, потому что они сами по себе фактически полузакрытые фреймворки, где требуется огромное количество ручного ввода, а интеграция с чем-то внешним серьёзно затруднена. Верификация кода на 5,000 строк требует 200,000 строк кода доказательств :)

А хорошо бы более активно и солверы, особенно свои, применять для автоматического поиска доказательства и стыковки с AI:
- обучение на существующих формализованных доказательствах;
- генерация подсказок и дополнений при построении доказательств;
- приближение языка формализации к обычному математическому;
- более понятная визуализация доказательств
и т д и т п.

Стратегически в планах сделать (причём именно в таком порядке)
1 "свой формальный верификация"
2 "свой пруф-ассистант"
3 "свой солвер"

Солвер же это на сегодня задача по сути чисто техническая, никаких питонов, сразу надо делать скоростную версию на rust. Но там такая логика, что для реальных проектов нужна оперативка на сотни гигов, для возни с булевыми формулами. Никогда уже не накоплю на раб.станцию, на последние гроши взял свежую книжечку "Введение в алгебраическую топологию" (лекции на мехмате МГУ, в Новосибе: симплициальные, сингулярные и клеточные гомологии, связь с гомотопическими группами клеточных пространств, кольцо когомологий, двойственность Пуанкаре...). Не исключено, что сильная математическая база вполне может снять кучу технических проблем.