Другая математика (2/2)
Для обычных математиков тот язык, на котором они реально работают, это естественный язык (русский, английский и т.д.).
Для математических логиков такое положение дел не является приемлемым. Создаются разнообразные теории, находящиеся в активной разработке и идущие на острие прогресса: логики высших порядков, теории типов, все эти HoTT, HOTT и SIP, множество разработок в области теории категорий и др.
Не в малой мере рост интереса к математической логике вызван популяризацией proof assistants – языков программирования, выступающих в роли систем автоматизации математических доказательств (которые в свою очередь стали популярны на волне ИИ – общая идея захода в том, чтобы создать периметр безопасности/уверенности средствами формальной верификации, внутри которых ИИ мог бы искать оптимальное решение, гарантированно не нарушая заданные правила).
Развитие математических теорий начинает идти по законам развития компьютерных систем, накопление знания соответствует росту кода библиотек, организация изложения материала превращается в дизайн архитектуры кода, декомпозицию модулей и стиль кодирования.
Компьютеры стали неотъемлемой частью быта каждого человека, одновременно компьютерные алгоритмы стали метафорами, которыми мы живём – элементом культуры и ментальности. Математики беспомощно проспали этот момент, но математические логики давно были готовы, придумав современные передовые парадигмы языков программирования на сто лет заранее.
Лейденский манифест де-факто приравнивает использование пруф-ассистентов к ИИ, ну какие-то технические штуки там, не то что наше, кондовое, читать тексты на бумаге и прямым озарением верифицировать верность написанного. При этом совершенно не понимая что в этот момент происходит, что сами делают – что вот эта подстановка "по определению" это альфа-эквивалентность, что вот это упрощение выражения это бета-редукция, и что вот этот перенос доказательств вдоль изоморфизма это вообще что-то из гомотопической теории типов.
Компьютеры и ИИ подсветили логические дыры в рассуждениях, но вообще-то преодоление этих дыр и есть суть математики.
"Другая математика" это, в данный момент, всевозможные варианты математической логики. Если бы математика была серьёзной наукой, а не способом времяпрепровождения в своё удовольствие, усилия, вкладываемые в развитие логики, были бы на порядок выше.
Если бы математики всерьёз писали декларацию будущего это была бы очередная программа о следующих ста годах развития математической логики. Единственно важный вопрос гуманитарных наук это вопрос об устройстве самого человека. Единственно важный вопрос математики, следовательно, это вопрос совершенствования математической логики – как дисциплины, моделирующей особенную часть человеческой рациональности.
Какой единственно важный вопрос ИИ? Дилемма здесь не в том, будет ли внедрятся ИИ или нет, этот момент давно пройден и упущен. Дилемма в том сколько будет в нём чего-то тёплого и лампового. За это можно было бы побороться, но едва ли на столь абстрактную цель удастся отвлечься от насущных вопросов грантов, журнальных рейтингов, борьбы с блогами, оценки рисков окружающей среде и всех прочих повышения удоев и измерения площадей полей, к чему Лейденская декларация редуцирует деятельность своих подписантов.
9
6June 20, 2026 426 1 3
