AI가 도운 증명, 11개 정사각형 최적 배열의 수학적 검증을 통과하다
AI-assisted proof of optimal packing for 11 squares
11개 정사각형을 가장 작은 정사각형에 담는 최적 배열 문제의 최적성 증명이 Lean으로 형식화되어 검증을 통과했다. 7,920개의 Lean 모듈이 모두 승인되었고, 최종 감사에서 무결점으로 확인되었다. 최적 한 변의 길이는 8차 방정식의 근으로 주어지며 약 3.87708이다. 이 증명은 Lean 커널과 네이티브 컴파일러를 신뢰 모델로 사용한다.
완성된 EvolvingPrograms 검증 실행은 7,920개의 로컬 Lean 모듈을 모두 승인했고, 최종 감사는 제로 어드미션을 보고했다.
HN 토론
42- golden-face
정사각형 패킹이 실제로 무엇을 의미하는지 이해하는 데 꽤 시간이 걸렸다 (위키가 통찰력 있다) 하지만 요약하자면: 단위 정사각형(1x1)을 더 큰, 임의 크기의 정사각형에 패킹하는 것이다. 더 큰 정사각형의 변 길이가 정수가 아닐 때, 내부에 배치/패킹할 수 있는 1x1 정사각형의 최대 개수를 결정하는 것이 비자명해진다.
- DevelopingElk
나는 몇 가지 개인적인 변경을 가하여 이 증명을 재현하는 작업을 하고 있다. 기본 접근 방식은 표준적인 컴퓨터 지원 "피할 수 없는 집합" 접근법이다. 먼저, 두 정사각형의 중심이 같은 영역에 들어가지 않을 만큼 작은 영역을 선택한다. 이 글에서는 16을 사용했다. 각 영역은 정사각형을 포함하거나 포함하지 않아야 하며, 이는 16 choose 11 경우로 약 2000가지이다. 각 경우에 대해 이를 배제하려고 시도한다. 이는 정사각형으로 반드시 덮여야 하는 영역을 식별하고 이 정보를 전파함으로써 수행한다. 또한 1989년 Stromquist가 했던 것처럼 패킹 LP를 사용하여 더 많은 구성을 배제할 수 있다. 그런 다음 남은 경우에 집중하고 더 세분화한다.
AI 이전에 이것이 이루어지지 않은 유일한 이유는 진지한 초점의 주제가 아니었기 때문이라고 생각한다. 1989년의 컴퓨터는 모든 경우를 처리하기에 너무 약했다. 그러나 모든 기본 요소는 케플러 추측 증명에 존재했다. AI가 한 일은 노력을 충분히 낮춰서 정사각형 패킹을 좋아하는 아마추어들이 그러한 증명을 수행하고 형식적으로 검증할 수 있게 한 것이다. 나는 그러한 아마추어 중 하나라고 생각한다. 따라서 이것은 AI가 수학자의 증명을 훔치거나 초인적인 일을 하는 사례가 아니라 민주화의 사례이다. 나는 AI가 수학에 미치는 영향과 AI 기업의 행동 방식에 대해 우려하고 있지만, 이것은 걱정할 사례가 아니다. 이 배열이 최적임을 증명하기 위한 계산은 항상 손으로 확인하기에는 너무 클 것이다. 그러나 나는 패킹 LP 또는 핵심 중첩에 대한 멋진 시각화를 제작하기를 희망한다 […]
- dkural
처음 보이는 것만큼 임의적이거나 추하지는 않다 - 여기 이미지와 설명을 참조하라: https://x.com/davidmbudden/status/2107646435659481548
- yzydserd
참고로 정사각형 속 정사각형 패킹의 주요 사이트는 https://kingbird.myphotos.cc/packing/squares_in_squares.html 이다.
삼각형 뷰가 가장 흥미롭다. 그리고 이 뷰에 대한 20분 비디오는 다음에 있다:
- WithinReason
이미지와 함께 많은 정사각형 패킹 목록: