11개의 단위 정사각형을 더 큰 정사각형 안에 넣는 문제에서 최소 크기의 외곽 정사각형이 무엇인지에 대한 수학적 논쟁이 새로운 국면을 맞았습니다. Walter Trump이 1979년에 발견한 배열이 실제로 최적인지 확인하는 과정에 인공지능 시스템이 직접 참여했고, 그 결과가 형식적 검증 언어인 Lean을 통해 완전히 증명된 상태입니다.
해당 프로젝트는 2026년 10월 6일 GitHub 저장소 ’11SquaresFormalized’를 통해 공개되었습니다. 저장소에는 총 7,920개의 Lean 모듈이 포함되어 있으며, 최종 감사 결과 모든 모듈이 오류 없이 검증되었습니다. 또한 증명 과정에서 임의의 가정을 받아들여야 하는 ‘admission’은 단 한 건도 발생하지 않았습니다.
증명 대상이 된 배열은 외곽 정사각형의 변 길이가 약 3.87708359002281인 구조입니다. 이 값이 11개의 정사각형을 담을 수 있는 가장 작은 크기임을 컴퓨터 보조 증명을 통해 확립했습니다. 프로젝트에는 인간 협업자들과 함께 OpenAI의 Astra와 Anthropic의 Claude가 직접 기여자로 명시되어 있습니다.
기존 수학계에서는 이러한 복잡한 조합론적 문제를 해결하기 위해 ‘피할 수 없는 집합(unavoidable set)’ 접근법을 사용해 왔습니다. 두 정사각형의 중심이 같은 영역에 들어갈 수 없을 정도로 공간을 세분화하고, 각 경우의 수를 배제하는 방식입니다. 1989년에는 Stromquist가 선형 계획법(LP)을 활용해 일부 구성을 배제한 바 있지만, 당시 컴퓨터 성능으로는 전체 경우의 수를 처리하기 어려웠습니다.
이번 사례에서 AI의 역할은 기존 방법론의 자동화와 효율화에 집중되었습니다. Hacker News 커뮤니티의 한 참여자는 이번 작업이 AI가 수학자의 역할을 대체한 것이 아니라, 개인 연구자들이 복잡한 검증을 수행할 수 있도록 진입 장벽을 낮춘 ‘민주화’의 예라고 평가했습니다. 과거 케플러 추측 증명에서도 유사한 컴퓨터 보조 기법이 사용되었으나, 이번처럼 소규모 팀이나 개인이 전체 증명을 형식적으로 완성한 경우는 드물었습니다.
다만 이 증명은 여전히 계산량이 방대하여 인간이 손으로 일일이 확인할 수 없는 형태입니다. 따라서 신뢰성은 Lean과 같은 형식 검증 도구의 정확성에 의존합니다. 현재까지 공개된 자료는 해당 저장소의 검증 상태를 명확히 하고 있으나, 다른 유사 난제들에 대한 AI 기반 증명의 일반화 가능성은 아직 입증되지 않은 상태입니다.