Talk given on November 9, 2022 on Zoom.

Abstract: A. N. Kolmogorov in 1932 proposed an original version of mathematical intuitionism where the concept of problem plays a central role, and which differs in its content from the versions of intuitionism developed by A. Heyting and other followers of L. Brouwer. The popular BHK-semantics of Intuitionistic logic follows Heyting's line and conceals the original features of Kolmogorov's logical ideas. Homotopy Type theory (HoTT) implies a formal distinction between sentences and higher-order constructions and thus provides a mathematical argument in favour of Kolmogorov's approach and against Heyting's approach. At the same time HoTT does not support the constructive notion of negation applicable to general problems, which is informally discussed by Kolmogorov in the same context. Formalisation of Kolmogorov-style constructive negation remains an interesting open problem.