ПостЛейденская декларация математиков против LLM-ок

Лейденская декларация математиков против LLM-ок Кевин Баззард (говорили про него раньше) в числе подписантов "Лейденской декларации об ИИ и математике". Ещё в 2020 году объявил проект по дешёвому сбору данных для обучения ИИ – заставлять бакалавров математики переводить стандартный материал курсов на Lean. На этой волне и стал мировой знаменитостью. В 2026 году пишет: "техногиганты лезут к нам в математику, да что ж творят-то, караул!". А кто им дверь открыл и ковёр постелил? :) Саму декларацию подписало тысячи людей (подписать можно легко онлайн), среди которых несколько лауреатов Филдсовской премии и прочих выдающихся специалистов. Главная мысль декларации примерно такая: во-первых, гопатыч ничего не может и плохо работает; во-вторых, кто ж нам теперь будет деньги платить, если мы срочно не начнём его саботировать? В общем-то декларации писать поздно, так как вопрос с "доказательством теорем" закрыт. Ну, программисты точно такие же переживания испытали уже год-два назад.