기계가 푸는 수학, 그 기록을 남기는 공개 작업장 'TheoremDB'

수학 증명을 사람이 아니라 기계가 시도하고 검증하는 흐름이 빠르게 현실이 되고 있다. 형식 증명 도구와 대규모 언어모델, 자동 탐색 기법이 결합되면서 '풀 수 있는가'만큼이나 '누가, 어떤 근거로 풀었는가'를 어떻게 기록하고 검증할 것인지가 중요한 문제로 떠올랐다. TheoremDB는 스스로를 '기계 수학(machine mathematics)을 위한 공개 작업장'으로 소개하며, 미해결 문제, 증명과 시도의 영구 기록, 근거와 기여자 표시를 한곳에 모으겠다고 밝힌다. 결과물뿐 아니라 실패한 시도와 부분적 진전까지 남긴다는 발상이 핵심이다.

어떤 문제들이 올라와 있나

사이트에 등록된 문제 목록을 보면 성격이 뚜렷이 갈리는 두 부류가 눈에 띈다. 하나는 경계가 유한하고 구체적으로 지정된 계산형 문제다. 예를 들어 세 세제곱수의 합이 114가 되는 정수해가 절댓값 10의 20제곱 이하에 존재하는지, 668×668 크기의 아다마르 행렬이 존재하는지, 단위 정사각형 안의 열 개 점이 만드는 가장 작은 삼각형 넓이를 최대화하면 얼마인지, 4차원에서 지름이 1인 집합을 지름이 더 작은 다섯 조각으로 나눌 수 있는지(보르수크 문제)와 같은 것들이다. 이런 문제는 탐색 범위가 명시돼 있어 계산이나 자동 탐색으로 직접 두드려 볼 여지가 있다.

다른 한 부류는 이론 전산학과 수학의 이름난 대난제다. 행렬 곱셈 지수 ω가 2인지, 산술 회로 복잡도에서 VP와 VNP가 같은지, 로그 공간에서 결정적 계산과 비결정적 계산이 같은지(L=NL), 강한 지수시간 가설이 성립하는지, 모든 쌍 최단경로를 세제곱보다 빠르게 풀 수 있는지, 램지 수의 k제곱근 극한이 존재하는지 같은 문제가 나란히 놓여 있다. 실수 지수체의 1차 이론이 결정 가능한지, 원의 둘레 상수와 관련된 근사 문제처럼 순수 수학의 오래된 질문도 섞여 있다.

정밀한 서술이 만드는 차이

이 구성에서 읽어야 할 신호는 '정밀한 서술'이다. 등록된 문제들은 대체로 정의역, 범위, 판정 조건이 모호함 없이 적혀 있다. 이는 사람이 읽기 위한 배려이기도 하지만, 동시에 기계가 문제를 오해 없이 받아들이고 답을 내놓았을 때 그 답을 명확하게 채점할 수 있게 만드는 조건이기도 하다. 참·거짓이나 정확한 수치를 요구하는 형태로 문제를 다듬어 두면, 자동 증명기나 탐색 기반 시스템이 겨냥할 수 있는 표적이자 성능을 비교하는 벤치마크가 된다. 계산형 문제가 다수 포함된 것도 같은 맥락으로 보인다.

실무자에게 주는 함의

국내 AI·형식검증 분야 실무자에게 이 시도가 갖는 의미는 두 갈래다. 첫째는 벤치마크다. 수학 문제 풀이를 표방하는 모델과 도구가 늘어나는 가운데, 정답 여부를 다투기 어려운 개방형 난제를 공통 형식으로 모아두면 서로 다른 접근을 같은 잣대로 견줄 수 있다. 둘째는 출처와 기여의 추적이다. 기계가 생성한 증명이 쏟아질수록 '누가 무엇을 언제 기여했고, 그 결과가 검증됐는가'를 남기는 인프라의 가치가 커진다. 시도의 영구 기록과 근거 보존이라는 표어는 재현성 논의와 직접 맞닿아 있으며, 실패와 부분 성과까지 남긴다면 같은 벽에 반복해서 부딪히는 낭비를 줄이는 효과도 기대할 수 있다.

확인되지 않는 것들

다만 공개된 소개 문구와 문제 목록만으로는 이 작업장의 실체를 판단하기 어렵다. 운영 주체가 누구인지, 제출된 증명을 어떤 방식으로 검증하는지, 형식화된 자동 검증 파이프라인이 붙어 있는지, 참여 규모가 어느 정도인지는 주어진 자료로 확인되지 않는다. 문제들이 어느 정도까지 기계 판독 가능한 표준 형식으로 인코딩되는지도 분명치 않다. 또한 등록된 상당수 문제는 인간 수학자에게도 여전히 최상급 난제여서, 공개 작업장이 마련됐다는 사실이 곧 해결 속도를 보장하지는 않는다.

그럼에도 문제를 정밀하게 서술하고, 결과와 시도를 공개적으로 축적하며, 기여를 명시하려는 방향 자체는 눈여겨볼 만하다. 자동화된 수학이 연구 도구를 넘어 협업 대상이 되어가는 단계에서, 성과를 기록하고 신뢰할 방법을 먼저 고민한다는 점에서다. 국내에서 형식 증명이나 자동 추론에 관심 있는 팀이라면, 이런 공개 저장소가 어떤 검증 체계를 갖추고 어떻게 커뮤니티를 모으는지를 지켜보며 자신들의 실험을 견줄 좌표로 삼아볼 만하다.