Доказательство оптимальности упаковки 11 квадратов прошло проверку в Lean
AI-assisted proof of optimal packing for 11 squares
Полное доказательство оптимальности упаковки 11 квадратов формализовано в Lean и успешно прошло верификацию: все 7920 локальных модулей приняты, финальный аудит не выявил ни одного допущения. Оптимальная длина стороны выражается через корень многочлена 8-й степени и приблизительно равна 3.8770835900228141773. Модель допускает произвольные ориентации квадратов, легальные касания границ и непересекающиеся открытые внутренности. Для воспроизведения проверки достаточно выполнить скрипт run_verification.sh.
Полное доказательство оптимальности прошло верификацию с нативными числовыми сертификатами.
- golden-face
Мне потребовалось немало времени, чтобы понять, что на самом деле означает упаковка квадратов (статья в Wiki даёт понимание), но если кратко: это упаковка единичных квадратов (1x1) в больший квадрат произвольного размера. Когда длина стороны большего квадрата не является целым числом, становится нетривиальной задачей определить, сколько единичных квадратов 1x1 можно разместить/упаковать внутри.
- DevelopingElk
Я работаю над воспроизведением доказательства с некоторыми личными изменениями. Базовый подход — стандартный компьютерно-ассистированный метод «неизбежного множества». Сначала выбираются некоторые области, достаточно маленькие, чтобы центры двух квадратов не поместились в одну область; в статье использовалось 16. Каждая область должна содержать или не содержать квадрат, что даёт 16 выбрать 11 случаев, примерно 2000. Для каждого случая вы пытаетесь его исключить. Вы делаете это, определяя области, которые должны быть покрыты квадратом, и распространяя эту информацию. Вы также можете использовать упаковочные LP, как это делал Стромквист в 1989 году, чтобы исключить больше конфигураций. Затем вы сужаете оставшиеся случаи и разбиваете их дальше.
Я думаю, единственная причина, по которой это не было сделано до ИИ, — это то, что тема не была предметом серьёзного внимания. Компьютеры 1989 года были слишком слабы, чтобы обработать все случаи. Но все основные ингредиенты присутствовали в доказательстве гипотезы Кеплера. Что сделал ИИ, так это снизил необходимые усилия настолько, что любители, которым просто нравилась упаковка квадратов, смогли выполнить и формально проверить такое доказательство. Я считаю себя одним из таких любителей. Так что это не случай, когда ИИ крадёт доказательства математиков или делает что-то сверхчеловеческое, это случай демократизации. Я обеспокоен тем, как ИИ влияет на математику и как ведут себя компании, занимающиеся ИИ, но это не тот случай, о котором стоит беспокоиться. Вычисления для доказательства оптимальности этой конфигурации всегда будут слишком большими, чтобы их можно было проверить вручную. Однако я надеюсь создать несколько хороших визуализаций упаковочного LP или перекрытия ядра […]
- dkural
Это не так произвольно или уродливо, как может показаться на первый взгляд — см. изображение здесь и объяснение: https://x.com/davidmbudden/status/2107646435659481548
- yzydserd
к сведению: основной сайт по упаковке квадратов в квадраты находится по адресу https://kingbird.myphotos.cc/packing/squares_in_squares.html
Треугольный вид наиболее интересен. И 20-минутное видео об этом виде доступно по ссылке
- WithinReason
Список многих упаковок квадратов с изображениями: