최근 몇 달 사이 오래된 난제부터 새로운 결과까지 인공지능이 만들어낸 수학 증명이 눈에 띄게 늘었고, 그중 일부는 증명 보조 언어인 Lean으로 형식화되기도 했다. 문제는 특정 Lean 저장소가 정말로 주장하는 명제를 증명하는지 확인하는 일이 결코 간단하지 않다는 점이다. Lean에 익숙하지 않은 독자라면 더욱 그렇다. 우선 형식화된 Lean 명제에 딸린 증명이 실제로 타입체크를 통과하는지 봐야 하고, 그 증명이 별도의 공리를 추가하는 식의 '꼼수'를 담고 있지 않은지 검사해야 하며, 형식적 명제가 비형식적으로 서술된 결과와 의미상 일치하는지까지 따져야 한다.
수학자 테런스 타오는 자신의 블로그를 통해 이런 혼란을 정리하기 위한 시도로 'Palomar(팔로마)'라는 Lean 검증 수학 등록소가 제출을 받기 시작했다고 밝혔다. 팔로마는 Lean FRO와 ICARM이 인큐베이팅한 이니셔티브로, 천문대 이름에서 따왔다. 타오는 과학자문위원회 등 여러 역할을 맡고 있으며, 위원회에는 제러미 아비가드, 매튜 발라드, 브리나 크라, 킴 모리슨, 라비 바킬, 악샤이 벤카테시 등이 함께 이름을 올렸다.
프리프린트 서버에 가까운 구조
팔로마를 가장 단순하게 설명하면 Lean 증명을 위한 프리프린트 서버에 해당한다. 다만 논문 원고 자체를 올리는 것이 아니라, 외부 GitHub 저장소, 더 정확히는 특정 커밋으로 고정된 저장소의 '스냅샷'을 등록하는 방식이다. 등록 대상 저장소는 현재 통용되는 형식화 모범 사례를 따라야 하며, 여기에는 몇 가지 추가적인 기술 요건도 붙는다. 즉 팔로마는 코드 자체를 호스팅하는 저장소가 아니라, 검증을 통과한 저장소의 특정 시점을 가리키는 목록에 가깝다.
제출된 스냅샷은 두 갈래의 검사를 거친다. 첫째는 풀이 모듈이 타입체크를 통과하고 챌린지 파일에 명시된 결과를 정확히 증명하는지를 보는 검사다. 이 과정은 Lean 도구인 Comparator를 이용한 순수 기계적 절차다. 둘째는 formalization.yaml 파일에 담긴 비형식적 서술이 챌린지 파일이 주장하는 결과와 실제로 맞아떨어지는지 확인하는 검사인데, 이 부분은 대규모 언어모델이 수행하는 비결정적 판정이다. 저장소가 두 검사를 모두 통과하고 등록소의 최소 기준을 충족하면 팔로마에 등재될 수 있다.
동료심사가 아니라는 점
여기서 반드시 짚어야 할 것은 이 두 검사가 사람이 수행하는 정식 동료심사와는 거리가 멀다는 사실이다. 타오 스스로도 이 절차가 결과의 참신성, 흥미로움, 정확성을 사람이 평가하는 수준에는 한참 못 미친다고 분명히 밝혔다. 팔로마는 명제와 증명이 형식적으로 맞물려 있는지, 그리고 그 형식이 말로 풀어 쓴 주장과 일치하는지를 보증할 뿐이며, 그 결과가 학문적으로 의미 있는지까지 판단하지는 않는다. 다시 말해 팔로마는 동료심사 학술지가 아니다.
실무적으로 보면 이 구분은 중요하다. 형식화된 증명이 팔로마에 등재됐다는 사실은 '이 코드가 주장하는 명제를 꼼수 없이 증명한다'는 기계적 신뢰를 제공하지만, '이 결과가 새롭고 중요하다'는 학술적 승인과는 별개다. AI가 생성한 증명이 늘어나는 상황에서, 검증 가능성이라는 기술적 신뢰와 가치 판단이라는 학문적 신뢰를 분리해 다루려는 설계로 읽힌다. 실제로 타오는 최근 센도프 추측 증명의 형식화를 시험 삼아 직접 제출해 성공했으며, 과거 형식화 결과물도 곧 등록할 계획이라고 덧붙였다.
제출 절차는 꼼꼼하지만 감당할 수 없는 수준은 아니라는 게 타오의 평가다. 사람이 만든 것이든, AI가 생성한 것이든, 둘을 섞은 것이든 오래된 결과와 새로운 결과 모두 제출을 환영한다. 흥미로운 대목은 최신 AI 에이전트가 제출의 기계적 세부 작업을 상당 부분 도와줄 수 있다는 점인데, 타오는 그럼에도 사람의 검토가 여전히 강력히 권장된다고 못 박았다. 검증 자동화의 일부를 AI에 맡기더라도 최종 책임은 사람에게 있다는 태도인 셈이다.
한국의 개발자나 연구 실무자 관점에서 팔로마는 두 가지 시사점을 준다. 하나는 형식 검증 인프라가 개별 연구자의 저장소 수준을 넘어 공용 레지스트리 형태로 제도화되기 시작했다는 신호이고, 다른 하나는 AI가 만든 증명을 '믿을 수 있는가'라는 물음을 사람의 권위가 아니라 재현 가능한 기계 검사와 명제-서술 정합성 확인으로 옮겨가려는 흐름이다. 논의와 피드백은 Zulip 채널에서 이뤄지며, 제출을 고려한다면 사전에 공개된 상세 지침을 먼저 읽어보는 편이 좋다.