수학 난제였던 '정사각형 11개 최적 포장' 문제, AI·수학 증명 도구로 완전 검증 성공

요약 수학계에서 오랜 시간 난제로 꼽히던 정사각형 패킹 문제 중 하나인 '11개 정사각형의 최적 패킹(11 square packing)' 증명이 대화형 정리 증명기 린(Lean)을 통해 공식 검증을 통과했습니다. 이번에 공개된 깃허브 저장소(11SquaresFormalized)에 따르면, 총 7,920개의 로컬 린 모듈 전체가 검증을 통과했으며 미해결 가정(admission)이 전혀 없는 완전한 검증 결과를 기록했습니다. 이번 형식화 증명에서는 기하학적 논증과 체커의 건전성, 전체 증명 조립은 린의 일반적인 정리 증명을 유지하면서도, 계산량이 방대하고 정밀한 수치 인증서 검증에는 네이티브 컴파일러를 활용하는 방식을 채택했습니다. 이에 따라 최종 정리는 린 커널과 네이티브 컴파일러를 신뢰 모델로 삼아 성립되었습니다. 연구진이 제시한 11개 단위 정사각형을 담을 수 있는 가장 작은 큰 정사각형의 한 변의 길이는 약 3.8770835900228141773으로 도출되었습니다. 이는 특정 8차 방정식의 유일한 근을 바탕으로 정밀하게 계산된 수치이며, 임의의 회전 각도와 경계면 접촉을 허용하는 조건 아래에서 더 이상 줄일 수 없는 절대적인 최적값임이 입증되었습니다. 연구진은 린 4.34.1 버전 및 Mathlib 고정 리비전을 사용해 누구나 검증 스크립트를 재현할 수 있도록 빌드 구성을 함께 공개했습니다.