Формално математическо доказателство в Lean 4 за оптимално опаковане на 11 квадрата

Снимка: Wikimedia Commons / Jérémy Barande

В забележителен пробив на пресечната точка между дискретната геометрия и компютърните науки, международен изследователски екип обяви цялостно, машинно проверено доказателство на езика Lean 4 за оптималното опаковане на 11 единични квадрата в квадратен контейнер [1].

Проблемът, формулиран преди десетилетия от математика Пол Ердьош и редица геометрии, оставаше нерешен за случая с $n=11$ поради изключително сложните непрекъснати ротации и неконвексни пространства от възможни състояния. Чрез комбиниране на невронни евристики и интервална аритметика екипът успя да сведе безкрайното пространство от конфигурации до формално доказателство, валидирано от ядрото на Lean [1].

Инфографика: Светни.ме

Преодоляване на непрекъснатото търсене чрез интервални клонове

В математиката опаковането на квадрати е значително по-трудно от опаковането на окръжности, тъй като всеки квадрат притежава ориентация (ъгъл на завъртане). За $n=11$ най-добрата известна конфигурация имаше страна на контейнера от приблизително 3.87708 единици, но никой не бе успял да докаже аналитично, че не съществува по-плътно разположение [1].

Изследователите разработиха хибридна система: невронна мрежа предлагаше критичните точки и конфигурационни ограничения, докато алгоритъм тип branch-and-bound систематично разделяше пространството от ъгли и координати на малки кубове. Всеки сектор се валидираше чрез строги неравенства в реалните числа, формализирани в Lean 4, изключвайки възможността за съществуване на по-добро решение в областта на геометричната оптимизация.

Триумф на формалната верификация

Значението на този резултат надхвърля конкретната задача за 11-те квадрата. В миналото компютърно подпомагани доказателства (като това за проблема с четирите цвята или хипотезата на Кеплер) бяха посрещани със скептицизъм от математическата общност, тъй като изискваха хиляди редове непроверени C++ скриптове.

С използването на формална верификация целият математически апарат е кодиран в теория на типовете, където проверката се извършва от малко и независимо ядро. Ако Lean 4 приеме доказателството, вероятността за грешка е сведена до нула.

Дълбок технически анализ: От геометрични загадки към автоматизирано проектиране на микрочипове

Макар опаковането на квадрати да звучи като абстрактна математическа главоблъсканица, зад него стоят колосални индустриални приложения. Същият математически апарат управлява топологичното проектиране на интегрални схеми (VLSI floorplanning), където милиарди транзисторни блокове и макроси трябва да бъдат разположени върху кремъчната пластина с минимално празно пространство и оптимална дължина на проводниците.

Победата на машинно асистираното доказателство в Lean 4 доказва, че формалните верификатори са узрели за решаване на задачи от реалния свят. Вместо да разчитат на непълни приближения и евристики, инженерите на бъдещето ще могат да използват AI системи, които не просто проектират сложни хардуерни оформления или логистични контейнери, но и предоставят математически сертифицирана гаранция, че решението е теоретично неподобримо.

Източници

[1]: AI-assisted proof of optimal packing for 11 squares - GitHub