Сейчас для России уникальная возможность стать абсолютным топчиком в мировом ИТ (вопрос, правда, а кому-то тут это нужно?). Потому что будущее однозначно за человекочитаемыми формальными доказательствами корректности кода + AI, который сможет переводить структурированные доказательства между доменами и системами, а у нас (пока ещё) есть подходящие умы.

Во всём мире, среди всех математиков (Тао юзает и рекомендует) фактически ключевой тут культовый системой стал теорем-прувер + функциональный язык с зависимыми типами Lean(4) -- с ужасающей архитектурой, крайне тормозной и неполный, и при этом из РФ доступный лишь через впн (то есть никак).

Так-то формализация математики началась ещё в 1968 году с системы AUTOMATH (на ней в частности доказали полноту вещественных чисел). Другие исторически важные системы: LCF (70-е), HOL (80-е). Boyer–Moore (ACL2 в 90-е) для верификации кода -- все на Лиспе. Ну а потом, во многом трудами Воеводского, явился Coq (ныне Rocq), Agda, Isabelle, Lean и т.д. На них были формализованы доказательства знаменитых теорем: четыре цвета, теорема Фейта–Томпсона, гипотеза Кеплера (1611-й год:)...

Lean же привлёк математиков благодаря отказу от навязчивой "конструктивности" и относительно неплохой библиотеке, но это далеко не единственный разумный выбор на сегодня. В частности принцип "пропозиции как типы" не обязателен; AUTOMATH и LCF работают без него. В LCF не нужны громоздкие объекты доказательств благодаря абстрактным типам данных из нашего любимого семейства ML.

Isabelle предлагает лучшую "автоматизацию", читаемость, ну и кстати отсутствие завтипов (и связанных с ними проблем) -- многие сложные конструкции (поля, p-адические числа, схемы Гротендика) можно проще формализовать и без них. Но и у этого языка куча своих проблем -- прежде всего исторических конечно, связанных с его развитием в эпоху до AI.

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

Уровень для этого? Вполне достаточно стандартный PhD в cs. Пример приводил недавно, как парнишка в одиночку подобный язык создаёт, и в "Функциональных архитектурах" сейчас разбираю эту темку подробнее.

Хотя по хорошему конечно, надо идти не от функциональщины, а от математики -- HoTT, HOTT, топологии в целом... Я тут что-то пытаюсь сделать на коленке...