dxdt.blog: занимательный интернет-журнал

Кто бы сомневался, но, как и следовало ожидать, в октябрьском обновлении “Коуровской тетради” много задач, явно отмеченных как решённые “с использованием AI”. Есть там среди многих и решение для задачи 11.115 (“unverified AI solution”), про которую я писал: точно тот же контрпример, что упоминается и на dxdt.blog, но в записке про то, как я проверял возможности Claude Fable 5/Opus 5 по конструированию контрпримеров сразу с доказательством на Lean. У меня используется квадрат элемента группы, а в опубликованном контрпримере (M. Kinyon, J. Urban) – указана степень m≥2 – понятно, что m == 2 подходит. Цитата из моей записки:

[…] если кому-то интересны супертехнические подробности, то вот: построим подгруппу на словах с чётными и нечётными степенями (это отображение в Z/2Z), и подгруппу на соотношениях с a^2.

Надо заметить, что формулировку контрпримера, найденного Claude, я вводил и в ChatGPT. Я, конечно, найденный LLM контрпример никуда не отправлял (ну, кроме ChatGPT), так что понять, откуда результат взялся в выдаче LLM, как там пересеклись входные “промпты” от разных пользователей, – могут только операторы этих LLM. Но вот в том, что возможно найти контрпримеры для огромного количества старых задач с помощью LLM, при участии большого количества пользователей, задающих направления, – в этом я не сомневаюсь, а про “Коуровскую тетерадь”, как источник таких задач для LLM, я писал ещё в 2024 году (но это совершенно очевидный для специалиста выбор). Вот, кто-то занялся вплотную. Собственно, именно этот момент, взятый по модулю способа публикации (ну, представьте, что решения произвольно публикуются на персональных сайтах), и беспокоит сообщество.

Адрес записки: https://dxdt.blog/2026/10/01/19346/