Онтология и гомотопическая теория типов: унифицировать всё против найти «убойное приложение»
Основное назначение «чистой математики» — это давать интересные типы объектов, чтобы представлять/represent основные черты поведения объектов физического мира, а также основные черты поведения объектов ментального мира (других математических объектов). Само это представление/representation — это предмет онтологии. Онтологические исследования в приложении современной теории типов (а не теории множеств) как основы/элементов математики активно ведутся[1], хотя не все математики и физики признают эту связь семантики, математики, онтологии, физики, теории понятий.
Представление о развитии математики тем самым оказывается связанным с важностью развития математики для решения каких-то внешних по отношению к математике проблем, а не просто «математики для математики». Это волновало Воеводского, волнует Родина и ещё множество математиков: если не получать время от времени задач из физики или других естественных наук, то происходит застой в самой математике — ибо не появляется интересных задач в прикладной математике, для которых чистая математика предложила бы новые типы математических объектов, удобные для их решения. Унивалентные основания математики тут помогут удержать разговор о новых типах математических объектов совместимым с разговором о старых типах объектов, то есть они помогают удержать рамки формальности/строгости в рассуждениях о постоянно расширяющемся наборе математических объектов с хорошо понимаемым интересным поведением.
Есть два варианта: либо пытаться воткнуть куда-то основания математики для 1) переписывания старого не очень формального (без компьютерной проверки доказательства теорем, написано в виде текстов на естественном языке с вкраплениями формул, совместно это «гипертекст», а не «компьютерная программа») и разношёрстного уже накопленного/legacy знания, или 2) поддержать новой математикой решение новых проблем: то есть повторить ход изобретения разных исчислений по потребностям естественной науки (типа как интегрирование и дифференцирование изобретены для решения задач механики, а потом развитие этих исчислений привело к выходу на квантовую теорию поля), и только потом формализации этих новых исчислений, уж насколько это возможно (полностью формализовать математические выкладки нельзя, об этом говорят теоремы Гёделя о неполноте[2]).
Одна из текущих проблем тут — это отсутствие развитого формального аппарата, компактно и формально описывающего распределённые представления/distributed representations. Нейросети стремительно растут в их применениях (в частности, появились LLM типа GPT-4 и Bard), но работ по распределённому представлению онтологий не так много. Отдельные работы по теории нейросетей и вычислениям в нейросетях как универсальных аппроксиматорах есть, но этих работ не так много и они по линии «классической математики с представлением функций», а не по линии классической онтологии с объектами и отношениями.
С доведением до практики, конечно, в этом направлении всё плохо: обычная проблема каких-то «оснований» в том, что с их приложениями знакомо много людей, а с самими основаниями — очень мало людей. С унивалентными основаниями математики людей знакомо очень мало, ибо основная аксиома во всём этом — аксиома унивалентности --сформулирована в 2006-2007 годах, для математики это очень малый срок (это ведь не распространение приложения по смартфонам, это распространение теории по головам людей, это проходит медленно).
К предложенному подходу с унивалентными основаниями математики отношение должно быть общим, как ко всем идеям, предлагаемым в ходе техно-эволюции (меметической эволюции): это гипотеза, что весь этот матаппарат будет хоть как-то полезен, сэкономит время, даст невиданные результаты. Пока непонятно, что может быть «убойным приложением»/«killer application». Текущая попытка найти такое приложение — это «доказательство правильности компьютерных программ» и предложение языков программирования, которые обладают повышенной выразительной силой в силу использования идеи зависимых типов (возможны вычисляемые типы переменных). Это явно не супервостребованное направление, особенно после понимания того, что значительная часть вычислений связана с нейронными сетями, где вопрос о формальности очень плохо проработан.
Как узнать, что получено «убойное приложение» какой-то идеи? Что-то должно стать эффективней, быстрее, дешевле, проще (то есть опять-таки дешевле и быстрее) — желательно, чтобы во много раз. Но с этими приложениями унивалентных оснований математики пока проблемы. Есть ли что-нибудь такое, что раньше нельзя было посчитать, а сегодня применили новую математику — и посчитали? Похоже, ничего такого нет — новых расчётов или повышения точности для старых расчётов при переложении со старых математических подходов на новые не предложено.
Если предположить, что новая математика нужна для компактификации и унификации математического знания (не помощь в новых расчётах, а объявление каких-то результатов, полученных разными математиками, «одним и тем же», переписывание старых результатов на новый язык, например, теоркатегорный язык), то считать, что экономится человеческое знание, тоже нельзя. Всё это «похожее» редко приходится рассматривать одним и тем же людям — разные инженеры делают разные расчёты, и как в эволюции идея каких-нибудь плавников или крыльев изобреталась много раз и реализована разными генами, так и в математике придумывалось много разных способов решения задач на каком-то уровне строгости. И интерес сейчас даже не столько к новому аппарату для формальной строгой математики, сколько к идеям нейросетей как универсальных аппроксиматоров, универсальных оптимизаторов, а также интерес к явно недоизученым распределённым (прежде всего нейросетевым, «выучиваемым») представлениям.