📌
Palomar - реестр проверенных LEAN-доказательств
Последние месяцы доказательства, сгенерированные ИИ, посыпались валом как для новых результатов, так и для старых, причем часть из них формализована на Lean и проверить такой репозиторий непросто, особенно если ты не эксперт. Нужно убедиться:
🟠что заявленные формальные утверждения действительно имеют доказательства, проходящие проверку типов;
🟠что в доказательствах нет жульничества;
🟠что формальные утверждения по смыслу совпадают с тем, что описано словами.
Под эту задачу и Теренс Тао запустил
Palomar - реестр математики, верифицированной на Lean. Инициативу вырастили
Lean FRO и
ICARM.
Прием заявок уже идет, чтобы в него попасть, в репозитории должно быть три вещи:
🟢challenge file с коротким и читаемым человеком описанием заявленных результатов на Lean;
🟢solution module с доказательством любой длины;
🟢файл
formalization.yaml, где те же результаты изложены обычным языком и собраны метаданные и раскрытия.
Снимок поданного репозитория проверяют двумя этапами.
Сначала инструмент
Comparator смотрит, что solution module типизируется и доказывает ровно то, что заявлено в challenge file. После этого языковая модель сверяет, похоже ли неформальное описание в на то, что заявлено формально.
Прошел оба - попал в реестр. Принимают формализации и старых результатов, и новых. Кто автор доказательства - человек, ИИ или оба вместе - значения не имеет.
@ai_machinelearning_big_data
#news #ai #ml
