El repositorio 11SquaresFormalized documenta la verificación formal completa de la prueba de optimidad del empaquetado de 11 cuadrados, utilizando el lenguaje de verificación Lean 4. El proyecto ha superado la verificación con certificados numéricos nativos, aceptando todas las 7.920 módulos locales sin admitencias en los informes de auditoría. Esta formalización integra pruebas geométricas exactas y constructos numéricos, confiando en el núcleo de Lean y el compilador nativo, lo que permite una validación rigurosa de la solución óptima.
La solución óptima se define por la longitud de lado T, que depende de la única raíz u de la ecuación polinómica 5u^8-10u^7-2u^6+14u^5+12u^4-6u^3+2u^2+2u-1=0, situada en el intervalo (9/25, 37/100). El modelo geométrico permite orientaciones arbitrarias y contacto legal en los bordes, alcanzando una densidad aproximada de 3.8770835900228141773. El código está estructurado en archivos Lean que cubren fundamentos geométricos, interfaces de interacción con herramientas de verificación y teoremas de optimidad incondicional.
El proyecto fija la versión de Lean 4.34.1 y una revisión específica de Mathlib. Incluye scripts de ejecución para Linux y macOS que permiten la verificación completa mediante el comando run_verification.sh, requiriendo un entorno con Python 3, Git y curl. La documentación detalla los requisitos de hardware, el uso de elan para macOS y las instrucciones para reproducir la verificación sin errores. Este trabajo representa un avance significativo en la aplicación de la verificación formal a problemas geométricos complejos, ofreciendo una base matemática verificada y reproducible para la comunidad de investigación en ciencias de la computación y matemáticas.