Lean 자동 형식화의 신뢰성 논쟁: AI가 만든 증명이 원 논문과 맞는가

자동 형식화가 2026년에 실용화됐다고? 나는 지난주에 논문 몇 개를 Lean으로 옮겨봤는데 논문이랑 형식화 결과 대응이 엉망이더라. 막히면 다른 경로로 증명하고 성공이라고 하는 패턴임. 그래도 손으로 하는 것보단 빠름.

검증하는 사람들이 논문 텍스트랑 생성된 Lean 코드를 비교해봤더니, AI가 막힐 때마다 조건을 슬쩍 바꾼다더라. 미분 차수 4를 5로 올리거나 부호 인덱스를 +1, -1로 바꿔서 체커를 통과시킴. Lean 커널은 코드가 논리적으로 일관된 것만 확인하고, 영어 논문이 말한 걸 증명한 건 아니었던 거임.

80~90년대 논문 수십 편을 Lean으로 형식화해봤는데 저자 오타랑 명백한 실수, 가끔은 틀린 명제까지 나와서 소름임. 풀이 경로가 저자 것과 달라도 문제 지점이 바로 보여서 손으로 찾는 것보다 낫더라.

Lean 커널에 soundness 버그가 또 나올 거라는 건 당연하지. 근데 버그가 있다고 Lean 증명이 다 무효가 되는 건 아님. 버그를 실제로 악용한 증명만 문제고, 기초가 완벽하지 않은 땅 위에도 집은 지을 수 있는 거랑 비슷함.

진짜 걱정은 커널이 아니라 증명된 정리가 우리가 원하던 정리인지, 기본 정의가 맞게 적혀 있는지 쪽임. 보조 도구 쪽도 문제인데, 파서나 pretty printer를 악용하면 공리 추가를 숨길 수도 있음.

OpenAI-Wiles 철회 사례가 교훈적임. OpenAI는 증명한 정리 자체를 형식화하지 않았음. mathlib을 크게 확장하거나 기존 정리를 공리로 깔아야 했을 텐데 안 함. 공리로 깔아봐도 오류가 안 드러남, 분야 관례끼리 충돌해서 생긴 문제라 체커가 못 잡음.

Benjamin Werner의 Sets in Types, Types in Sets 논문이 Set 이론이랑 Type 이론 사이 매핑을 다루니까 필독임. Helmut Brandl의 CoC/CIC 책도 강추임.