...Но с другой стороны, давайте будем максимально честными: нафига нам "свой прувер"? Чтобы получилось точно такая же ситуация, как и со "свой игровой движок" -- потратим миллиарды, а на выходе карго-культ?

Причём ещё ладно если так, а если это будет что-то существенно хуже работающее, чем существующий опенсорс, и к нему будут принуждать насильно? Тогда вместо формальной верификации наши КИИ получат ужасающее количество бэкдоров :)

И главное, а кто это будет делать-то? Последний наш мировой спец по HoTT уехал в Европу в 2023-м, а тут требуется не только топовая математика, но и мощнейший инженерный бэкграунд, чтобы не получился в итоге ещё более слабый клон Lean4 (который сам по себе кривейший и архитектурно и концептуально).

...Впрочем, а я-то чего об этом волнуюсь? Я в этих темах никто, и звать меня никак. С моей стороны это чисто научпоп. Поэтому, надо просто принять и простить, что Lean4 стал на сегодня в отрасли фактически промышленным стандартом. Да, очень кривейшим, примерно как Java на фоне нормальных языков, но лучше-то нету! Ну, Coq/Rocq, Agda, F*, но они уже очень сильно отстают просто потому, что в лине есть мощнейшая mathlib, куда уже впилили кучу математики, и продолжают активно накачивать.

Поэтому надеюсь, что свой прувер у нас делать не будут, потому что без матлибы он будет пшиком... Ну ок, можно делать синтаксически совместимым с лином, это значит и потащить за собой все его кривые фичи. Или писать свой конвертер, который ещё надо формально верифицировать, и т.д. и т.п.

Всё, поезд ушёл.

В связи с вышеизложенным с глубоким прискорбием вынужден сообщить, что я буду обучать (вас:) Lean4, коли даже стартапы чётко под него собирают по миллиарду долларов. И, конечно, это musthave, если вы математик и хотите укатить в европы америки...