Верификация длинных доказательств: мечты, планы и реальность

We will mainly talk about the unfinished project of Vladimir Voevodsky (the preliminary result of which is summarized in the collective monograph [1]), in which it was supposed to significantly expand the interaction of mathematicians with computers in the construction and verification of proofs.
After a brief overview of the univalent foundations of mathematics, attention will be focused on the problems that arise in connection with proofs, the traditional understanding of which is difficult or impossible due to their length and complexity. Examples will be given; the position of the speaker will be critically compared with the provisions of the well-known provocative text of Nikolai Vavilov [2].
In conclusion, considerations will be expressed about the formalization of the taught mathematics.
[1] Homotopy Type Theory: Univalent Foundations for Mathematics. Univalent Foundations Project, Institute for Advanced Study, 2013. (465 pages) arXiv: 1308.0729
[2] Nikolai Vavilov. Reshaping the metaphor of proof. Philosophical Transactions of the Royal Society A. Mathematical, Physical, and Engineering Sciences, 2019. DOI: 10.1098 / rsta.2018.0279
The meeting will be combined with the Research Seminar on Mathematical Logic of the Department of Mathematical Logic and Theory of Algorithms, link to the recording of the seminar: http://lpcs.math.msu.su/rus/nis.htm.