Создатель сайта задач Эрдёша остановил приём ИИ-доказательств

Математик Томас Блум, создатель сайта erdosproblems.com — сайта со списком нерешённых задач математика Пола Эрдёша, — перестал принимать новые решения и комментарии к задачам. Сайт работает с мая 2023 года, когда на нём было около 200 задач. Сейчас их 1221, комментариев — больше 9000, зарегистрированных пользователей — почти 2000, а посетителей — от 10 000 до 25 000 в день. Блум говорит, что раздел комментариев заполнился доказательствами, сгенерированными ИИ, без каких-либо объяснений. Люди стали постить их в основном, чтобы застолбить приоритет, и настоящее обсуждение задач почти исчезло.

Блум не запрещает ИИ. Он убирает только витрину: сайт больше не помечает статус задачи как решённой и не засчитывает результат — ни человеку, ни ИИ, — если доказательство не сопровождается понятным объяснением. Доказательства с чётким письменным объяснением получат приоритет, когда Блум вручную обновляет страницы задач. Приоритет получат и формальные доказательства на Lean — формате, который компьютер может проверить строка за строкой. Их нужно зарегистрировать в Palomar — реестре, который подтверждает, что такие доказательства корректно компилируются. Голый вывод ИИ без объяснения рассматривается как непротестированный код: в продакшен он не идёт.