29 сентября 2026 г.
ИИ помог найти фигуру без повторов: Chair44 заполняет трёхмерное пространство
16 сентября GPT-6 Astra помогла Иоаннису Циокосу найти Chair44: фигуру из 7 кубов с доказательством в Lean.
В 1960-х Роберту Бергеру понадобилось больше 20 тысяч плиток, в 1970-х Роджер Пенроуз сократил набор до двух, а в 2023 году Дэвид Смит нашёл плоскую «шляпу». Теперь копии одной Chair44 заполняют трёхмерное пространство без зазоров и повторов.
Проверка без установки. В репозитории автора есть локальный viewer и notebook для Google Colab или Jupyter. Полная Lean-сборка требует 4 CPU, 16 ГБ RAM и 32 ГБ диска, а у автора заняла 26 минут 53 секунды при пике 9,8 ГБ RAM. GPT-6 Astra доступна в Codex CLI 0.153.0 и новее, а API стоит $10 за миллион входных и $50 за миллион выходных токенов.
21 сентября Хаим Гудман-Страусс опубликовал отдельный препринт с более ясным описанием Chair44.
Первоисточник