La prueba de optimalidad para empaquetar 11 cuadrados supera la verificación en Lean
AI-assisted proof of optimal packing for 11 squares
El repositorio 11SquaresFormalized presenta una formalización completa en Lean de la prueba de optimalidad para el empaquetado de 11 cuadrados. La verificación aceptó los 7920 módulos locales de Lean y no reportó admisiones. La longitud óptima del lado es aproximadamente 3.8770835900228141773, expresada mediante una raíz algebraica. El modelo permite orientaciones arbitrarias y contacto en los límites. La prueba final confía en el kernel de Lean y el compilador nativo, no solo en el kernel.
La longitud óptima del lado es T = (6u+4)/(1+2u-u^2), donde u es la única raíz en (9/25,37/100) de 5u^8-10u^7-2u^6+14u^5+12u^4-6u^3+2u^2+2u-1=0.
- golden-face
Me tomó un buen rato entender qué significa realmente el empaquetamiento de cuadrados (la Wiki es esclarecedora), pero en resumen: se trata de empaquetar cuadrados unitarios (1x1) dentro de un cuadrado más grande de tamaño arbitrario. Cuando el cuadrado más grande tiene una longitud de lado que no es un número entero, se vuelve no trivial determinar la mayor cantidad de cuadrados de 1x1 que se pueden colocar dentro/empaquetar.
- DevelopingElk
Estoy trabajando en una reproducción de la prueba con algunos cambios personales. El enfoque básico es el estándar de "conjunto inevitable" asistido por computadora. Primero, se eligen algunas regiones lo suficientemente pequeñas como para que los centros de dos cuadrados no quepan en la misma región; el artículo usó 16. Cada región debe contener o no contener un cuadrado, lo que da 16 elige 11 casos, alrededor de 2000. Para cada caso intentas descartarlo. Esto se hace identificando áreas que deben estar cubiertas por un cuadrado y propagando esta información. También puedes usar LPs de empaquetamiento como hizo Stromquist en 1989 para descartar más configuraciones. Luego te enfocas en los casos restantes y los subdivides más.
Creo que la única razón por la que esto no se hizo antes de la IA fue porque no era un tema de interés serio. Las computadoras de 1989 eran demasiado débiles para manejar todos los casos. Pero todos los ingredientes básicos estaban presentes en la prueba de la conjetura de Kepler. Lo que hizo la IA fue reducir el esfuerzo lo suficiente como para que aficionados a los que simplemente les gustaba el empaquetamiento de cuadrados pudieran realizar y verificar formalmente tal prueba. Me considero entre esos aficionados. Así que este no es un caso de IA robando pruebas de matemáticos, o haciendo algo sobrehumano, es un caso de democratización. Me preocupa cómo la IA está afectando las matemáticas y cómo se están comportando las empresas de IA, pero este no es el caso que debería preocuparnos. Los cálculos para probar que este arreglo es óptimo siempre serán demasiado grandes para ser verificados a mano. Sin embargo, espero producir algunas visualizaciones agradables del LP de empaquetamiento o la superposición central […]
- dkural
No es tan arbitrario o feo como puede parecer a primera vista; mira la imagen aquí y la explicación: https://x.com/davidmbudden/status/2107646435659481548
- yzydserd
por si acaso, el sitio principal para el empaquetamiento de cuadrados en cuadrados está en https://kingbird.myphotos.cc/packing/squares_in_squares.html
La vista triangular es la más interesante. Y hay un video de 20 minutos sobre esta vista en
- WithinReason
Una lista de muchos empaquetamientos de cuadrados, con imágenes: