Naukowcy udowodnili formalnie optymalny algorytm pakowania 11 kwadratów w jednostkowy kwadrat przy wsparciu sztucznej inteligencji. Dowód został całkowicie sformalizowany i opublikowany na GitHub, co stanowi znaczący krok w automatyzacji matematycznych weryfikacji za pomocą narzędzi AI.
Problemy pakowania geometrycznych figur należą do klasyki zagadnień optymalizacyjnych o ogromnym praktycznym znaczeniu. Są wykorzystywane w logistyce, planowaniu rozmieszczenia, produkcji i wielu dziedzinach inżynierii. Poszukiwanie optymalnych rozwiązań dla takich problemów jest tradycyjnie bardzo czasochłonne i wymaga połączenia intuicji matematycznej z obliczeniami komputerowymi.
Zastosowanie AI do formalnego dowodzenia matematycznych twierdzeń ma głębokie implikacje. Pozwala nie tylko na odkrywanie rozwiązań, ale przede wszystkim na ich automatyczną weryfikację w rygorystycznym formalnym systemie. To otwiera drogę do bardziej systematycznego podejścia do trudnych problemów kombinatorycznych i geometrycznych. Projekt pokazuje, jak narzędzia AI mogą wspierać matematyków w procesie formalnego dowodzenia, potencjalnie przyspieszając odkrycia w działalach wymagających precyzyjnych weryfikacji.