Kolmogorov and Gödel's approach to intuitionistic logic: current developments

Intuitionistic mathematics was created by Brouwer on the basis of constructive reasoning, where the existence of a proof was the criterion for truth. Kolmogorov and Gödel proposed interpreting intuitionistic logic on the basis of classical notions of a problem's solution and of provability. In 1933 Gödel made the first substantial step toward the building of such an interpretation. Despite much progress in the understanding of intuitionism, this task was not complete before the author's 1995 paper. This survey will cover the results of the past decade obtained within this framework.