Rzk Proof Assistant and Simplicial HoTT Formalisation
A Russian-language STEP seminar talk introducing rzk as an experimental proof assistant for synthetic ∞-category theory, and demonstrating early formalisations. Delivered several months before the English-language HoTTEST 2023 talk.