Narya -- new proof assistant that implements a type theory that is a common generalisation of dTT and HOTT!
Да ещё и написано это чудо на
(только HOTT это не HoTT :)
This type theory seeks to combine the advantages of "Book HoTT" and cubical HoTT, and avoid some perceived disadvantages of either
Про кубики я пояснял 5 лет назад: "Кубическая теория типов для малышей"
=
"Towards Large Language Models as Copilots for Theorem Proving in Lean"
Our latest experiments show that our co-pilot can automate >80% of the proof steps (2.3 times better than the previous rule-based baseline aesop).
P.S. Тем временем: "Яндекс разрабатывает Календарь+ с ИИ" 😁