AI 에이전트 7개로 조합론 하한 개선…Lean 검증 결과 공개

제임스 창(James Chang)이 AI 에이전트 일곱 개로 조합론 문제의 하한을 높인 증명을 공개했다. 연구자 원문과 Palomar 기록에 따르면 C(24,14,4)의 하한을 19에서 20으로 높인 결과가 기계 검증을 통과했다. 수학자 동료심사는 아직 받지 않았다.

덮개 설계는 작은 부분집합을 묶어 가능한 조합을 모두 포함하는 문제다. 이번 증명은 24개 원소 중 14개씩 고른 블록으로 모든 4개 원소의 조합을 덮으려면 적어도 20개 블록이 필요하다는 내용이다. 19개로는 불가능하다는 뜻이지, 20개만으로 충분하다는 뜻은 아니다.

창은 공개 저장소에서 10월 1일부터 3일까지 OpenAI Dots의 조정 에이전트 한 개와 연구 에이전트 여섯 개로 작업했다고 설명했다. 에이전트들은 수학적 논증, Lean 형식화, 계산 탐색, 반례 검토 등을 나눠 맡았다. 그는 문제를 고르고 연구 방향과 접근법을 조정했다.

AI가 작성한 논증을 다른 AI가 검토하는 것만으로 결과를 확정하지는 않았다. 공개 코드는 증명 보조 도구 Lean으로 정리를 표현하고, 명시한 가정에서 결론이 논리적으로 따라오는지 검사하도록 구성했다. Palomar의 10월 4일 등록 기록에는 검증한 저장소 커밋과 도구 버전, 별도 증명 검사기의 정보가 남아 있다.

같은 검증 기록은 C(25,15,5)의 하한을 32에서 34로 높인 정리도 포함한다. 이는 25개 원소 중 15개씩 고른 블록으로 모든 5개 원소의 조합을 덮을 때 적어도 34개 블록이 필요하다는 뜻이다. 두 문제 모두 정확한 최소 블록 수까지 결정한 것은 아니다.

창은 수학자의 검토를 요청했지만 아직 동료심사를 받지 않았다고 밝혔다. 기계 검증은 형식적으로 적은 정리에 대한 증명을 검사한다. 연구의 새로움이나 사람이 읽는 해설의 정확성까지 동료심사처럼 평가하는 절차는 아니다. 웹사이트의 해설과 형식 증명이 일치하는지도 별도로 살펴야 한다고 명시했다.

이번 공개 자료는 AI 에이전트가 낸 답과 검증 가능한 결과를 구분한 사례다. 수학적 탐색을 AI에 맡기되 정리의 진술, 증명 코드, 외부 기계 검증 기록을 함께 공개해 다른 사람이 결과를 확인할 수 있도록 했다.

출처: James Chang 연구자 원문 https://unexcitedneurons.substack.com/p/i-used-openai-dots-as-an-agent-swarm · 공개 증명 저장소 https://github.com/jamesyc/covering/tree/17bca0067a6bfa8c6c25669d97fca1190d20c8a3 · Palomar 등록·검증 기록 https://palomar-registry.org/entry.html?id=PALOMAR-2026-10-04-000003&version=1 · 연구자 검증 범위 설명 https://jamesyc.com/covering/trust/