OpenAI 수학 저장소가 Lean 형식화를 늘리며 정리 3건을 철회했다

OpenAI가 공개한 수학 저장소(openai/math)가 최신 갱신을 통해 Lean 형식화 6건을 새로 추가하고 19건을 수정했으며, 기존에 실려 있던 결과 3건을 철회했다. 저장소가 다루는 핵심 결과 가운데 약 42%가 형식화된 상태다.

철회된 원고는 'Algebraicity of Weil classes on split abelian eightfolds', 'Algebraicity of Kuga–Satake Correspondences for K3 Surfaces', 'The rational Hodge conjecture for products of K3 surfaces' 세 편이다. 아벨 다양체와 K3 곡면을 둘러싼 대수성·호지 추측 계열이라는 공통점이 있다.

Lean은 수학 정리와 증명을 기계가 검사할 수 있는 형식 언어로 적는 도구다. 자연어로 쓰인 논문은 사람이 읽고 검증해야 하지만, Lean으로 옮긴 증명은 컴파일러가 통과 여부를 판정한다. OpenAI가 수학 결과를 저장소 형태로 관리하며 형식화 진행률까지 공개하는 배경도 여기에 있다.

이번 갱신 소식은 Dan Roberts가 X를 통해 알렸다. 그는 새 형식화를 계속 추가하고, 발견되는 오류(errata)도 저장소에 반영해 나가겠다고 밝혔다.

개발자 입장에서 눈에 띄는 대목은 정리도 소프트웨어처럼 버전 관리된다는 점이다. 새 결과가 들어오고, 기존 결과가 수정되고, 문제가 생기면 철회 기록이 남는다. 철회가 공개 로그로 남는 일은 수학계에서 흔치 않아, 해커뉴스에서는 이런 관행을 더 많은 연구소가 따라야 한다는 반응이 나왔다.

42%라는 숫자는 양쪽으로 읽힌다. 형식화된 결과는 기계 검증을 거쳤다는 뜻이지만, 나머지 58%는 아직 그렇지 않다. 저장소의 결과를 인용하거나 참고할 때 형식화 여부를 함께 확인해야 하는 이유다.

철회된 세 원고가 어떤 이유로 빠졌는지는 이번 공지에 담기지 않았다. 저장소 측은 앞으로도 새 형식화와 오류 수정을 계속 반영하겠다는 계획만 밝혔다.