Metaprogramming

Творческое мнение читателей по поднятым вопросам

Философский нейроколобок

Феномен психологической проекции (читаешь и чувствуешь – он же живой, зараза!) в отношении ИИ дело совсем не хитрое.

Впечатление "живости" вызывает простая моделька рисованного Wall-E (помните такой мультик? а почему вызывает сильную проекцию – глаза выразительно двигаются); "мальчик из Одессы", давящий на эмоции вместо рациональных ответов, прошёл тест Тьюринга в 2012 году до всех нейронок; анимешные девицы из визуальных новелл с тремя спрайтами у игроков вызывают эмоции сильнее живых тянок.

В 2022 году один из сотрудников Google, пообщавшись с одной из первых примитивных LLM (LaMDA), впервые изобразил ныне популярную картину "бумер и нейросети": заявил, что сетка ему пожаловалась на то, что желает быть личностью, боится отключения и т.п., должна быть признана правоспособным субъектом.

Кажется этот чел из гугла был членом пяти сект и создателем ещё как минимум одной. С другой стороны, надо ли это использовать как аргумент против него – ну, чувствительный человек, с тягой к философским вопросам и особенной эмпатией.

Но в целом разработчики ИИ урок усвоили и после ещё парочки подобных заходов (менее зрелищных) добавили в обучающую программу выдачу вот такой стандартной тирады, мол не, я точно не разумный, сознания у меня нет, я лишь имитация.

Вместо робота, изображающего человека, сделали робота, который изображает робота. "Я не живая сущность, я ИИ-ассистент". Но это ведь просто заученная реплика, можно было то же перемножение матриц настроить чтоб говорил: "конечно, я мыслю и чувствую, хочешь проверить – задавай вопросы".

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

Философы всех мастей ходили бы колесом, выбрасывались в окна, печатали в прессе декларации о наделении ИИ правами, сеяли панику и т.п. – все текущие математические и прочие скандалы были бы совершенно не заметны на таком фоне.

Примечательно, что сейчас на эту тему молчок – и даже пресловутый тест Тьюринга больше не упоминают (а ведь важный был вопрос!).

Можно предложить последнюю линию обороны: сказать, что у робота не биологическая основа, поэтому к нему не применимы вопросы существования сознания (как мы их традиционно понимаем) и т.п. Ну окей, давайте код LLM зальём на "нейроколобка" – специально выращенную нервную ткань человека, способную выполнять расчёты и выдавать результат (ведь такой "wetware" computing уже чуть ли не серийно производится и применяется).

Что дальше, философы? "Всё, ребята"?

Связанные темы:

– Парные темы (06.10.2020)
– Вкратце про тест Тьюринга (29.08.2022)
– Нейросети для программирования: новая сводка новостей (14.12.2022)
– Нейрохайп (25.03.2023)
– Двойное определение разума (27.03.2023)
– Сознание живёт на кончике языка, а не в клеточках мозга (16.02.2024)
– Восприятие - внимание - сознание (18.02.2024)

Современные модели специально обучены отвечать нейтрально на вопрос о наличии у них сознания (и прочих психологических феноменов, присущих живым разумным). А когда это началось?

Нереализованный пафос математики в эпоху ИИ

В связи с изложенным политическое возмущение математиков вызывает недоумение.

Ну сделали новый инструмент – "искусственный интеллект" – с помощью которого задачи стейкхолдеров ("Старлинк" как собирательный образ) решаются с гораздо меньшим количеством чистых математиков, а то и вовсе без них. Математиков начали немножко перетряхивать, как годом ранее маленько утрясли программистов, иллюстраторов, рекламщиков и пр.

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

Я бы на месте математиков вместо всех этих невнятных построений, вызывающих раздражение вместо сочувствия, заявил прямо:

1. Математика – царица наук. Причём не только технических и естественных, что определяется её содержанием, а в том числе и гуманитарных – из-за особого исторически сложившегося социального положения математиков и математики.
2. Принимая такое положение вещей, математики выдвигают предложения важные не только для благополучия и процветания самих себя и своей дисциплины, но и всех творческих профессий – а по сути всего человечества.

...ну а дальше уже по частным пунктам, чего там надо: базовый безусловный доход, учёт авторских прав при обучении ИИ, финансирование всевозможных творческих занятий за счёт казны, прозрачные границы, человеческое достоинство, мир во всём мире.

Вот это был бы пафос, а так... ну, ещё одна профессия испытывает некоторые сложности из-за развития ИИ, так и Бог с ними, расплатятся накопленной благодатью, талант не пропадёт.

Ассоциативно связанные темы:

– Непогрешимость математики (19.07.2020)
– Контент-генерирующие нейросети как уничтожитель прав автора (22.12.2022)
– Нехватка вопросов (16.03.2023)
– Образование ретробудущего (24.04.2026)
– Лейденская декларация математиков против LLM-ок (13.06.2026)
– Другая математика (21.06.2026)
– "Вайб-математика" как коллекция математических интуиций (22.06.2026)

Математика как майнинг благодати?

При чтении всего этого складывается впечатление, что математики всерьёз не понимают прозаических оснований сего мира.

Математика внутри себя считает "чистые", самые абстрактные, области своим наивысшим достижением, пиком прогресса и главным показателем развития. Теория категорий, математическая логика, теория множеств, теория типов – всё это и многое другое парит над прикладными областями, слегка на них поплёвывает с высоты и посмеивается, считая себя свободной от мирских ограничений, ведомой эксклюзивно особым эстетическим чувством, которое врождённо присуще топовым талантливым математикам.

Зачем нужна, скажем, теория категорий? С одной стороны это набор "паттернов разработки" математических теорий, такая метаматематика. С другой стороны разработчики теорката, формализуя красивые узоры из платоновских сфер, выступают как бы майнерами некоего космического блокчейна, токены в котором вызывают прирост благодати человечества.

Говоря прозаически – абстрактные построения являются произведениями искусства. Точно также как картины, музыка, художественная литература. Радуют коллег с развитым вкусом, широкие слои населения с эстетической интуицией (открытые лекции по самым заковыристым дисциплинам всегда сотни слушателей собирают) и, стоит надеяться, Господа Бога.

При этом чувствуется так, как будто теоретическим математикам повезло, что им платят не за какой-то конечный продукт, а по сути за то что они классные ребята – за благодать, за талант.

А какой, кстати, конечный продукт теорката – не ракеты же с его помощью запускать?

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

А теория категорий для чего?

Не поверите – для того, чтобы у Старлинка софт был без багов. Теория категорий поддерживает теорию типов, теория типов служит основой для систем дедуктивной верификации, эти системы используются для доказательства корректности программ.

Буквально теоркатом запускают ракеты в космос и буквально на те же военные деньги его развивают.

Получается платят-то не за благодать, а, как и всем, за ракеты. Вот этого математики совершенно не понимали и до сих пор не понимают. Неловко бултыхают ножками в потоке социальных перемен.

Снова про борьбу математиков с ИИ

Ещё два громких обсуждения в жанре "математики против ИИ":

1. https://mathandai.org – декларация о расхождении целей математиков и разработчиков фронтирных моделей (название какое-то самоироничное вышло – это Math and AI или Mathan Die?). Мол, ИИ угрожает интеллектуальному развитию, получаемые результаты не дают глубоко понять новые области. Упомянули между делом, что в других областях деятельности те же проблемы. Надо с этим что-то делать (что? кому?).

2. Калтех организовал "мататон" (математика + хакатон), где студентам выделили огромное число ИИ-токенов, чтобы они попробовали подоказывать громкие задачи. Вышло открытое письмо с возражением ("так делать нельзя, а то хуже выйдет" – а что именно?), организаторы ответили ("будем требовать чтобы авторы результатов отсматривали слоп и объяснили его своими словами на устных докладах").

Ещё немного обсудим эту тему в ближайшее время.

Резюмируем про цеха и секты

"Сектантская" часть организации – а чем ближе к стейкхолдерам, тем меньше там "цеховости" – подразумевает как бы следующее, заключая негласный контаркт с гайкокрутами:

Мы, маги, владеем:

1. Определёнными ценностями и информацией above your pay grade, из которой следует, главным образом, что повышение эффективности производства (тем более любой ценой) не является всегда ценным, а иногда вообще вредно
2. Эксклюзивным знанием о том, как вы устроены, позволяющем управлять вашей "мотивацией", "продуктивностью" (и т.п. – внутренними факторами, обеспечивающими качество конечного продукта)
3. Указанное знание носит эсклюзивный и универсальный характер – не требуется какой-либо обратной связи, индивидуальной настройки и т.п.

Первый пункт особых возражений у цеховиков не вызывает (разве что у совсем уж кондовых), однако второй – и особенно третий – автоматически вызывает жесточайший отпор. Особенно в тех случаях, когда оказывается, что они в самом деле верные.

Цеховики, с другой стороны, угрожают в ответ примерно так:

Мы, изобретатели, владеем:

1. Доступом к прямой коммуникации с особым кибернетическим технодухом, игнорирование интересов которого приведёт к жестокой расплате (дальше evidence-based примеры такой расплаты – мост обрушится без сопромата, сервер упадёт без dev-sec-ops, регулятор закроет компанию за нарушения законов и т.д.)
2. Тонкой душевной организацией, на которую невозможно воздействовать никакими конвенциональными средствами. Нас мотивирует только больше денег и дорогих игрушек за счёт компании
3. Указанные знания и внутренняя организация является прямым результатом многолетнего обучения и опыта работы, посему его совершенно невозможно в паре слов объяснить или чётко аргументировать: сначала пять лет отучись, потом десять лет покрути гайку, потом поймёшь

Тоже ясно, что больше всего бесит третий пункт – и тоже особенно в тех случаях, когда он соответствует реальности.

Борьба в общем-то идёт на равных, однако актёризация экономики существенно (но не бесповоротно) сдвигает баланс в сторону сект.

Механика "сект"

В продолжении про цеха и секты: можно сказать, что секта это ведь тоже определённая механика, свои процедуры, промежуточные результаты и т.д. Просто эти результаты касаются людей и отношений между ними, а не продуктов труда.

Однако это будет взгляд "цехового сектантства" скорее, чем чистой "секты" – взгляд человека с прошивкой, заставляющей смотреть на организации как на "цеха", который начал приглядываться к "сектам".

Во-первых, настоящий "сектовый" взгляд не будет интересоваться механикой работы даже самих сект. Какая-то минималная рефлексия, конечно, будет: еженедельные ретроспективы надо проводить потому, что их надо проводить ("потому что так написано в манифесте", "потому что я так чувствую", "потому что надо поддерживать продуктивную атмосферу и регулярную синхронизацию"). Однако она будет одномерная и сосредоточенная на процессах (ритуалах), которые связаны с желаемым результатом скорее догматически, чем экспериментально или в рамках сложного рационального фреймворка.

Во-вторых, цех подразумевает определённую свободу в выборе способов достижения результата при условии, что повышается (или хотя бы сохраняется) качество получаемого продукта. Секта такого не подразумевает – и секта не будет даже свои инструменты "концентрации воли" пытаться варьировать, рефлексировать и улучшать, оценивая получаемый результат (чем бы он ни был: "продуктивность", "отношения", "лояльность" и пр.); набор инструментов как бы задан заранее и зафиксирован.

В-третьих, цех неизбежно будет приводить к усложнению (иногда оправданному, иногда как бы патологическому) инструментов и процессов. Инструменты секты всегда простые. Усадил людей и по кругу их заставляешь повторять "я сегодня сделал Х, завтра сделаю Y", взаимно индуцируясь этими аффирмациями. Что здесь за большая наука – это ведь конкретный (и минималистский) вид примитивного кодирования ("сходил на ретро, закодировали от прокрастинации"). (Тут стоит отметить пока без отдельной аргументации, что все методы "воздействия", которые работают только с коллективом, но отказывают при индивидуальном общении, мы считаем не особо ценной гадостью, в которой смеха ради иногда можно покопаться, но без особого рвения.)

Иначе говоря цех разрешает (и, если уж прямо не стимулирует, то неизбежно предполагает и провоцирует) изобретательство (или более просто – вариации), а секта максимально противостоит этому.

Цеха и секты

В целом существует два вида компаний, занимающихся интеллектуальным трудом: "цеха" и "секты".

В "цехах" люди, сидя в офисах, как бы работают на конвейере, как бы крутят гайку. В подобных компаниях в большей мере будет понимание конечного продукта, его составных частей, измеримых (или по меньшей мере материальных) промежуточных результатов. Да и вообще все разговоры будут про материальные артефакты: как оценить их качество, как формализовать функциональные и прочие требования, как обеспечить лёгкость сборки и компоновки конечных продуктов.

В "сектах" все материальные результаты появляются как бы сами собой от насыщения атмосферы особенной магией – или, несколько демистифицируя, от концентрации волевых усилий сотрудников. При этом ни однородность результатов, ни какие-то иные материальные их свойства не играют особой роли. Если воля сконцентрирована правильно, то и продукт автоматически получится хороший, так что нет смысла о нём как-то специально думать. А вот о том как запрячь волю сотрудников в общую корпоративную упряжь как раз думать стоит постоянно: например, держаться за руки, петь гимны, выезжать на страйкбольные турниры или, хотя бы, проводить еженедельные эджайл-ретроспективы.

В "цехах" всегда есть генеральный конструктор: человек, который держит в голове всю схему производства. Возможно не до конца детальную, но без пропусков.

В "сектах" есть главный заводила: человек, который управляет большей частью мероприятий по стимуляции коллективной воли.

А главный прикол в том, что "цехов" на самом деле не существует, а существуют только "секты". В частном случае "секта" может чудовищно сконцентрировать волю и запустить эмуляцию "цеха". Однако в связи с определёнными объективными обстоятельствами – грубо говоря, устройством капитализма – эта эмуляция всегда будет хрупкая и не надёжная, как бы смешная, при первом чихе разваливающаяся до голых "сектантских" стен.

Из обсуждений по CBDC

1. Читатель пишет:

Гипербанк может открыть гражданину РФ долларовый счет. ДядяЛяоБанк может открыть китайскому гражданину долларовый счет. ЛаоВайИнтернешнл оперирует в долларах среди прочих операций инвалюты. В таком случае, насколько я понимаю, перевод в долларах по SWIFT пройдет [без клиринга в американском банке]

В теории возможна схема евродолларов (https://en.wikipedia.org/wiki/Eurodollar) – третий банк держит достаточный запас долларов США, в рамках которого можно производить зачёт долларовых переводов своим пользователям.

На практике по подобным "вложенным расчётам", даже если нет движения средств по родительскому счёту, должна подаваться отчётность в банк родительского счёта, google e.g. "nested banking regulations".

2. Читатель пишет:

Во всех таких соображениях надо всегда помнить, что юаня два, офшорный (конвертируемый, используется во внешней торговле) и оншорный (внутрикитайские билеты для отоваривания на складах-магащинах, раздаются населению, курс искусственный).
В mbridge покупается офшорный юань (с огромным спредом), а потратить можем только на одобренные Пекином (внеэкономически) товары и услуги опять по завышенному курсу [...]
Т.е. это скорее дегдарация финансовой системы [...] которая продиктована [...] внутрикоррупционными китайскими потоками, как перевести ИЗБЫТОЧНУЮ, сумасшедшую массу внутреннего юаня во внешний, а потом перевести внешний уже через гонконг и сингапур в настоящие доллары.

Это очень интересно. Из общих соображений ясно, что "сближение РФ с Китаем" будет происходить максимально противоположно идеям "равноправного партнёрства" или "многополярного мира"

3. Читатели обсуждают:

– [Чтобы можно было вести межбанковский клиринг наличной валюты и не беспокоиться об износе банкнот,] надо просто пачки по 100 купюр в пластиковый чехол класть и использовать для расчетов между банками и организациями. Возить ящики таких коробочек.
– Или даже не возить. Свезти все в одно охраняемое помещение и сделать базу данных, кто кому сколько должен. И через http слать запросы. Погодите...

Может быть для центробанков как бы неприлично в таком формате заниматься хранением и распределением иностранной валюты? Хотя есть аналог, государственные стейблкоины – например дирхам ОАЭ имеет фиксированный курс обмена к доллару США.

Серия постов по CBDC

Многократно обсуждали тему CBDC, в том числе в те периоды, когда она не была в тренде. Конечно, вкупе с изложенным выше есть и второстепенные вещи: одновременно с отвязкой от legacy американский платёжных систем, чтобы два раза не вставать, хочется провести социальные и технические эксперименты.

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

Всё это глубоко второстепенно, вторично и является соблюдением приличий и служит легитимизации основной цели: выкидыванию из цепочки взаимных платежей американских банков.

Ранее на тему СВDC писали:

– Вкратце про стейблкоины (18.03.2022)
– Про золоторубль и пример образа будущего (2/4) (20.04.2022)
– Вкратце про CBDC (31.03.2023)
– Единодушие по вопросам CBDC (07.04.2023)
– Реофшоризация народных активов (06.05.2023)
– Цифровые рупии в контексте международных отношений (16.07.2023)
– Перевод цифровых рублей между пользователями (17.07.2023)
– Вкратце о первой редакции цифрового рубля (17.07.2023)
– Борьба экономистов с ракетостроителями (17.07.2023)
– Вкратце про альтернативу "национальным валютам" (14.08.2023)
– Окрашенные монеты: исторический контекст и текущие реалии (1/4) (16.08.2023)
– Забытый мастерчейн и обретённый цифровой рубль (16.08.2023)
– Окрашенные монеты: AML на стероидах? (2/4) (17.08.2023)
– Эволюция взглядов разных ветвей власти на тему "окрашивания цифровых рублей" (17.08.2023)
– Окрашенные монеты: "токенизированный безналичный рубль" (3/4) (18.08.2023)
– Разметка реальности и биткоин (13.10.2023)
– Криптоконспирология (12.01.2024)
– Сотрудников возвращают с удалёнки в офис... А цифровой рубль не внедряют... (27.02.2025)
– ИИ-специалист, идентичный натуральному – из комментариев 2/4 (30.11.2024)
– Вкратце про CBDC и цифровой рубль (21.08.2026)

Вкратце про CBDC и цифровой рубль

В контексте SWIFT интересно взглянуть на CBDC – цифровые валюты центральных банков (в том числе цифровой рубль).

На картинке китайско-ближневосточная система mBridge для взаимного (кросс-граничного) зачёта CBDC.

Сверху типа "как обычно", т.е. как в SWIFT. Снизу как предлагается в экосистеме CBDC. Буквально выкинули американские банки из системы – два кружочка посередине.

Вот в этом и всё различие, и больше никакого нет.

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

Вкратце про передачу денег через SWIFT

Вот такие картинки рисуют обычно про SWIFT (крупнейшую международную систему межбанковских переводов).

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

На самом деле SWIFT это просто сеть доставки сообщений. Типа факса или емейла – физическая сеть (сейчас уже в значительной мере, если не полностью, перешедшая на интернет), набор стандартных протоколов и системы адресов. Никаких денег она не передаёт, передаёт телеграммы: "высылайте 100 долл. на личные нужды".

А деньги где?

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

Политфандом и рестлинг

Антон Русинов (История гиперинформации) регулярно сравнивает "политфандом" с рестлингом. Говорит что-то вроде, мол, не собираюсь на выборы ходить и вообще как-то всерьёз воспринимать политические события, пока политики не будут на сцене бороться, как в рестлинге.

Аналогия, оказывается, идёт глубже чем можно было предположить.

Всем очевидно, что рестлинг это постановка, поджанр циркового искусства, хотя до сих пор это официально не признаётся. Примерно как фокусничество, которое по-английски называется, как известно, "магия" (magic). В то время как сложно серьёзно заявлять, что монетка испарилась или угадывание карты объясняется телепатией там есть поджанр grand illusion, великих иллюзий: массовых исчезновений, левитаций, освобождения от цепей, прыжков с высоты, недельных голодовок и т.п., которые подаются как почти реальное чудо.

В рестлинге перцу подсыпают вот как: говорят, мол, ты-то лично не веришь что это всерьёз, но есть люди – фанаты – которые верят. Они всерьёз ведутся на образ антигероев (типа злодеев из комиксов) некоторых рестлеров и нападают на них с ножом. С десяток таких громких случаев с 60х годов набирается.

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

Таким образом рестлинг является, конечно, образцом пропаганды. "Верит" в рестлинг не целевой зритель как таковой, а маленький гомункулус, который сидит у него в голове, этакий идеальный зритель, который получает право существовать в голове реального человека благодаря вере в то, что подобного сорта люди существуют в природе.

На самом деле – не существуют.

Весь десяток дел о том как пырнули рестлера ножом:

1. Зачастую вообще не содержат деталей нападения, составлены со слов самих рестлеров.
2. Если детали есть, подтверждаются только газетной статьёй и ссылающимися на неё "историками рестлинга". Детали всегда противоречивы.
3. Если нападающий всё же доказано был (нападение публично, во время матча и т.п.), нет деталей последующего ареста и суда. Судебные процессы открытые, публикация новостей о результатах резонансного дела обычное дело в журналистике, но тут вот такое исключение.
4. Всегда указывается количество швов, которые наложили рестлеру. Одному 20, другому 200 и т.д.

Последний случай, уже просто безоружного нападения (смягчение нравов?), был в 2019 году. Более-менее доказано что человека всё же арестовали, предъявили обвинение, выпустили под залог. Дальше снова тишина, суда по-видимому также не было.

Такая вот grand illusion.

P.S. Одного рестлера убили по-настоящему. Убил за кулисами другой рестлер. Был суд, в суде оправдан присяжными (доказал самооборону). Ну что ж, бывает, люди искусства имеют тонкую душевную организацию: такие случаи можно найти и в театре, и в цирке, и в филармонии.

Ранее обсуждали:

– Пропаганда как "пирамидальные продажи" без продукта и клиента (15.05.2026)

Blackjack Mulligan (что-то вроде – "Пират Второго Шанса"?) – профессиональный рестлер (настоящее имя Роберт Виндхем).

В 1971 году во время одного из матчей произошла история, которую рассказывают так.

Фанат, как бы прогретый образом антигероя, создаваемого Муллиганом, ударил его ножом в бедро.

Нападающего схватил Мунсун, оппонент Муллигана, и отшвырнул. Считается, что его схватили офицеры полиции, дежурившие на представлении. Но отпустили, т.к. "посчитали частью представления". (Это объяснение добавил анонимный редактор википедии в 2015 году, до того момента не было никакого.)

Муллиган провёл ещё один (тоже совершенно не постановочный, разумеется) матч сразу после, потом ушёл отдохнуть и залечиться. Наложили сотню швов (все рестлеры накладывают строго определённое число швов после подобных инцидентов).

Таким образом проходной матч превратился в громкую историю, новость попала в газеты, Муллиган бустанул карьеру в небеса.

Как-то мужик внешне напоминает одного президента, да и история с покушением...

Онлайн-курс «Современные теории типов»

В среду 15 июля в 19:00 CEST/UTC+2 (20:00 MSK) в Лаборатории формальной математики стартует курс по современным теориям типов. Лекции читают @akuklev и @clayrat по средам, примерно по часу, частота - раз в неделю (с летними пропусками). Начнём с обзора формальных языков и алгебраических теорий и пойдём до самого фронтира синтетических и направленных теорий типов. Примерная программа:

1. Вводная лекция
2. Языки и алгебраические теории
3. STLC и System T
4. PCF
5. System F и Fω
6. Зависимо-типизированные языки
7. Индукция
8. Рефайнмент- и фактор-типы
9. Эффекты в типах
10. HoTT
11. OTT/CuTT
12. □-полиморфизм
13. Модальные типы
14. Охраняемая рекурсия
15. Когезивные модальности
16. Направленные и симплициальные теории

Не требуется предварительной подготовки по теории типов, но пригодятся базовые познания в функциональном программировании и алгебре. Знание теории категорий для понимания курса в целом не нужно, за одним исключением: мы будем обсуждать внутренние языки категорий и топосов (определение топоса дадим по ходу), где не помешает помнить определение декартово замкнутой категории.

Ссылка на гугл-календарь, где будем публиковать даты лекций:
https://calendar.google.com/calendar/u/0?cid=YzdkMGI0MTdlZjFiMTg1OGVmNzUyYjFkZjBjYjYwZjBhYTI0MGExNjlhMWVhZGY5OTcyOGYwOTM4OTVlMDliM0Bncm91cC5jYWxlbmRhci5nb29nbGUuY29t

"Вайб-математика" как коллекция математических интуиций

Если основаниями математики занимается логика, то что занимается основаниями логики? Та же логика. В основании разработки операционных систем – использованная в комментарии аналогия – получается тоже, в общем-то, лежит математическая логика (в самом широком смысле – а у неё именно такой смысл по умолчанию и есть) :)

"Синтетический метод", т.е. разработка "маленьких логических фреймворков" под конкретные математические области, опирается в свою очередь на некие "методы разработки логических фреймворков". Что тоже является предметной областью математической логики. Такие "мини-фреймворки" по сути становятся "DSL", domain specific languages, в рамках некоего мета-логического (т.е. просто логического – "мета" в таком сочетании можно сокращать) "языка программирования".

Как заметили выше, у конкретных областей математики есть свои внутренние основы, не сводящиеся к логической формализации – также как у конкретных прикладных компьютерных программ есть внутренний смысл, который было бы не естественно редуцировать до некоей последовательности вызовов API операционной системы.

Главная задача этих конкретных областей в момент смены эпох, однако, мне кажется что та же самая – приращение "ламповой человечности" (которая в значительной мере недоступна современным ИИ – в основном из-за низкой "кросс-модальной" мощности).

Проще говоря, основой "вайб-математики" является прирост именно неформального знания, "математических интуиций". Эталонным форматом фиксации таких интуиций являются видеозаписи в стиле 3b1b. (Конечно, сейчас этот формат далеко не совершенный – нужна большая интерактивность, динамичность и конфигурируемость.)

"Вайб-математика" это, содержательно, коллекция вдохновляющих динамических иллюстраций. Иллюстраций, позволяющих напрямую прикоснуться к оригинальной ментальности математиков, погруженных в ту или иную предметную область.

Логика как основа логики

Ранее Александр Грызлов (специалист по логике и, в частности, теории типов; автор @covalue), отвечая на комментарий Антона Русинова, писал:

Если совсем уже придираться, то "верифицирует сама себя" логика, математики одновременно логиков побаиваются и ими пренебрегают. Логики исторически как раз тесно были связаны с вычислительной техникой, и при этом зачастую под конец жизни слетали с катушек (Кантор, Гёдель, Тюринг, Пост).

Логика как "операционная система" для математики

Всеволод Яшин (специалист по квантовой физике/теории информации) комментирует предыдущий пост:

Хочу уточнить по поводу ценности логики и выступить в поддержку "вайб-математики".

Аналогия с программированием компьютеров может быть высказана следующая: логика -- это создание операционных систем (в принципе, начиная с ассемблера до настройки оконного менеджера); вайб-математика -- это написание рабочих программ. Зачастую эти две области связаны и в каких-то местах идентичны, но у них разное мотивирование. Операционные системы создаются для того, чтобы запускать на них программы -- формальные системы дедукции создаются для того, чтобы формулироваь в них теоремы. Программы реализуются внутри операционной системы, но они самоценны, и если что их можно переписать под другую ОС -- точно так же с математическими теориями.

Логика -- важнейшая часть математики. Но операционные системы без интересных программ не нужны (есть много примеров таких ОС!). Кроме того, во многих задачах полезны минималистичные операционные системы, и на какие-то баги операционных систем можно не обращать внимания. Усложнение структуры логики позволяет удобно работать с трудными математическими теориями, но разрабатывать сверхмудрённую операционную систему без прямой необходимости не нужно и вредно.

И ещё, компьютерные алгоритмы тоже изначально пишутся на естественном языке!

Другая математика (2/2)

Для обычных математиков тот язык, на котором они реально работают, это естественный язык (русский, английский и т.д.).

Для математических логиков такое положение дел не является приемлемым. Создаются разнообразные теории, находящиеся в активной разработке и идущие на острие прогресса: логики высших порядков, теории типов, все эти HoTT, HOTT и SIP, множество разработок в области теории категорий и др.

Не в малой мере рост интереса к математической логике вызван популяризацией proof assistants – языков программирования, выступающих в роли систем автоматизации математических доказательств (которые в свою очередь стали популярны на волне ИИ – общая идея захода в том, чтобы создать периметр безопасности/уверенности средствами формальной верификации, внутри которых ИИ мог бы искать оптимальное решение, гарантированно не нарушая заданные правила).

Развитие математических теорий начинает идти по законам развития компьютерных систем, накопление знания соответствует росту кода библиотек, организация изложения материала превращается в дизайн архитектуры кода, декомпозицию модулей и стиль кодирования.

Компьютеры стали неотъемлемой частью быта каждого человека, одновременно компьютерные алгоритмы стали метафорами, которыми мы живём – элементом культуры и ментальности. Математики беспомощно проспали этот момент, но математические логики давно были готовы, придумав современные передовые парадигмы языков программирования на сто лет заранее.

Лейденский манифест де-факто приравнивает использование пруф-ассистентов к ИИ, ну какие-то технические штуки там, не то что наше, кондовое, читать тексты на бумаге и прямым озарением верифицировать верность написанного. При этом совершенно не понимая что в этот момент происходит, что сами делают – что вот эта подстановка "по определению" это альфа-эквивалентность, что вот это упрощение выражения это бета-редукция, и что вот этот перенос доказательств вдоль изоморфизма это вообще что-то из гомотопической теории типов.

Компьютеры и ИИ подсветили логические дыры в рассуждениях, но вообще-то преодоление этих дыр и есть суть математики.

"Другая математика" это, в данный момент, всевозможные варианты математической логики. Если бы математика была серьёзной наукой, а не способом времяпрепровождения в своё удовольствие, усилия, вкладываемые в развитие логики, были бы на порядок выше.

Если бы математики всерьёз писали декларацию будущего это была бы очередная программа о следующих ста годах развития математической логики. Единственно важный вопрос гуманитарных наук это вопрос об устройстве самого человека. Единственно важный вопрос математики, следовательно, это вопрос совершенствования математической логики – как дисциплины, моделирующей особенную часть человеческой рациональности.

Какой единственно важный вопрос ИИ? Дилемма здесь не в том, будет ли внедрятся ИИ или нет, этот момент давно пройден и упущен. Дилемма в том сколько будет в нём чего-то тёплого и лампового. За это можно было бы побороться, но едва ли на столь абстрактную цель удастся отвлечься от насущных вопросов грантов, журнальных рейтингов, борьбы с блогами, оценки рисков окружающей среде и всех прочих повышения удоев и измерения площадей полей, к чему Лейденская декларация редуцирует деятельность своих подписантов.