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

Кевин Баззард (говорили про него раньше) в числе подписантов "Лейденской декларации об ИИ и математике".

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

В 2026 году пишет: "техногиганты лезут к нам в математику, да что ж творят-то, караул!". А кто им дверь открыл и ковёр постелил? :)

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

Главная мысль декларации примерно такая: во-первых, гопатыч ничего не может и плохо работает; во-вторых, кто ж нам теперь будет деньги платить, если мы срочно не начнём его саботировать?

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