11개 정사각형 최적 배치 증명, AI 보조로 완성
원제 AI-assisted proof of optimal packing for 11 squares
115 포인트댓글 53
Key Point
최적화 문제의 엄밀한 증명에 AI 보조 도구와 형식 검증이 어떻게 결합되는지 보여주는 사례로, 수학적 추측을 기계 검증 가능한 형태로 변환하는 최신 방법론을 시연한다.
핵심 요약
- Lean 형식 검증을 통해 11개 정사각형의 최적 배치 문제에 대한 완전한 증명을 완성했다.
- 7,920개 지역 Lean 모듈을 EvolvingPrograms 검증 시스템으로 검증했으며 모든 감사에서 오류가 0건이다.
- 최적 한 변의 길이는 T = (6u+4)/(1+2u-u²) 형태이며, u는 방정식 5u⁸-10u⁷-2u⁶+14u⁵+12u⁴-6u³+2u²+2u-1=0의 (9/25, 37/100) 범위 내 유일한 근이다.
- 최적 배치에서 달성되는 한 변의 길이는 약 3.877083590으로 임의 방향 회전, 경계 접촉, 서로 겹치지 않는 내부를 허용한다.
- 증명의 핵심은 Lean 커널과 네이티브 컴파일러를 신뢰하며, 기하학과 검증기 건전성은 일반 Lean 증명으로 유지하고 수치 인증서는 native_decide로 처리한다.
- 7,920개 모듈 검증 결과와 수치 인증서의 정확한 해시값은 verification/native-certificates.json에 기록되었다.
- Lean 4.34.1과 Mathlib d13f23b723b8a 버전으로 고정되어 있으며 Linux/macOS에서 bash scripts/run_verification.sh로 재현할 수 있다.
- 검증 재현 시 반드시 OPTIMALITY_PROVED_WITH_NATIVE_CERTIFICATES, 0건의 오류, trust_model: lean_kernel_and_native_compiler 요구사항을 충족해야 한다.