Похоже, что интуиционизм еще не заматерел, не выкристаллизовался, и нам еще только предстоит осознать его значение.
Интуиционизм возник в начале XX века как один из способов преодоления кризиса в основаниях математики. В теории множеств, на основании которой хотелось бы построить математику, обнаружились всякие парадоксы и противоречия. Чтобы выйти из кризиса, математики пробовали идти разными путями, и один из них — интуиционизм. Он сформировался не сразу, и интуиционистами могут называть математиков с разными взглядами. Обычно интуиционисты не строят доказательства от противного и с особой осторожностью работают с бесконечностями. А еще для них важно, что построение математических объектов и рассуждения о них должны быть интуитивно ясны и убедительны.
Взять какие-то высказывания, потом манипулировать ими по формальным правилам и делать формальные выводы — не для интуиционистов. Некоторые из них вообще отрицали манипулирование значками. Каждый отдельный вывод должен быть очевиден и ясен индивидуально. Но возможны некоторые общие правила, по которым из одних утверждений интуитивно очевидным путем получаются другие утверждения. Вот такие правила составляют интуиционистскую логику.
Она отличается от классической. Например, в классической логике каждое высказывание либо истинно, либо ложно. А у интуиционистов есть истинные высказывания, ложные и все остальные, пока еще непроверенные. Если высказывание не является истинным, отсюда еще не следует, что оно ложно.
https://ru.wikipedia.org/wiki/Гомотопическая_теория_типов#/media/Файл:Hott_book_cover.pngНад основаниями своей науки математики продолжают работать. И интуиционистская логика дает направление для этой работы. Интуиционистское исчисление высказываний строил А.Н.Колмогоров (и другие). Его ученик Пер Мартин-Лёф создал интуиционистскую теорию типов. Его подход использовал В.А.Воеводский для создания гомотопической теории типов. Он ввел аксиому унивалентности и довел свои идеи до этапа практических применений. На этой базе уже можно создавать системы автоматической проверки доказательств. В институте перспективных исследований в Принстоне 2012-2013 учебный год объявили годом унивалентных оснований. Приезжали математики и информатики со всего мира, чтобы развивать эту теорию. Построили набор формальных описаний для Coq (автоматизированная система для работы с доказательствами), чтобы формулировать доказательства для абстрактных разделов математики.
В 2017 году Воеводский умер, и это большая потеря для современной математики, ему был всего 51 год. Неясно, будут ли продолжены его работы, кем и как. По меркам истории математики прошло не так много времени для развития этого направления.
Я бы сравнила создание интуиционистской логики с трудами Семёна Дежнёва. В XVII веке он открыл Колыму, вышел с товарищами в Ледовитый океан и прошёл Беринговым проливом задолго до Беринга. Основное значение путешествий Дежнёва в том, что он их совершил. Раз видно белое пятно на карте, — надо идти в разведку. Такая обзорная разведка не ставит конкретных целей, зато по ее результатам можно определиться с дальнейшими направлениями исследования.
Современное состояние этого направления в математике — это как заявка России на арктический шельф. Заявка — ещё не освоение, мы не знаем точно, какие будут результаты.