요약
정사각형 11개를 담는 가장 작은 정사각형의 한 변이 약 3.877임을 Lean으로 증명했습니다.
한 변이 1인 정사각형 11개를 큰 정사각형 안에 가장 빽빽하게 넣는 문제를 다룬 GitHub 저장소입니다. 발터 트룸프가 찾은 배치가 최적이라는 컴퓨터 보조 증명을 증명 보조기(수학 증명을 기계가 검사하는 프로그램) Lean 4로 옮겨 검증했습니다.
왜 중요한가
- 트룸프의 배치보다 더 작게 넣는 방법이 없다는 것을 기계가 끝까지 검사해 확정했습니다.
- 다만 이 검증은 Lean 커널뿐 아니라 네이티브 컴파일러까지 믿어야 성립한다고 저장소가 직접 밝혔습니다.
핵심 내용
- 최적인 한 변의 길이는 8차 다항식의 한 근으로 정확히 표현되며, 값은 약 3.8771입니다.
- 정사각형을 아무 방향으로나 돌릴 수 있고 테두리끼리 닿아도 되는 조건에서 증명했습니다.
- 전체 검증에서 Lean 모듈 7,920개가 모두 통과했고, 증명을 비워 둔 곳(sorry)은 없었습니다.
- 계산이 무거운 일부 수치 검산에는 코드를 컴파일해 실행하는 native_decide 기능을 썼습니다.
- 제목과 달리 README에는 어떤 AI를 어떻게 썼는지에 대한 설명이 없습니다.
HN 반응
- 증명을 재현 중인 한 이용자는 표준적인 경우 나누기 방식이며, AI는 아마추어도 해낼 만큼 수고를 줄였다고 설명했습니다.
- README에 배치 그림이 없고 글도 LLM이 쓴 것 같다는 불만이 나와, 이용자들이 그림을 볼 수 있는 사이트를 공유했습니다.
참고로 정사각형 안에 정사각형 채우기를 다루는 대표 사이트는 https://kingbird.myphotos.cc/packing/squares_in_squares.html 입니다.
가장 흥미로운 건 삼각형 보기 방식입니다. 이 보기 방식을 20분 동안 설명하는 영상은 https://youtu.be/uL5wuiy34rs 에 있습니다.
"신은 죽었다. 그리고 정사각형의 최적 패킹이 그를 죽였다." 이 괴물 같은 배치들을 볼 때마다 이 밈이 떠올라요. 이해는 하겠는데, 마음에 들지는 않네요. ;)
제 택배가 다 찌그러져서 도착하면 이유는 이거겠네요. 22개가 아니라 다른 택배 23개와 같이 실렸는데, 기사님이 정사각형 최적 패킹 해법을 꿰고 있는 거죠.
83과 87은 왜 더 작아질 수 없는지 설명해 주실 분 계신가요?
바깥 테두리가 정사각형이어야 하니까요. 83과 87은 한쪽 방향으로는 바깥 테두리를 줄일 수 있지만, 두 방향을 동시에 줄일 수는 없습니다.
줄일 수 있을 가능성도 있습니다. 목록에 있는 83과 87의 배치가 최적이라는 건 아직 증명되지 않았습니다.
어느 블록을 움직이면 해를 더 작게 만들 수 있다고 생각하세요? 아니면 아예 다른 배치를 떠올리고 계신 건가요?
저는 어떤 이유에선지 안쪽 블록 상당수가 렌더링되지 않았거든요 ㅎㅎ
처음 보기만큼 제멋대로이거나 못생긴 배치는 아닙니다. 그림과 설명은 여기서 볼 수 있습니다: https://x.com/davidmbudden/status/2107646435659481548
흥미로워 보이는데, 혹시 nitter 버전 같은 건 없나요? 아니면 누가 그 이미지를 받아서 트위터가 아닌 곳에 올려 주실 수 있을까요?
X 링크는 안 누르겠지만, 말씀은 고맙습니다.
X 말고 다른 곳에 올라온 설명은 없나요?
언급된 논문은 이것입니다: https://pingyou.com/papers/eleven-squares.pdf
저는 이게 깊은 의미가 있는지는 잘 모르겠습니다.
수학에서 해답은 언제나 의미가 있습니다.
저는 이 증명을 일부 변경을 주면서 재현하는 작업을 하고 있습니다. 기본 접근법은 컴퓨터를 활용하는 표준적인 '불가피 집합(unavoidable set)' 방식입니다. 먼저 정사각형 두 개의 중심이 한 영역에 함께 들어갈 수 없을 만큼 작은 영역들을 정합니다. 기사에서는 16개를 썼습니다. 각 영역에는 정사각형이 있거나 없거나 둘 중 하나이므로, 경우의 수는 16개 중 11개를 고르는 조합, 약 2000가지입니다. 각 경우를 하나씩 배제해 나가는 겁니다. 반드시 정사각형으로 덮여야 하는 구역을 찾아내고, 그 정보를 전파하는 식으로요. 1989년에 스트롬퀴스트(Stromquist)가 했던 것처럼 패킹 LP를 써서 더 많은 배치를 배제할 수도 있습니다. 그다음 남은 경우만 골라 더 잘게 나눕니다.
제 생각에 AI 이전에 이 증명이 나오지 않은 유일한 이유는 이 주제가 진지하게 다뤄지지 않았기 때문입니다. 1989년의 컴퓨터로는 경우의 수를 감당할 수 없었습니다. 하지만 기본 재료는 케플러 추측 증명에 이미 다 있었습니다. AI가 한 일은 정사각형 패킹이 그저 좋아서 달려든 아마추어도 이런 증명을 해내고 형식 검증까지 할 수 있을 만큼 수고를 덜어 준 것입니다. 저도 그런 아마추어 중 하나라고 생각합니다. 그러니 이건 AI가 수학자의 증명을 가로챈 사례도, 초인적인 일을 해낸 사례도 아닙니다. 민주화에 가깝습니다. AI가 수학에 미치는 영향도, AI 기업들의 행태도 걱정스럽긴 하지만, 이 사례는 걱정할 대상이 아닙니다. 이 배치가 최적임을 증명하는 계산은 앞으로도 손으로 검산하기에는 너무 큽니다. 다만 저는 각 배치를 기각하는 패킹 LP나 코어 겹침을 보여 주는 멋진 시각화를 만들어 보고 싶습니다.
이건 정말 시각화가 있었으면 좋겠습니다.
"정사각형 두 개가 들어가지 않는 영역을 고른다 -> 16(??)"
저는 고급 수학을 (능숙하진 않아도) 읽을 줄은 안다고 생각하는데, 이 대목은 헷갈리고 제 쪽에서 가정을 많이 깔아야 이해가 됩니다.
더 쉽게 보자면, 먼저 큰 정사각형에서 가장자리로부터 0.5 단위 떨어진 중앙 영역에 주목하세요. 정사각형의 중심은 모두 이 영역 안에 있어야 합니다. 이 영역을 크기가 같은 정사각형 타일 25개의 격자로 나눕니다. 이제 각 타일은 정사각형 두 개의 중심이 같은 타일 안에 들어갈 수 없을 만큼 작습니다. 그러면 가능한 경우는 25개 중 11개를 고르는 조합이 됩니다. 기사에서는 이 영역을 대신 육각형으로 나눴는데, 이 육각형도 정사각형 두 개의 중심이 같은 육각형 안에 들어갈 수 없을 만큼 작았습니다. 덕분에 타일을 16개만 쓸 수 있었고, 가능한 경우의 수가 크게 줄었습니다.
여러 정사각형 패킹을 이미지와 함께 모아 놓은 목록입니다.
https://jlevy.github.io/squares/
저는 기하학을 좋아하는데, 이 패킹들을 보면 51처럼 못생긴 숫자가 있네요.
ㅎㅎ 105는 엉망이에요.
예쁘네요! OEIS를 확인해 봤는데, "흥미로운" 타일링은 k < floor(sqrt(k)) * ceiling(sqrt(k))를 만족하는 수 k에서 나타나는 것 같습니다(A189151).
이런 타일링을 찾는 사람들한테는 당연한 얘기일 수도 있지만, 저는 꽤 깔끔하다고 생각했습니다.
README에 패킹을 설명하는 그림이 없네요 :(
여기에 멋진 그림이 있어요: https://x.com/ojoshe/status/2107590622005924265
네오 트위터에 클릭을 바치지 않아도 되는 미러는 없을까요?
https://kingbird.myphotos.cc/packing/squares_in_squares.html
다른 패킹(원 안에 원 등)이 더 보고 싶으시면 이 페이지를 확인해 보세요: https://erich-friedman.github.io/packing/index.html
저도 같은 생각을 했어요! 그림 좀 보여 주세요.
수정: 몇 개 아래 링크에서 찾았습니다. https://jlevy.github.io/squares/cases/11.html
< https://en.wikipedia.org/wiki/File:Packing_11_unit_squares_in_a_square_with_side_length_3.87708359....svg > 이 파일은 https://en.wikipedia.org/wiki/Square_packing 에 있습니다.
README도 전부 LLM이 쓴 것 같아요.
저는 정말 이해가 안 가요. 뭔가 멋진 일을 해냈다고 생각한다면 왜 자기 말로 이야기하고 싶지 않을까요?
더 많은 그림은 여기 있습니다: https://jlevy.github.io/squares/
엉망으로 흐트러진 배치가 가지런히 정렬한 배치보다 더 최적일 수 있다는 건 직관에 반합니다. 지금까지 나온 최선의 해들을 보면 대체로 깔끔한 배치가 최선이긴 한데, 항상 그런 건 아니고요. 이 어수선한 경우들은 어떻게 설명해야 할까요?? 나눗셈 때문에 무리수가 나올 수 있는 것과 관련이 있나요? 그래서 최적으로 넣을 수 있는 정사각형 수가 어느 선에 가까워지면 이렇게 어수선한 배치가 나오는 건가요?