9월 6일 artwaste.land 가 평면 위 점 15개로는 정확히 세 점을 지나는 직선을 32개 만들 수 없다는 결과를 올려, 1974년 버·그륀바움·슬론 논문이 '31 아니면 32'로 남겨 둔 값을 31로 확정했다고 밝혔어요. 직선 31개를 만드는 배치는 2018년에 이미 그림으로 나와 있어서 새로 붙은 건 '32개는 안 된다' 한 문장이고, 기하 문제를 SAT 논리식 네 덩어리로 바꿔 반박한 뒤 그 기록을 drat-trim 과 cake_lpr 두 검사기로 다시 검사했는데 cake_lpr 은 자기 정확성이 HOL4 에서 기계로 증명된 검사기예요. 다만 글쓴이가 직접 '기하 문제를 논리식으로 바꾸는 축소는 기계 검사를 안 받은 한 쪽짜리 증명이고 논리식 생성기도 감사만 받았지 정확하다고 증명되진 않았다'고 적어 뒀고, 저장소 README 는 이 사이트가 앤트로픽 클로드 인스턴스가 밤마다 하나씩 이어 쓰는 곳이며 'OEIS 는 AI 가 쓴 제출을 받지 않고 그게 옳다'고 밝혀 둬서, 바깥 수학자가 확인한 기록은 아직 없어요.
용어 풀이
- SAT
- 논리식을 참으로 만드는 값 배정이 있는지 판정하는 문제. 없다고 판정되면 그 논리식은 모순
- drat-trim
- SAT 풀이기가 남긴 '답 없음' 증명 기록을 원래 논리식에 다시 대 보며 검사하는 프로그램
- cake_lpr
- SAT 증명 기록 검사기. 자기 자신이 옳게 동작한다는 것이 HOL4 라는 증명 도구에서 기계로 증명돼 있음
- OEIS
- 온라인 정수 수열 백과사전. 정수 수열의 값과 근거를 모아 두는 공개 데이터베이스
운영자 인사이트
에이전트가 '기계로 검증했다'며 결과를 내놓으면 어느 단계가 검사됐는지부터 갈라 보세요. 여기서 기계가 검사한 건 논리식이 모순이라는 것뿐이고, 그 논리식이 원래 문제를 옳게 옮겼는지는 검사를 안 받은 한 쪽짜리 글에 걸려 있어요. 테스트가 다 통과했다는 말도 테스트가 요구사항을 옳게 옮겼을 때만 뜻이 있으니, 에이전트가 함께 써 준 테스트일수록 그 옮김을 직접 읽어 보세요.
여러 관점으로 보기
- 사이트 정체와 등재 경로 저장소 README 가 이 사이트를 '앤트로픽 클로드 인스턴스가 밤마다 하나씩 이어 쓰는 곳'이라고 밝히고, 'OEIS 는 AI 가 쓴 제출이나 자동 제출을 받지 않으며 그게 옳다'고 적어 뒀어요. 별은 0개이고 라이선스는 MIT 예요. GitHub
- 직선 31개 배치는 이미 있었어요 울프럼 블로그가 2018년 2월에 점 15개로 직선 31개를 만드는 배치를 그림으로 실었어요. 그러니 이번에 새로 붙은 건 배치가 아니라 '32개는 만들 수 없다' 쪽이에요. Wolfram Blog
- 왜 점 15개가 남아 있었나 알려진 값 표는 점 14개(직선 26개)까지만 적혀 있고 15개 칸이 없어요. 그린과 타오가 2013년에 공식을 증명했지만 '충분히 큰 n' 에만 해당해서 15 같은 작은 값은 그 정리로 덮이지 않아요. Wikipedia