Astra и Claude доказали оптимальность наилучшей известной упаковки 11 квадратов (формализовано в Lean)

ИИ-модели Astra и Claude совместно с математиками доказали, что известное решение задачи упаковки 11 квадратов является оптимальным. Результат был формализован в доказательном ассистенте Lean, что демонстрирует новые возможности ИИ в решении сложных комбинаторных задач и верификации математических теорем.