AI는 왜 반례부터 찾았나
무엇이 백 년 된 추측을 무너뜨렸을까. 2026년 7월 19일 수학자 Levent Alpöge는 X에 Claude Fable 5가 찾은 3변수 다항사상을 공개했다. 야코비 행렬식(함수의 국소적 변화율을 나타내는 행렬식)은 언제나 -2이지만, 서로 다른 세 입력을 같은 값으로 보내므로 역함수가 없는 사상이다. 1884년에 원형이 제시되고 1939년 Keller가 정식화한 야코비안 추측은 이 반례로 차원 3 이상에서 거짓임이 확인됐다. 반례가 조건을 만족하는지 확인하는 데는 몇 분이면 충분했다.
즉 증명은 모든 경우를 다뤄야 하지만 반증에는 조건을 깨는 대상 하나면 충분하다. 그 대상을 유한한 식이나 구조로 쓰고 간단한 계산으로 검사한다면, 기계는 많은 후보를 빠르게 걸러낼 수 있다. AI가 먼저 성과를 낸 곳은 이처럼 탐색은 넓지만 후보 하나의 판정은 싼 문제였다.
1946년 Erdős가 제시한 단위거리 추측도 그런 사례다. OpenAI 모델은 기존 정수론 연구를 조합해, 점이 개일 때 단위거리인 점의 쌍이 1보다 큰 지수로 늘어나는 배치를 만들었다. 이후 프린스턴대 수학자 Will Sawin이 이 구성을 분석해 규모로 늘어난다는 지수를 도출했다. 오래된 예상은 폐기됐고, 최적 성장률은 아직 밝혀지지 않았다. 알려진 하계와 상계 사이에는 여전히 와 의 간격이 남아 있을 뿐이다.
이처럼 수학자는 성공 가능성이 낮은 경로에 오랜 연구 경력을 걸기 어렵지만, 모델은 계산 예산 안에서 실패를 싸게 반복하며 수많은 경로를 시험한다. 야코비안 반례를 두고 수학자 Tim Gowers는 결과가 증명이 아니라 반례임을 확인한 뒤 파급 범위를 낮춰 봤지만, 사람이 Annals에 제출했다면 게재를 추천했을 수준이라는 평가는 유지했다.
병목은 작성에서 검토로 옮겨갔다
단위거리 반증 뒤에는 형식 검증이 빠르게 이어졌다. Logical Intelligence의 Aleph Prover는 논문을 엿새 만에 Lean(수학 증명을 기계가 검증하는 언어) 코드로 옮겼고 OpenAI의 Sol은 3주 동안 120만 줄을 생성했다. 이는 9년에 걸쳐 구축된 mathlib 230만 줄의 절반과 비슷한 양 이다. 자동 생성 코드와 오랜 검토를 거친 라이브러리의 가치는 같지 않다. 다만 사람이 한 줄씩 작성하던 때와 다른 규모의 초안이 한꺼번에 생기기 시작했다.
역할도 나뉘었다.
- Sol이 유한 군스킴의 반례를 만들자 Fable이 Lean 1,076줄로 옮겼고 사람이 mathlib에 제출할 변경안으로 정리했다.
- 야코비안 반례 역시 박사과정 연구자 Paul Lezeau가 DeepMind 저장소의 형식 진술과 연결했다.
모델이 발견과 코드 초안을 맡았고 사람이 기존 수학 체계에 통합했다.
그런데 코드 생산이 빨라지자 검토가 뒤따르지 못했다. Mathlib Initiative에는 약 300건의 변경안이 쌓였고 첫 검토까지 걸리는 시간의 중앙값은 2주였다. 이 단체는 상근 편집팀을 꾸려 2026년 9월까지 회신의 90%를 일주일 안에 처리한다는 목표 를 세웠다. 사람이 설명하거나 유지할 책임을 지지 않는 저품질 자동 생성 코드는 닫을 수 있다는 기여 원칙 도 마련했다. 이제 부족한 것은 코드가 아니라 검토할 사람이었다.
Lean은 증명해도 뜻은 증명하지 않는다
Lean이 통과시킨 증명은 무엇을 보증할까. Lean 커널은 주어진 형식 진술에서 결론이 논리적으로 따라오는지 확인한다. 그러나 그 진술이 원래 추측의 뜻을 정확히 옮겼는지는 보증하지 않는다. 원문을 잘못 번역했다면 틀린 진술을 완벽하게 증명한 코드도 통과한다. 잘못된 문제를 완벽하게 푸는 것과 같다. 그래서 사람이 먼저 확인할 대상은 진술의 정확성이다.
논리적으로 맞는 파일이 곧 좋은 수학 라이브러리인 것도 아니다. 실제로 Vasily Ilin과 Brian Nugent가 Grothendieck 소멸정리를 형식화했을 때 코드는 빈칸 없이 컴파일됐지만 전문가들은 정의의 선택과 정리의 일반성, 파일 구성과 재사용성을 문제로 지적했다. 에이전트는 컴파일 오류처럼 기계가 판정할 수 있는 국소 문제에는 잘 대응했지만, 정의와 인터페이스 설계에는 약했다. 검증되는 증명 파일과 오래 쓰이는 라이브러리는 요구되는 기준이 서로 다르다.
이 점에서 형식 검증은 사람이 살필 대상을 수백 쪽 논증에서 핵심 진술과 정의로 줄여 준다. 다만 신규성까지 확인하지는 않는다. 문헌 조사를 생략해 이미 풀린 Erdős 333번을 새 성과로 발표한 사례도 있었다. Lean을 사용해도 진술의 번역과 선행 연구는 사람이 확인해야 한다.
야코비안 반례 역시 같은 구조였다. 프리프린트와 동료심사 없이 먼저 알려졌고 Lean 파일이 빠른 확인 근거가 됐다. 연구자 Jun-Yong Park은 결정적 주장을 기계가 검증할 수 있는 형식으로 공개해 누구나 감사할 수 있게 하자고 제안했다. 형식 공개가 동료심사를 대신하는 것은 아니다. 정확한 진술과 라이브러리의 품질을 판단할 수학자가 있어야 검증 체계도 작동한다.
반례 이후에 남는 일
반례를 유한하게 표현할 수 있고 찾는 비용보다 확인하는 비용이 훨씬 낮은 문제에서 AI가 먼저 성과를 냈다. 기존 라이브러리의 정의와 정리까지 재사용할 수 있으면 발견에서 형식 검증으로 곧바로 넘어간다. 조합론, 이산기하, 대수적 구성에서 성과가 먼저 나왔다.
그러나 리만 가설이나 나비에–스토크스 문제는 후보 하나를 짧은 계산으로 판정하는 구조가 아니다. 검산 자체에 새로운 논증이 필요할 수 있다. 자동 탐색의 범위도 아직 좁다. 형식 진술이 마련된 미해결 문제 353개를 대상으로 한 평가에서 자율적으로 해결된 문제는 9개였다. 아직 소수에 그친 셈이다.
사람에게 남는 일은 최종 확인만이 아니다. 연구할 질문을 고르고 뜻을 훼손하지 않는 형식 진술을 만들고 발견된 대상을 설명하는 이론을 세우는 일도 사람의 몫이다. 반례는 명제가 거짓임을 알려 줄 뿐 어떤 명제가 대신 참인지는 말하지 않는다.
단위거리 반례도 마찬가지다. Erdős의 예상은 폐기했지만 상계와 하계의 간격을 닫지 못했다. 아홉 명의 수학자가 19쪽짜리 동반 논문에서 구성을 다시 설명한 이유 는 다음 연구에 쓸 언어와 관점이 필요했기 때문이다. 기계가 더 많은 반례를 찾더라도, 정확한 진술과 읽을 수 있는 설명이 없으면 다음 연구로 이어질 언어는 사라진다.