я бы прежде всего конечно перенёс мой HoTT/кубический движок на питончик 3.14, уже имея в отличие от стэнфордских пацанов
- тесную интеграцию со всем стеком PyTorch/JAX/NumPy -- для обучения тактик, ретривера лемм, RL с фидбэком от проверяющего ядра;
- полный контроль над trusted kernel/аксиоматикой HoTT (Univalence, HITs, кубические Сигмы, Kan-композиция) + быстрые эксперименты;
- гибкую архитектуру термов (de Bruijn/HOAS);
- программируемую генерацию синтетики: пути/ кубы/системы → мощные датасеты и property-based тестирование "из коробки".
Дальше,
- допиливаем кэширование/мемоизацию, тонкое профилирование (py-spy, tracers),
- легко и просто склеиваем с SMT/ATP (z3-solver, cvc5);
- добавляем нейросимволические циклы Generate→Check→Learn на одном Питоне!!1 Трассы поиска/ошибки элаборации/метаданные обучающих эпизодов -- у меня все под руками прямо в Py.
Фигак фигак и в прод: notebooks с визуализацией кубиков, REST/gRPC, и деплой через pip/docker без кривейшего тулчейна Lean.