Lean이 AI 증명을 믿는 방식, 1300만 줄도 작은 커널이 검사한다

Lean이 AI 증명을 믿는 방식은 생성 모델의 설명이나 추론 능력을 평가하는 것이 아니다. AI가 작성한 소스를 정교화기가 명시적인 증명 항으로 바꾸고, 작은 신뢰 커널이 그 항의 형이 목표 명제와 일치하는지 검사한다. 1300만 줄 규모의 코드도 이 검사를 통과할 수 있지만, 커널이 원시 소스의 모든 줄을 직접 읽는다는 뜻은 아니다.

커널 통과가 보장하는 범위도 조건부다. 주어진 정의와 공리, Lean의 유형 이론을 전제로 결론이 올바르게 도출됐음을 보장할 뿐이다. 형식화된 명제가 작성자의 의도와 같은지, 받아들일 수 없는 공리가 숨어 있는지, 현실에 관한 입력이 사실인지는 별도로 판단해야 한다.

소스가 증명 항으로 바뀌는 과정

사람이나 AI가 작성하는 Lean 소스는 커널이 바로 검사할 수 있는 완전한 표현이 아니다. 표기법, 생략된 인수, 오버로딩, 전술 호출처럼 작성을 편하게 하는 요소가 들어 있기 때문이다. Lean의 정교화·컴파일 문서 는 정교화가 사용자용 구문을 핵심 유형 이론으로 변환하고, 신뢰 커널이 그 결과를 유형 이론의 규칙에 따라 검사한다고 설명한다.

1. 소스와 전술: 작성자가 읽고 수정하기 쉬운 명령과 표기다.
2. 정교화기: 문맥을 이용해 암묵적 인수와 빈칸을 채우고 전술을 실행한다.
3. 증명 항: 핵심 언어로 표현된 명시적인 증명 객체다.
4. 커널: 각 정의와 증명 항이 선언된 형을 실제로 갖는지 판정한다.

정교화기와 전술은 커널보다 훨씬 복잡하다. 버그가 잘못된 후보 항을 만들 수는 있지만, 그 항이 핵심 규칙에 맞지 않으면 커널 검사를 넘지 못한다. 따라서 증명의 논리적 건전성을 위해 모든 전술과 자동화 기능을 커널과 같은 수준으로 신뢰할 필요는 없다.

여기서 커널 검사와 실행 파일을 만드는 컴파일은 구분해야 한다. Lean의 처리 과정에는 둘 다 포함되지만, 정리의 증명 여부를 판정하는 핵심 단계는 정교화된 항에 대한 커널 검사다. “컴파일됐으니 참이다”라는 표현은 어떤 명제를 어떤 전제 아래 검사했는지 생략하므로 정확하지 않다.

P → P가 통과하는 이유

조건부 명제 P → P를 예로 들면 구조가 선명해진다. 이 명제의 증명 항은 P의 증거 p를 입력받아 같은 p를 반환하는 함수다. 명제를 형으로, 증명을 그 형의 값으로 보는 관점에서 커널은 이 함수가 실제로 P → P라는 형을 갖는지 계산하고 확인한다.

반대로 AI가 P의 증거를 받지 않은 채 임의로 P를 반환하려 한다고 가정하자. 사용할 수 있는 공리나 기존 정리가 없다면 그런 항을 구성할 수 없다. 자연어 설명이 그럴듯하거나 추론 과정이 길어도 존재하지 않는 증거를 대신하지 못한다.

복잡한 자동 증명도 판정 원리는 같다. 생성 과정에서는 탐색, 실패, 수정과 확률적 선택이 일어날 수 있지만, 최종 승인은 제출된 항이 목표 형을 갖는지에 달려 있다. Lean은 AI의 사고 과정을 인증하는 시스템이 아니라 AI가 남긴 형식적 산출물을 검사하는 시스템이다.

독립 검사기가 신뢰 범위를 더 줄인다

Lean의 신뢰 기반에는 편집기, 모든 전술, 최적화기와 코드 생성기 전체가 반드시 포함되지 않는다. Lean 공식 FAQ의 증명 객체 설명 에 따르면 소스와 전술은 명시적인 증명 항을 만들며, 이 객체는 주 Lean 프로세스와 분리된 프로세스나 다른 컴퓨터의 검사기로 다시 확인할 수 있다. 여러 검사기를 이용하면 한 구현의 결함에만 결과를 맡기는 위험도 줄일 수 있다.

독립 검사가 모든 위험을 없애는 것은 아니다. 검사기들이 같은 논리적 결함을 공유할 가능성, 증명 객체를 전달하는 형식의 문제, 검사 대상 정리 문장의 바꿔치기 같은 위협은 별도로 다뤄야 한다. 중요한 점은 신뢰의 대상을 거대한 생성 시스템 전체에서 비교적 작고 독립적으로 구현 가능한 형 검사기로 좁힐 수 있다는 데 있다.

정교화기 오류도 완전히 무해하지는 않다. 올바른 증명을 거부하거나 사용자가 예상하지 않은 명제를 구성해 작업을 왜곡할 수 있다. 다만 논리 규칙에 맞지 않는 항을 유효한 증명으로 승인하는 문제는 최종 검사기와 기반 논리의 건전성에 집중된다.

1300만 줄 사례에서 실제로 검사된 것

대규모 형식화에서 커널은 1300만 줄을 하나의 수학적 이야기처럼 이해하지 않는다. 프로젝트는 정의와 보조정리의 의존 관계로 나뉘며, Lean은 정교화된 각 선언이 앞서 승인된 선언을 이용해 올바른 형을 갖는지 검사한다. 규모가 커져도 최종 판정에 쓰이는 핵심 유형 이론의 규칙은 달라지지 않는다.

Anthropic의 형식화 보고 에 따르면 Claude 에이전트들은 11일 동안 1300만 줄의 Lean 코드를 작성했고, 3만300개 정리를 증명했으며 그중 2만9500개를 최종 증명에 사용했다. 완성된 페르마의 마지막 정리 증명은 Lean으로 검사됐고, comparator는 증명한 정리 문장이 Mathlib의 해당 문장과 일치하는지도 확인했다.

따라서 제목의 “1300만 줄도 커널이 검사한다”는 말은 원시 텍스트의 줄마다 진위를 판정한다는 뜻이 아니다. 그 코드에서 정교화된 정의와 증명 항이 커널의 형 검사를 거쳤다는 의미다. 줄 수는 증명의 난도나 신뢰 수준을 직접 측정하는 값이 아니라 생성되고 관리된 코드의 규모를 보여주는 수치다.

같은 결과를 다시 확인하려면 논리적 통과 외에도 사용한 Lean과 라이브러리 버전, 의존성, 빌드 환경이 필요하다. 환경이 달라지면 정교화 결과나 참조 가능한 정의가 달라질 수 있다. 커널은 재현 환경을 대신 관리하지 않지만, 재현된 증명 항의 논리적 유효성을 판정하는 마지막 경계가 된다.

커널이 막지 못하는 세 가지

첫째는 잘못된 명세다. 원래 문제의 중요한 조건을 빠뜨린 정리를 만들면 커널은 그 누락을 추측하지 않는다. 작성된 정리를 완벽히 증명해도 자연어로 의도한 문제의 답이 아닐 수 있다.

둘째는 원하지 않은 공리다. 선언되어 사용된 공리는 증명의 전제로 취급된다. 결론에 지나치게 가까운 가정이나 프로젝트에서 허용하지 않는 공리를 추가하면 항은 형 검사에 성공할 수 있어도 기대한 성과로 인정하기 어렵다.

셋째는 외부 세계와의 대응이다. 프로그램 사양, 센서 측정값, 데이터에 관한 전제가 현실과 일치하는지는 커널 밖의 문제다. Lean은 입력된 형식 모델 내부의 도출을 검사할 뿐 현실을 관찰해 전제를 확인하지 않는다.

이 세 경계 때문에 성공 표시만으로 증명의 의미를 판단할 수 없다. 정확한 정리 문장, 참조하는 정의, 사용된 공리와 의존 라이브러리를 함께 봐야 한다. 엄밀한 표현은 “AI가 이 명제를 무조건 참으로 만들었다”가 아니라 “이 정의와 공리 아래에서 구성된 증명 항이 커널 검사를 통과했다”다.

결국 무엇을 신뢰하는가

Lean은 AI 전체를 신뢰 목록에 넣지 않는다. 생성 모델과 전술은 후보 증명을 생산하고, 정교화기는 이를 핵심 언어의 항으로 바꾸며, 작은 커널은 그 항이 목표 명제의 형을 갖는지 판정한다. 필요하면 동일한 증명 객체를 독립 검사기로 다시 확인해 특정 구현에 대한 의존도도 낮출 수 있다.

그 결과 검토 대상은 모델의 막연한 신뢰도에서 명세, 정의, 공리, 증명 항과 검사기로 좁혀진다. 이 구조가 보장하는 것은 정해진 형식 체계 안의 논리적 타당성이다. 명세의 의미와 현실 전제까지 함께 검토해야 비로소 AI가 만든 증명이 실제로 주장하려던 내용을 입증했는지 판단할 수 있다.

함께 읽기:

• AIR에 5000만 달러…AI 에이전트의 플러그인까지 검사한다