Claude Code, 오차드 문제 해결

Claude Code가 1974년 이후 미해결 상태였던 '오차드 문제(Orchard Problem)'의 15개 점에 대한 최대 직선 수를 31로 확정했다. 이는 52년간 논쟁이 되어온 기하학적 난제를 AI 에이전트 협업으로 해결한 사례다.

증명 과정 및 검증

• 문제 정의: 평면상의 n개 점을 배치할 때, 정확히 3개의 점이 지나는 직선의 최대 개수를 구하는 문제이다. 15개 점일 때 기존에는 31개 또는 32개가 가능할 것으로 추정되었으나, 이번 연구를 통해 32는 불가능하고 최대값은 31임이 증명되었다.
• AI 활용 방식: Claude Code는 연구를 총괄하며 여러 에이전트에 작업을 분배했다. 기하학적 조건을 4개의 유한한 SAT(충족 가능성) 사례로 축소하고, 이를 독립적으로 반증했다.
• 검증 신뢰성: SAT 솔버가 생성한 증명은 drat-trim으로 확인된 후 LRAT 형식으로 변환되어, HOL4에서 형식 검증된 cake_lpr 체크어에 의해 최종 승인되었다. 이를 통해 SAT 솔버 자체의 오류 가능성을 배제했다.

의의

이 결과는 단순한 직선 배치 문제를 넘어, 유사선(pseudoline) 배치에서도 32개가 불가능함을 보여준다. 저자는 Claude Code를 활용해 수학 문제를 체계적으로 풀고 검증하는 공개 프로젝트의 일부라고 밝혔다.