Лейденская декларация математиков против LLM-ок
Кевин Баззард (говорили про него раньше) в числе подписантов "Лейденской декларации об ИИ и математике".
Ещё в 2020 году объявил проект по дешёвому сбору данных для обучения ИИ – заставлять бакалавров математики переводить стандартный материал курсов на Lean. На этой волне и стал мировой знаменитостью.
В 2026 году пишет: "техногиганты лезут к нам в математику, да что ж творят-то, караул!". А кто им дверь открыл и ковёр постелил? :)
Саму декларацию подписало тысячи людей (подписать можно легко онлайн), среди которых несколько лауреатов Филдсовской премии и прочих выдающихся специалистов.
Главная мысль декларации примерно такая: во-первых, гопатыч ничего не может и плохо работает; во-вторых, кто ж нам теперь будет деньги платить, если мы срочно не начнём его саботировать?
В общем-то декларации писать поздно, так как вопрос с "доказательством теорем" закрыт. Ну, программисты точно такие же переживания испытали уже год-два назад.
Кевин Баззард (говорили про него раньше) в числе подписантов "Лейденской декларации об ИИ и математике".
Ещё в 2020 году объявил проект по дешёвому сбору данных для обучения ИИ – заставлять бакалавров математики переводить стандартный материал курсов на Lean. На этой волне и стал мировой знаменитостью.
В 2026 году пишет: "техногиганты лезут к нам в математику, да что ж творят-то, караул!". А кто им дверь открыл и ковёр постелил? :)
Саму декларацию подписало тысячи людей (подписать можно легко онлайн), среди которых несколько лауреатов Филдсовской премии и прочих выдающихся специалистов.
Главная мысль декларации примерно такая: во-первых, гопатыч ничего не может и плохо работает; во-вторых, кто ж нам теперь будет деньги платить, если мы срочно не начнём его саботировать?
В общем-то декларации писать поздно, так как вопрос с "доказательством теорем" закрыт. Ну, программисты точно такие же переживания испытали уже год-два назад.
👍9🔥3❤1
Картинка из "Гипериона" (классическое НФ произведение, которое я всё не доберусь прочитать, хех).
Изобретена телепорация и решены все материальные проблемы, но при этом надо строить небоскрёбы.
Не живётся без бетонных коробок человечеству. А может быть и в самом деле человечество ушиблено модерном настолько сильно, что обречено сохранять внешние черты модернизма навсегда – как периода, в котором в каком-то смысле себя впервые (на массовом уровне) осознало.
Изобретена телепорация и решены все материальные проблемы, но при этом надо строить небоскрёбы.
Не живётся без бетонных коробок человечеству. А может быть и в самом деле человечество ушиблено модерном настолько сильно, что обречено сохранять внешние черты модернизма навсегда – как периода, в котором в каком-то смысле себя впервые (на массовом уровне) осознало.
👍11🔥4
Театр экономики
В значительной мере любая организованная деятельность это театр: сам факт наличия зафиксированных ролей делает их исполнение чем-то наносным, "неаутентичным".
Однако достижения ИИ обостряют и доводят до предела подобный расклад. Картинка получается вполне себе научно-фантастическая: достигнута технологическая сингулярность, а люди по-прежнему ходят работать в небоскрёбы.
А зачем?
Взять текущий уровень развития LLM и программирование: вполне можно заменить тестировщика на разработчика, разработчика на продуктового менеджера, продуктового менеджера на аналитика и т.д. во всех комбинациях. Через пару недель адаптации при наличии подписки на фронтирную модель никто не заметит разницы. В найме, однако, важно показать соответствие роли: ну, способность к импровизации, убедительность образа ("верю!"), знание классических произведений.
Стейкхолдеры же вообще изначально являются сортом актёров. Репетируют речи, делают презентации, нетворкинг, то сё.
Не трудно предположить дальнейшее распространение "актёризации".
Например, водители будут играть роль водителей. То есть "обучаться", "получать права" и потом "держать руки на руле". Получается Илон Маск то в самом деле гений, если ещё 20 лет назад понял, что нужен не настоящий автопилот, а автопилот, который требует постоянное участие актёра-человека.
Второй пример, банковские операционисты и, шире, сотрудники фронт-офиса любой публичной организации уже сейчас лишь играют роль клерков. Вся работа с клиентами сводится к нажатию в приложении кнопочек, соответствующих запросам, и зачитыванию с экрана стандартных ответов или результатов работы ИИ-моделей.
Адвокатов, прокуроров и судей легко заменить на LLM – при этом среднее качество правосудия значительно возрастёт – однако кому такое придёт в голову? Будут распечатывать ответы чатгпт и отправлять по бумажной почте друг другу, манифестируя свою волю, интенцию и правоспособность.
Сократить целые пласты "рабочего класса" без какого-либо ущерба для экономики можно было и десять лет назад, и двадцать, а может и ещё раньше, однако никто этого не сделал. Нет оснований предполагать, что сейчас это должно случиться (хотя может – как могло и десять лет назад, и двадцать).
Думаю в настоящий момент консенсус относительно внедрения ИИ состоит именно в "актёризации" всевозможных сфер экономики. Так что и математикам – имея в виду предыдущий пост – особо не надо беспокоиться – подкинут токенов чтоб на хлеб с маслом хватало. Хотя я бы на их месте манифест по-другому формулировал.
В значительной мере любая организованная деятельность это театр: сам факт наличия зафиксированных ролей делает их исполнение чем-то наносным, "неаутентичным".
Однако достижения ИИ обостряют и доводят до предела подобный расклад. Картинка получается вполне себе научно-фантастическая: достигнута технологическая сингулярность, а люди по-прежнему ходят работать в небоскрёбы.
А зачем?
Взять текущий уровень развития LLM и программирование: вполне можно заменить тестировщика на разработчика, разработчика на продуктового менеджера, продуктового менеджера на аналитика и т.д. во всех комбинациях. Через пару недель адаптации при наличии подписки на фронтирную модель никто не заметит разницы. В найме, однако, важно показать соответствие роли: ну, способность к импровизации, убедительность образа ("верю!"), знание классических произведений.
Стейкхолдеры же вообще изначально являются сортом актёров. Репетируют речи, делают презентации, нетворкинг, то сё.
Не трудно предположить дальнейшее распространение "актёризации".
Например, водители будут играть роль водителей. То есть "обучаться", "получать права" и потом "держать руки на руле". Получается Илон Маск то в самом деле гений, если ещё 20 лет назад понял, что нужен не настоящий автопилот, а автопилот, который требует постоянное участие актёра-человека.
Второй пример, банковские операционисты и, шире, сотрудники фронт-офиса любой публичной организации уже сейчас лишь играют роль клерков. Вся работа с клиентами сводится к нажатию в приложении кнопочек, соответствующих запросам, и зачитыванию с экрана стандартных ответов или результатов работы ИИ-моделей.
Адвокатов, прокуроров и судей легко заменить на LLM – при этом среднее качество правосудия значительно возрастёт – однако кому такое придёт в голову? Будут распечатывать ответы чатгпт и отправлять по бумажной почте друг другу, манифестируя свою волю, интенцию и правоспособность.
Сократить целые пласты "рабочего класса" без какого-либо ущерба для экономики можно было и десять лет назад, и двадцать, а может и ещё раньше, однако никто этого не сделал. Нет оснований предполагать, что сейчас это должно случиться (хотя может – как могло и десять лет назад, и двадцать).
Думаю в настоящий момент консенсус относительно внедрения ИИ состоит именно в "актёризации" всевозможных сфер экономики. Так что и математикам – имея в виду предыдущий пост – особо не надо беспокоиться – подкинут токенов чтоб на хлеб с маслом хватало. Хотя я бы на их месте манифест по-другому формулировал.
👍12🔥6❤1
@GrandHamsterGms отвечает на пост, вспоминая мысли К.А. Крылова:
В самом деле, ни ММО, ни "образования будущего", ни гулагов не надо – людей может занять тем, что их и так уже сейчас занимает – теми же работами, что они сейчас делают. Только делать будет ИИ, превращая людей в зиц-председателей на своей собственной должности.
В комментариях к предыдущему посту также выражают нейроскепсис. Думал, с чем бы это сравнить, что было прямо на наших глазах – да с интернетом. Помню в детстве родители иронически так смотрели, типа, ну хорошее место, анекдоты там почитать можно и всё такое. Это конец девяностых был, начало двухтысячных.
"А реально-то что?!"
Дальше, кстати, такая же ирония была про удалённую работу. Один друг рассказывал, жил в то время с бабушкой (родители умерли к тому времени), что она его месяцами пилила по поводу работы. Типа сидишь дома за компьютером целыми днями. В конце концов он сходил в банкомат, снял месячную зарплату наличкой, и дал бабушке подержать стопку – подействовало, жалобы прекратились, хоть и всё равно не вполне бабушка поняла в чём прикол. Это середина десятых была примерно.
Где-то чуть позже ещё были облачные сервисы. Ну это нишевая тема уже, конечно, с другой стороны у меня среди подписчиков одни айтишники :) Помню говорил с неким руководителем проектов интеграции SAP-а (из поколения ещё советских "айтишников"), что мол в облака всё уходить будет, а он непонимающе отвечал, мол, ну и чего, это уже было, вот помню в наше время к мейнфрейму терминалы подключали и работали с разделением времени.
Потом изобрели криптовалюту, уже была вторая половина десятых когда широко распространилась, над ней иронически хихикали даже неглупые финансисты типа известного Кримсональтера. После того как десять процентов Европы (даже по номинальному подсчёту, сколько де-факто – вопрос) убрали за барьер санкций – и "цифровые валюты" стали единственным доступным средством платежа – стало не до смеха и ранее иронизировавшие эксперты до сих пор на эту тему благоразумно молчат.
Сейчас вот LLM-ки. Ну тьфу, ллмки, а реально-то что?!
Но предположим столь же иронически, что может быть что-то всё же есть. Ну также как в интернете было изначально что-то интересное и т.п. Мне кажется мой взгляд не содержит неуместного восторга или алармизма по поводу ИИ, укоренён в наблюдаемых фактах (которые я не всегда явно привожу для краткости, особенно если их можно увидеть "посмотрев в окно").
Напомню вайбы канала, которые стараюсь выдерживать, которые служат моей мотивацией:
Раз уж математиков, консерваторов от природы, проняло, вроде не лишне было бы рационально призадуматься. Может быть прикол-то есть какой-то в "генераторе текста, не способном придумать ничего нового"? Может быть вот эта обязательная ироническая полуулыбка и махание рукой это в данный момент уже не проявление высокого интеллекта, а банальное бумерство? Да ну, ерунда какая-то! :)
...зачем городить огород с тоталитарными системами ущемления, если можно оставить всё как есть? Люди будут ходить в офисах, тыкать кнопки, получать зарплату...
В самом деле, ни ММО, ни "образования будущего", ни гулагов не надо – людей может занять тем, что их и так уже сейчас занимает – теми же работами, что они сейчас делают. Только делать будет ИИ, превращая людей в зиц-председателей на своей собственной должности.
В комментариях к предыдущему посту также выражают нейроскепсис. Думал, с чем бы это сравнить, что было прямо на наших глазах – да с интернетом. Помню в детстве родители иронически так смотрели, типа, ну хорошее место, анекдоты там почитать можно и всё такое. Это конец девяностых был, начало двухтысячных.
"А реально-то что?!"
Дальше, кстати, такая же ирония была про удалённую работу. Один друг рассказывал, жил в то время с бабушкой (родители умерли к тому времени), что она его месяцами пилила по поводу работы. Типа сидишь дома за компьютером целыми днями. В конце концов он сходил в банкомат, снял месячную зарплату наличкой, и дал бабушке подержать стопку – подействовало, жалобы прекратились, хоть и всё равно не вполне бабушка поняла в чём прикол. Это середина десятых была примерно.
Где-то чуть позже ещё были облачные сервисы. Ну это нишевая тема уже, конечно, с другой стороны у меня среди подписчиков одни айтишники :) Помню говорил с неким руководителем проектов интеграции SAP-а (из поколения ещё советских "айтишников"), что мол в облака всё уходить будет, а он непонимающе отвечал, мол, ну и чего, это уже было, вот помню в наше время к мейнфрейму терминалы подключали и работали с разделением времени.
Потом изобрели криптовалюту, уже была вторая половина десятых когда широко распространилась, над ней иронически хихикали даже неглупые финансисты типа известного Кримсональтера. После того как десять процентов Европы (даже по номинальному подсчёту, сколько де-факто – вопрос) убрали за барьер санкций – и "цифровые валюты" стали единственным доступным средством платежа – стало не до смеха и ранее иронизировавшие эксперты до сих пор на эту тему благоразумно молчат.
Сейчас вот LLM-ки. Ну тьфу, ллмки, а реально-то что?!
Но предположим столь же иронически, что может быть что-то всё же есть. Ну также как в интернете было изначально что-то интересное и т.п. Мне кажется мой взгляд не содержит неуместного восторга или алармизма по поводу ИИ, укоренён в наблюдаемых фактах (которые я не всегда явно привожу для краткости, особенно если их можно увидеть "посмотрев в окно").
Напомню вайбы канала, которые стараюсь выдерживать, которые служат моей мотивацией:
Собственно хотелось отрефлексировать, в чём пафос моего канала. Думаю, идеальный конечный результат это повышение удачливости (в самом широком смысле) моих читателей. Ведь что такое удача, как не умение своевременно замечать что, что обычно игнорируется, и действовать соответственно? А для того чтобы такое внимание развилось надо коллекционировать штуки, на которые стоит обращать внимание. И иногда чистить пространство восприятия от помех и заслонок, оставленных там по недосмотру или чьей-то злой воле.
Раз уж математиков, консерваторов от природы, проняло, вроде не лишне было бы рационально призадуматься. Может быть прикол-то есть какой-то в "генераторе текста, не способном придумать ничего нового"? Может быть вот эта обязательная ироническая полуулыбка и махание рукой это в данный момент уже не проявление высокого интеллекта, а банальное бумерство? Да ну, ерунда какая-то! :)
❤15👍3🔥3
Вайб-математика и аппаратчики
Эпоха искусственного интеллекта заостряет разделение математики на несколько частей.
Главная и подавляюще распространённая (как по числу математиков, так и по объёму содержания или числу открытий) математика это, назовём так, "вайб-математика" – интуитивная ("неформальная") математика.
Когда лектор пишет что-то на доске, размахивая руками – это вайб-математика. Когда студент решает в тетрадке задания из книги – это вайб-математика. Когда рецензент пишет замечания к статье в журнале – это вайб-математика. Казалось бы, вся математика по такому определению это вайб-математика (т.е. по идее "просто математика"), что не удивительно (вернёмся позже к вопросу иной математики).
Лейденская декларация начинается со слов "технологические разработки постоянно трансформировали практику математики". Однако что эта фраза означает – её авторы, конечно, именно вайб-математики – совершенно не ясно. Как трансформировали-то? Теперь выкладки вместо почтового отправления на лошадях по электронной почте пересылать можно? Вместо меловой доски использовать электронный проектор? Ерунда, никаких трансформирующих вайб-математику технологических разработок за последние 300 лет не было.
Вайб-математику можно назвать особым разделом интроспективной психологии (т.е. тщательным построением и исследованием конструкций ума), или сортом "настольной игры" (т.е. манипуляцией абстрактными объектами по строгим правилам), или художественной литературой определённого жанра (написанием текстов для взаимного развлечения и критики).
Лейденская декларация призывает вайб-математиков сплотиться и... и что делать? Давайте посмотрим отдельные тезисы. Для громкого заявления мирового уровня, которое предполагается обсуждать на всегалактических конгрессах декларация на удивление беззубая, к тому же специфичность предметной области заведомо не вызывает сочувствия у широких кругов населения.
"Искусственный интеллект нарушает авторские права математиков". А авторские права художников, писателей, философов, кого угодно ещё не нарушает? Почему бы не заявить требование что-то с этим сделать глобально и универсально – ну, математики же априори должны иметь тенденцию к максимальному обобщению?
"Искусственный интеллект может использоваться для военных целей". Поэтому надо с ним бороться или по меньшей мере саботировать? Нет, надо "оценивать этические последствия своей работы". Что бы это ни значило на самом деле, по факту прочитывается как "за деньги (и за интересы правильной страны) да".
Триггером публикации декларации, по-видимому, послужило опровержение гипотезы Эрдёша о единичных расстояниях. Пока модели доказывали что-то там своё в коде proof assistants вайб-математики спали спокойно, но как только успешно зашли в их область литературных спекуляций – начали испытывать заметную тревогу.
"Публикуйтесь в рецензируемых журналах, а в блогах не публикуйтесь". Это требование настолько жалкое, что лучше бы уж прямо писали "дайте денег, иначе редакции не на что будет кушать".
Математика всю свою историю была где-то на вершине социальной пирамиды, но почему она там оказалась? Если брать не прикладные разделы, имеющие прямое отношение к народному хозяйству, а так называемую чистую математику (о которой в основном и идёт здесь речь) – то не за счёт ли вайба?
Занятие математикой повышает интеллектуальный уровень, продлевает жизнь, позволяет сохранить здравость рассудка, математические объединения и кружки способствуют росту благосостояния общества, смягчению нравов, налаживанию взаимопонимания.
Вайб-математики должны иметь право на достойный базовый безусловный доход, на самоорганизацию, на доброжелательное и поддерживающее отношение государства и общества. Подобные требования необходимо заявлять прямо и открыто, не прикрывая нелепым шантажом, глупыми смутными угрозами и бюрократической суетой.
Всё то же самое верно для любых творческих профессий – для художников, для литераторов, для разработчиков игр, косплееров, тиктокеров, кого угодно. Вайб-математика это интересно и весело. Да и проблемы-то от ИИ не у них, а у злых дедов-аппаратчиков.
Эпоха искусственного интеллекта заостряет разделение математики на несколько частей.
Главная и подавляюще распространённая (как по числу математиков, так и по объёму содержания или числу открытий) математика это, назовём так, "вайб-математика" – интуитивная ("неформальная") математика.
Когда лектор пишет что-то на доске, размахивая руками – это вайб-математика. Когда студент решает в тетрадке задания из книги – это вайб-математика. Когда рецензент пишет замечания к статье в журнале – это вайб-математика. Казалось бы, вся математика по такому определению это вайб-математика (т.е. по идее "просто математика"), что не удивительно (вернёмся позже к вопросу иной математики).
Лейденская декларация начинается со слов "технологические разработки постоянно трансформировали практику математики". Однако что эта фраза означает – её авторы, конечно, именно вайб-математики – совершенно не ясно. Как трансформировали-то? Теперь выкладки вместо почтового отправления на лошадях по электронной почте пересылать можно? Вместо меловой доски использовать электронный проектор? Ерунда, никаких трансформирующих вайб-математику технологических разработок за последние 300 лет не было.
Вайб-математику можно назвать особым разделом интроспективной психологии (т.е. тщательным построением и исследованием конструкций ума), или сортом "настольной игры" (т.е. манипуляцией абстрактными объектами по строгим правилам), или художественной литературой определённого жанра (написанием текстов для взаимного развлечения и критики).
Лейденская декларация призывает вайб-математиков сплотиться и... и что делать? Давайте посмотрим отдельные тезисы. Для громкого заявления мирового уровня, которое предполагается обсуждать на всегалактических конгрессах декларация на удивление беззубая, к тому же специфичность предметной области заведомо не вызывает сочувствия у широких кругов населения.
"Искусственный интеллект нарушает авторские права математиков". А авторские права художников, писателей, философов, кого угодно ещё не нарушает? Почему бы не заявить требование что-то с этим сделать глобально и универсально – ну, математики же априори должны иметь тенденцию к максимальному обобщению?
"Искусственный интеллект может использоваться для военных целей". Поэтому надо с ним бороться или по меньшей мере саботировать? Нет, надо "оценивать этические последствия своей работы". Что бы это ни значило на самом деле, по факту прочитывается как "за деньги (и за интересы правильной страны) да".
Триггером публикации декларации, по-видимому, послужило опровержение гипотезы Эрдёша о единичных расстояниях. Пока модели доказывали что-то там своё в коде proof assistants вайб-математики спали спокойно, но как только успешно зашли в их область литературных спекуляций – начали испытывать заметную тревогу.
"Публикуйтесь в рецензируемых журналах, а в блогах не публикуйтесь". Это требование настолько жалкое, что лучше бы уж прямо писали "дайте денег, иначе редакции не на что будет кушать".
Математика всю свою историю была где-то на вершине социальной пирамиды, но почему она там оказалась? Если брать не прикладные разделы, имеющие прямое отношение к народному хозяйству, а так называемую чистую математику (о которой в основном и идёт здесь речь) – то не за счёт ли вайба?
Занятие математикой повышает интеллектуальный уровень, продлевает жизнь, позволяет сохранить здравость рассудка, математические объединения и кружки способствуют росту благосостояния общества, смягчению нравов, налаживанию взаимопонимания.
Вайб-математики должны иметь право на достойный базовый безусловный доход, на самоорганизацию, на доброжелательное и поддерживающее отношение государства и общества. Подобные требования необходимо заявлять прямо и открыто, не прикрывая нелепым шантажом, глупыми смутными угрозами и бюрократической суетой.
Всё то же самое верно для любых творческих профессий – для художников, для литераторов, для разработчиков игр, косплееров, тиктокеров, кого угодно. Вайб-математика это интересно и весело. Да и проблемы-то от ИИ не у них, а у злых дедов-аппаратчиков.
👍8🔥8❤6
Математика как верификация научного знания
Антон Русинов (@hyperhistory) комментирует предыдущий пост:
Антон Русинов (@hyperhistory) комментирует предыдущий пост:
Там, кстати, есть проблема даже более существенная, чем чувства людей с учеными степенями. Сама академия — это же центр верификации т.н. объективного знания. Ну типа "глобальное потепление существует" :) Это работает потому что помимо очевидных пропагандистских лозунгов академия занята поддержанием номенклатуры реального знания, и, что важней, имеет на него монополию. Если разрушается монополия на верификацию теорем, то разрушается и монополия на объявление лозунгов "научными фактами". И тут не зря закрутилось именно вокруг математики. Она во-первых сама по себе слишком точная, если доказательство написано — не отвертишься! А во-вторых не требует дорогого оборудования, экспериментов, подтверждения экспериментов и т.п.
Математическое доказательство верифицирует само себя. Максимальный анархизм.
— Глобальное потепление существует
— Кто сказал?
— Ученые!
— Почему им надо верить?
— А они теоремы доказывают. Вот ты доказываешь?
— Да, вот ссылка на мой блог
— РЯЯЯЯ
🔥8👍2
Другая математика (1/2)
(Стоит отметить, что я не специалист в математике, так что дальнейшее, если угодно, можно воспринимать как наивный взгляд со стороны, к которому специалисты могут сделать замечания или целиком опровергнуть.)
Можно провести такую аналогию: математика это блокчейн, у которого есть прикладные и системные (инфраструктурные) компоненты.
Основная работа чистых математиков это что-то вроде майнинга – внешне бессмысленная трата когнитивных усилий по формулировке и поиску решений неких синтетических задач.
В этой аналогии "вайб-математики" и их организации это различные узлы по производству и верификации математического знания. Возмущение внедрению искусственного интеллекта буквально сродни возмущению "расчётчиков" (была такая профессия) переходу на автоматику.
Основой и определяющей чертой любого блокчейна является алгоритм консенсуса, реализующий некий способ того, как распределённая бухгалтерская книга может последовательно накапливать информацию и избегать противоречий (типа "двойных трат" и т.п.).
Консенсусом в математике занимается математическая логика. Учитывая, что математика изначально претендует на некую универсальную абстрактную истину, "много математик" быть не может априори (если смотреть достаточно абстрактно и универсально, то истина по определению единственна).
К началу 20-го века прямой человеческой интуиции перестало хватать для того, чтобы сохранять консенсус имплицитно. Начались поиски оснований математики, в роли которой примерно к 30-м годам XX века закрепилась теория множеств. Что является в значительной мере историческим курьёзом, чем объективно оправданным наилучшим выбором.
Теория множеств (ZFC + FOL) служит чем-то вроде "языка ассемблера", низкоуровневого кода, в который можно потенциально перевести любое математическое утверждение из какой угодно теории. Потенциально можно, но реально этого никто не делает, также как программист, который пишет на языке высокого уровня не интересуется тем, в какие именно команды процессора он будет скомпилирован.
Т.е. математический консенсус равенгипостазии иллюзии существования консенсуса.
А на каком языке высокого уровня реально работает математика?
(Стоит отметить, что я не специалист в математике, так что дальнейшее, если угодно, можно воспринимать как наивный взгляд со стороны, к которому специалисты могут сделать замечания или целиком опровергнуть.)
Можно провести такую аналогию: математика это блокчейн, у которого есть прикладные и системные (инфраструктурные) компоненты.
Основная работа чистых математиков это что-то вроде майнинга – внешне бессмысленная трата когнитивных усилий по формулировке и поиску решений неких синтетических задач.
В этой аналогии "вайб-математики" и их организации это различные узлы по производству и верификации математического знания. Возмущение внедрению искусственного интеллекта буквально сродни возмущению "расчётчиков" (была такая профессия) переходу на автоматику.
Основой и определяющей чертой любого блокчейна является алгоритм консенсуса, реализующий некий способ того, как распределённая бухгалтерская книга может последовательно накапливать информацию и избегать противоречий (типа "двойных трат" и т.п.).
Консенсусом в математике занимается математическая логика. Учитывая, что математика изначально претендует на некую универсальную абстрактную истину, "много математик" быть не может априори (если смотреть достаточно абстрактно и универсально, то истина по определению единственна).
К началу 20-го века прямой человеческой интуиции перестало хватать для того, чтобы сохранять консенсус имплицитно. Начались поиски оснований математики, в роли которой примерно к 30-м годам XX века закрепилась теория множеств. Что является в значительной мере историческим курьёзом, чем объективно оправданным наилучшим выбором.
Теория множеств (ZFC + FOL) служит чем-то вроде "языка ассемблера", низкоуровневого кода, в который можно потенциально перевести любое математическое утверждение из какой угодно теории. Потенциально можно, но реально этого никто не делает, также как программист, который пишет на языке высокого уровня не интересуется тем, в какие именно команды процессора он будет скомпилирован.
Т.е. математический консенсус равен
А на каком языке высокого уровня реально работает математика?
🔥9❤3👍2
Другая математика (2/2)
Для обычных математиков тот язык, на котором они реально работают, это естественный язык (русский, английский и т.д.).
Для математических логиков такое положение дел не является приемлемым. Создаются разнообразные теории, находящиеся в активной разработке и идущие на острие прогресса: логики высших порядков, теории типов, все эти HoTT, HOTT и SIP, множество разработок в области теории категорий и др.
Не в малой мере рост интереса к математической логике вызван популяризацией proof assistants – языков программирования, выступающих в роли систем автоматизации математических доказательств (которые в свою очередь стали популярны на волне ИИ – общая идея захода в том, чтобы создать периметр безопасности/уверенности средствами формальной верификации, внутри которых ИИ мог бы искать оптимальное решение, гарантированно не нарушая заданные правила).
Развитие математических теорий начинает идти по законам развития компьютерных систем, накопление знания соответствует росту кода библиотек, организация изложения материала превращается в дизайн архитектуры кода, декомпозицию модулей и стиль кодирования.
Компьютеры стали неотъемлемой частью быта каждого человека, одновременно компьютерные алгоритмы стали метафорами, которыми мы живём – элементом культуры и ментальности. Математики беспомощно проспали этот момент, но математические логики давно были готовы, придумав современные передовые парадигмы языков программирования на сто лет заранее.
Лейденский манифест де-факто приравнивает использование пруф-ассистентов к ИИ, ну какие-то технические штуки там, не то что наше, кондовое, читать тексты на бумаге и прямым озарением верифицировать верность написанного. При этом совершенно не понимая что в этот момент происходит, что сами делают – что вот эта подстановка "по определению" это альфа-эквивалентность, что вот это упрощение выражения это бета-редукция, и что вот этот перенос доказательств вдоль изоморфизма это вообще что-то из гомотопической теории типов.
Компьютеры и ИИ подсветили логические дыры в рассуждениях, но вообще-то преодоление этих дыр и есть суть математики.
"Другая математика" это, в данный момент, всевозможные варианты математической логики. Если бы математика была серьёзной наукой, а не способом времяпрепровождения в своё удовольствие, усилия, вкладываемые в развитие логики, были бы на порядок выше.
Если бы математики всерьёз писали декларацию будущего это была бы очередная программа о следующих ста годах развития математической логики. Единственно важный вопрос гуманитарных наук это вопрос об устройстве самого человека. Единственно важный вопрос математики, следовательно, это вопрос совершенствования математической логики – как дисциплины, моделирующей особенную часть человеческой рациональности.
Какой единственно важный вопрос ИИ? Дилемма здесь не в том, будет ли внедрятся ИИ или нет, этот момент давно пройден и упущен. Дилемма в том сколько будет в нём чего-то тёплого и лампового. За это можно было бы побороться, но едва ли на столь абстрактную цель удастся отвлечься от насущных вопросов грантов, журнальных рейтингов, борьбы с блогами, оценки рисков окружающей среде и всех прочих повышения удоев и измерения площадей полей, к чему Лейденская декларация редуцирует деятельность своих подписантов.
Для обычных математиков тот язык, на котором они реально работают, это естественный язык (русский, английский и т.д.).
Для математических логиков такое положение дел не является приемлемым. Создаются разнообразные теории, находящиеся в активной разработке и идущие на острие прогресса: логики высших порядков, теории типов, все эти HoTT, HOTT и SIP, множество разработок в области теории категорий и др.
Не в малой мере рост интереса к математической логике вызван популяризацией proof assistants – языков программирования, выступающих в роли систем автоматизации математических доказательств (которые в свою очередь стали популярны на волне ИИ – общая идея захода в том, чтобы создать периметр безопасности/уверенности средствами формальной верификации, внутри которых ИИ мог бы искать оптимальное решение, гарантированно не нарушая заданные правила).
Развитие математических теорий начинает идти по законам развития компьютерных систем, накопление знания соответствует росту кода библиотек, организация изложения материала превращается в дизайн архитектуры кода, декомпозицию модулей и стиль кодирования.
Компьютеры стали неотъемлемой частью быта каждого человека, одновременно компьютерные алгоритмы стали метафорами, которыми мы живём – элементом культуры и ментальности. Математики беспомощно проспали этот момент, но математические логики давно были готовы, придумав современные передовые парадигмы языков программирования на сто лет заранее.
Лейденский манифест де-факто приравнивает использование пруф-ассистентов к ИИ, ну какие-то технические штуки там, не то что наше, кондовое, читать тексты на бумаге и прямым озарением верифицировать верность написанного. При этом совершенно не понимая что в этот момент происходит, что сами делают – что вот эта подстановка "по определению" это альфа-эквивалентность, что вот это упрощение выражения это бета-редукция, и что вот этот перенос доказательств вдоль изоморфизма это вообще что-то из гомотопической теории типов.
Компьютеры и ИИ подсветили логические дыры в рассуждениях, но вообще-то преодоление этих дыр и есть суть математики.
"Другая математика" это, в данный момент, всевозможные варианты математической логики. Если бы математика была серьёзной наукой, а не способом времяпрепровождения в своё удовольствие, усилия, вкладываемые в развитие логики, были бы на порядок выше.
Если бы математики всерьёз писали декларацию будущего это была бы очередная программа о следующих ста годах развития математической логики. Единственно важный вопрос гуманитарных наук это вопрос об устройстве самого человека. Единственно важный вопрос математики, следовательно, это вопрос совершенствования математической логики – как дисциплины, моделирующей особенную часть человеческой рациональности.
Какой единственно важный вопрос ИИ? Дилемма здесь не в том, будет ли внедрятся ИИ или нет, этот момент давно пройден и упущен. Дилемма в том сколько будет в нём чего-то тёплого и лампового. За это можно было бы побороться, но едва ли на столь абстрактную цель удастся отвлечься от насущных вопросов грантов, журнальных рейтингов, борьбы с блогами, оценки рисков окружающей среде и всех прочих повышения удоев и измерения площадей полей, к чему Лейденская декларация редуцирует деятельность своих подписантов.
🔥9👍6
Логика как "операционная система" для математики
Всеволод Яшин (специалист по квантовой физике/теории информации) комментирует предыдущий пост:
Всеволод Яшин (специалист по квантовой физике/теории информации) комментирует предыдущий пост:
Хочу уточнить по поводу ценности логики и выступить в поддержку "вайб-математики".
Аналогия с программированием компьютеров может быть высказана следующая: логика -- это создание операционных систем (в принципе, начиная с ассемблера до настройки оконного менеджера); вайб-математика -- это написание рабочих программ. Зачастую эти две области связаны и в каких-то местах идентичны, но у них разное мотивирование. Операционные системы создаются для того, чтобы запускать на них программы -- формальные системы дедукции создаются для того, чтобы формулироваь в них теоремы. Программы реализуются внутри операционной системы, но они самоценны, и если что их можно переписать под другую ОС -- точно так же с математическими теориями.
Логика -- важнейшая часть математики. Но операционные системы без интересных программ не нужны (есть много примеров таких ОС!). Кроме того, во многих задачах полезны минималистичные операционные системы, и на какие-то баги операционных систем можно не обращать внимания. Усложнение структуры логики позволяет удобно работать с трудными математическими теориями, но разрабатывать сверхмудрённую операционную систему без прямой необходимости не нужно и вредно.
И ещё, компьютерные алгоритмы тоже изначально пишутся на естественном языке!
❤3👍3🔥3
Логика как основа логики
Ранее Александр Грызлов (специалист по логике и, в частности, теории типов; автор @covalue), отвечая на комментарий Антона Русинова, писал:
Ранее Александр Грызлов (специалист по логике и, в частности, теории типов; автор @covalue), отвечая на комментарий Антона Русинова, писал:
Если совсем уже придираться, то "верифицирует сама себя" логика, математики одновременно логиков побаиваются и ими пренебрегают. Логики исторически как раз тесно были связаны с вычислительной техникой, и при этом зачастую под конец жизни слетали с катушек (Кантор, Гёдель, Тюринг, Пост).
🔥5👍3
"Вайб-математика" как коллекция математических интуиций
Если основаниями математики занимается логика, то что занимается основаниями логики? Та же логика. В основании разработки операционных систем – использованная в комментарии аналогия – получается тоже, в общем-то, лежит математическая логика (в самом широком смысле – а у неё именно такой смысл по умолчанию и есть) :)
"Синтетический метод", т.е. разработка "маленьких логических фреймворков" под конкретные математические области, опирается в свою очередь на некие "методы разработки логических фреймворков". Что тоже является предметной областью математической логики. Такие "мини-фреймворки" по сути становятся "DSL", domain specific languages, в рамках некоего мета-логического (т.е. просто логического – "мета" в таком сочетании можно сокращать) "языка программирования".
Как заметили выше, у конкретных областей математики есть свои внутренние основы, не сводящиеся к логической формализации – также как у конкретных прикладных компьютерных программ есть внутренний смысл, который было бы не естественно редуцировать до некоей последовательности вызовов API операционной системы.
Главная задача этих конкретных областей в момент смены эпох, однако, мне кажется что та же самая – приращение "ламповой человечности" (которая в значительной мере недоступна современным ИИ – в основном из-за низкой "кросс-модальной" мощности).
Проще говоря, основой "вайб-математики" является прирост именно неформального знания, "математических интуиций". Эталонным форматом фиксации таких интуиций являются видеозаписи в стиле 3b1b. (Конечно, сейчас этот формат далеко не совершенный – нужна большая интерактивность, динамичность и конфигурируемость.)
"Вайб-математика" это, содержательно, коллекция вдохновляющих динамических иллюстраций. Иллюстраций, позволяющих напрямую прикоснуться к оригинальной ментальности математиков, погруженных в ту или иную предметную область.
Если основаниями математики занимается логика, то что занимается основаниями логики? Та же логика. В основании разработки операционных систем – использованная в комментарии аналогия – получается тоже, в общем-то, лежит математическая логика (в самом широком смысле – а у неё именно такой смысл по умолчанию и есть) :)
"Синтетический метод", т.е. разработка "маленьких логических фреймворков" под конкретные математические области, опирается в свою очередь на некие "методы разработки логических фреймворков". Что тоже является предметной областью математической логики. Такие "мини-фреймворки" по сути становятся "DSL", domain specific languages, в рамках некоего мета-логического (т.е. просто логического – "мета" в таком сочетании можно сокращать) "языка программирования".
Как заметили выше, у конкретных областей математики есть свои внутренние основы, не сводящиеся к логической формализации – также как у конкретных прикладных компьютерных программ есть внутренний смысл, который было бы не естественно редуцировать до некоей последовательности вызовов API операционной системы.
Главная задача этих конкретных областей в момент смены эпох, однако, мне кажется что та же самая – приращение "ламповой человечности" (которая в значительной мере недоступна современным ИИ – в основном из-за низкой "кросс-модальной" мощности).
Проще говоря, основой "вайб-математики" является прирост именно неформального знания, "математических интуиций". Эталонным форматом фиксации таких интуиций являются видеозаписи в стиле 3b1b. (Конечно, сейчас этот формат далеко не совершенный – нужна большая интерактивность, динамичность и конфигурируемость.)
"Вайб-математика" это, содержательно, коллекция вдохновляющих динамических иллюстраций. Иллюстраций, позволяющих напрямую прикоснуться к оригинальной ментальности математиков, погруженных в ту или иную предметную область.
🔥8👍5❤1