Существует много разновидностей белковых существ, интересующихся теоркатом, гомотопической теорией типов, формальной логикой... Но среди них нету ни одного из тех, которых я хотя бы минимально помню по их постам в блогах или чатиках, кто бы сходил с ума по блокчейну и крипте в конце 2010-х… В основном ровно наоборот: они их хейтили.

Время от времени я просто думаю про себя: "Гомотопии и категории всё ещё здесь, а где блокчейн?". Те ребята заявляли, что веб3 изменит мир, а математика уже никому не нужна... Но я всё ещё здесь, а вот их как раз уже нету.…

Сегодня я аналогично думаю о повальном увлечении стартапами применением языков программирования из куба Барендрехта (прежде всего, языков с зависимыми типами и теорем-пруверов) к искусственному интеллекту. Да даже и чисто функциональные языки... Но это увлечение может только подорвать репутацию теории категорий или HoTT...

По крайней мере, так будет продолжаться до тех пор, пока эти люди не начнут понимать, что LLM -- это не только линза, или полиномиальный функтор, или тип (промпт) в огромном пространстве гомотопий (недетерминированных путей доказательства) и т.д. Пока они будут пытаться применять любые из этих вещей поверхностно, это в итоге категорически ни к чему не приведёт.

"А давайте обучим нейронку "программировать" на Lean4 или TLA+, и она потом будет писать безошибочный код!"

Я не очень хорошо отношусь к людям, которые пытаются превратить поверхностное понимание в деньги.