우리는 지금 의존 타입의 미래에 살고 있습니다

2026년 10월 8일 · 태그: ai, mathematics, formal-methods · 원문 · 한국어 번역(원문에서 변경됨)

9월 4일부터 10월 7일까지 34일 동안 다음과 같은 일들이 일어났습니다. Claude가 Lean으로 페르마의 마지막 정리를 형식화했습니다. OpenAI는 나비에-스토크스 방정식의 유한 시간 폭발(finite-time blowup)을 발표했습니다. 이 결과는 1만 개의 에이전트가 88시간 만에 찾아낸 것으로, Lean 형식화도 함께 첨부되었습니다. 한 모델은 코트(Khot)의 유일 게임 추측(Unique Games Conjecture)을 증명했습니다. 또 다른 모델은 두 정수를 $n\log n$보다 빠르게 곱했는데, 지수 개선 폭은 $2^{-182}$입니다(그러니 GMP에 곧 들어가리라고 기대하지는 마십시오!). 유리 호지 추측(rational Hodge conjecture)이 CM 아벨 다양체에 대해 해결되었습니다. 그러고 나서 OpenAI는 어느 화요일에 372개의 새로운 수학 결과를 GitHub에 쏟아냈습니다. 그리고 이 모든 일이 겨우 한 달 사이에 일어났습니다. 이제 모두가 묻는 질문은 일반화된 리만 가설이 소용돌이치는 텐서의 웅덩이에 무릎 꿇기까지 얼마나 걸리겠느냐는 것입니다.

16개월 전에 저는 수학의 미래는 몹시 기이할지도 모른다고 썼는데, 아이고, 어느새 우리는 바로 그 기이한 미래에 와 있습니다. 그리고 이건 끝내주게 멋집니다.

지금 어느 데이터 센터에는 가속기로 가득 찬 건물이 사실상 상시로 돌아가면서 수학의 최전선에서 진리의 광산을 캐고 있습니다. 그렉 이건(Greg Egan)의 SF 소설 디아스포라에서처럼, propext, Quot.sound, Classical.choice라는 세 공리에서 바깥으로 굴을 파 나가며 결과를 밤낮없이 지상으로 끌어올리고 있습니다. OpenAI는 자사 모델에 약 8천 개의 문제를 내고(그중 약 5%를 풀었습니다) 문제당 평균 세 시간씩 생각하게 했는데, 이것은 느리고 수공예적이며 일반인 친화적인 버전입니다. 산업용 버전은 멈추지 않습니다. 그것은 어떤 인간 공동체가 읽어 낼 수 있는 속도보다 빠르게 결과를 쏟아낼 것이며, 그중 상당수는 옳고, 일부는 중요하며, 점점 더 많은 비율이 이해 불가능할 것입니다. 참이고(진리에 대한 어떤 뒤틀린 철학적 정의에 따르면), 기계로 검증되었으며, 누구도 이해하지 못하는 결과입니다. 인간이 수학을 이해한다는 것은 곧 사치품이 될 것입니다. 이 세상에 그 밖에 무엇이 필요하든, 모델이 결과를 만들어 내는 속도에 맞춰 참인 결과와 지어낸 결과를 가려낼 수 있는 무언가가 반드시 필요하며, 지금 그 무언가는 바로 의존 타입, 즉 Lean입니다.

미래가 하필 이런 모습을 띠게 되었다는 것이 얼마나 기이한 일인지 잠시 곱씹어 보겠습니다. 저는 20대의 상당 부분을 런던 FP 커뮤니티 주변에서 보냈는데, 그곳에서 의존 타입은 클러큰웰의 크라운 태번(Crown Tavern)에서 맥주를 마시며 이야기하던 주제였습니다(기억하시는 분들도 계실 것입니다). 값에 의존할 수 있는 타입, 그래서 함수의 시그니처가 단지 “리스트를 반환한다“가 아니라 “입력을 정렬한 순열을 반환한다“라고 말할 수 있고, 컴파일러가 그 약속을 지키도록 강제하는 타입 말입니다. 증명은 프로그램이고 명제는 타입이라는 관찰인 커리-하워드는 근본적인 북극성이었습니다. 늘 내세우던 주장은 언젠가 우리가 명세에 맞춰 소프트웨어를 작성하고 기계가 그것을 검사하게 되리라는 것이었고, 늘 돌아오던 대답은 그것이 종신 교수직이 있고 마감이 없는 사람들에게나 어울리는 멋진 아이디어라는 것이었습니다. Dependent Haskell은 약 15년 동안 “몇 년 뒤면 나온다“는 상태였습니다. Idris와 Agda는 여전히 소수 취향의 언어로 남았습니다. 소프트웨어 공학은 여전히 대부분 C++와 기도, 그리고 이따금의 어둠의 주문으로 굴러갑니다. 그런데도 의존 타입의 미래는 결국 뒷문으로 도착했습니다.

수학과 강화 학습이 먼저 그곳에 도달했습니다. 알고 보니 의존 타입의 언어의 킬러 애플리케이션은 그 타입 검사기를 보상 함수로 쓰는 것이었습니다. 타입 검사기는 후보 증명에 대해 부분 점수도, 의견도 없이 예 또는 아니요만 말해 주는 오라클이며, 이것이야말로 아주 거대한 최적화기를 미해결 문제에 겨누고 마음껏 돌리고 싶을 때 정확히 필요한 것입니다. 우리가 펍에서 꿈꾸던 것이 이제는 프런티어 연구소의 핵심 인프라가 되었으며, 위에 나열한 결과 대부분은 결국 타입 검사기가 참을 반환했다는 주장입니다.

그렇기 때문에 우리에게는 더 나은 도구가 필요하며, 그것도 최대한 빨리 필요합니다. 의존 타입의 르네상스가 도래했고 형식화된 수학의 황금기가 눈앞에 와 있지만, 이제 이러한 데이터 센터의 내부 루프는 밤낮없이 의존 타입 커널을 돌리며 엄청난 속도로 엘라보레이션하고, 검사하고, 폐기하고, 재시도하고 있으며, 그 출력을 인증하는 것 역시 같은 속도로 돌아가야 합니다. 탐색이 마이크로초 단위로 돌아가는데 검증이 분 단위로 돌아간다면 검증이 병목이 되며, 신뢰의 병목은 슬그머니 건너뛰어지기 마련입니다. 이 시대의 가장 중요한 인식론적 질문인 “이 증명이 정말로 올바른가“에 대한 답을 어쩌다 따라잡을 만큼 빨랐던 검사기가 내리는 상황에 놓여서는 안 됩니다.

Mathlib 1분 장벽 돌파하기

생리학적으로 불가능한 일에서 이제는 동호회 러너들이 목표로 삼아 훈련하는 일이 된 1마일 4분 기록처럼, 형식 수학에도 한동안 고유의 장벽이 있었는데, 바로 Mathlib 전체를 처음부터 1분 안에 타입 검사하는 것입니다. 이제 이것은 충분히 달성 가능한 일로 드러났습니다.

nano-lean은 Lean 커널 언어를 위한 최소한이지만 완전한 타입 검사기로, 바인더에 대한 효율적인 de Bruijn 인덱스를 다루기 위해 제가 만든 바인딩 라이브러리 unbound를 기반으로 Rust로 작성되었습니다. 이 도구는 Lean 환경의 익스포트를 읽어 들여 모든 선언을 처음부터 독립적으로 다시 검사합니다(귀납 타입, 양성 조건, 재귀자, 몫, 유니버스 레벨, 프로젝션, 구조체 에타 등 전부를 검사합니다). Apple Silicon M5 Max에서 Mathlib 전체, 즉 718,577개의 선언을 오류 0건, 타임아웃 0건으로 11.85초 만에 검사합니다.

그 속도의 놀랄 만큼 많은 부분은 텍스트를 파싱하지 않는 데서 나옵니다. Lean에서 선언을 꺼내는 표준적인 방법은 한 줄에 JSON 객체 하나씩을 기록하는 lean4export인데, 수 기가바이트에 달하는 JSON을 파싱하는 일이 무언가를 검사하는 비용의 상당 부분을 차지하는 것으로 드러났습니다. 그래서 nano-lean의 동반 도구인 olean-export는 컴파일된 .olean 파일을 직접 읽어 모듈을 병렬로 디코딩하는데, Mathlib에 의존하는 라이브러리에서 lean4export보다 약 100배 빠르며, 빠른 mmap을 위해 설계된 새로운 바이너리 포맷인 blean을 출력할 수 있습니다. Blean은 NDJSON 익스포트와 같은 레코드 스트림을 같은 순서로 담고 있으며, 파싱할 것이 전혀 남아 있지 않습니다. 모든 레코드는 간결한 postcard 인코딩이고, id는 암묵적이며 빈틈없이 조밀하고, 레코드는 앞선 id만 참조하며, 각 표현식은 미리 계산된 해시를 담고 있습니다. 검사기는 파일 전체를 mmap하고, 운영체제에 파일을 처음부터 끝까지 한 번만 읽을 것이라고 알린 뒤, 매핑된 바이트에서 곧바로 이름, 레벨, 표현식을 디코딩하여 항 아레나에 넣습니다. 파싱 단계가 아예 없습니다. 디스크상의 바이트가 이미 메모리 내 데이터의 형태와 거의 같으며, 바로 이것이 Mathlib을 1분 안에 검사하는 방법입니다.

같은 기법은 최첨단 결과에도 통합니다. 다음은 nano-lean이 14개 스레드를 사용하는 M5 Max에서 각 라이브러리와 증명의 임포트된 전체 환경을 검사한 결과입니다.

Mathlib의 커널 시간을 선언 수로 나누면 선언 하나당 분할 상환 기준 10.5마이크로초가 나옵니다. 이것이 중요한 수치입니다. 릴리스 파이프라인 끝단에 놓이는 검사기가 아니라, RL 기반 탐색 루프 깊숙한 곳에서 수천억 번 호출되는 검사기에 걸맞은 자릿수이기 때문입니다. 10년에 걸친 자원봉사자들의 노력의 산물인, 인간이 형식화한 수학 라이브러리 전체가 에스프레소 한 잔을 내리는 시간보다 짧은 시간 안에 재검증됩니다.

마침 Google Cloud에 m2-ultramem-416도 하나 놀고 있었기에(누구나 그렇듯 vCPU 416개와 RAM 12 TB짜리입니다), 자연스럽게 nano-lean을 거기에 돌려 보았습니다. 네, Mathlib 10초 장벽을 깹니다. 하지만 암달의 법칙이 안부를 전해 오고, 의존성 그래프가 나눠 줄 독립적인 작업이 바닥나면서 코어 수가 백 개를 넘어가는 어딘가에서 곡선이 급격히 평평해집니다. 알고 보니 Mathlib이 너무 작은 것입니다. 미래의 Mathlib이나 Tau Ceti 같은 것이 이 머신을 실제로 포화시킬 만큼 커지는 날을 고대합니다. 그것이야말로 진정한 미래입니다!

제가 이것을 만든 것은 병목이 어디로 옮겨 갔는지를 보여 주기 위해서입니다. 커널은 이제 새로운 종류의 과학 경제에서 핫 루프이며, 핫 루프는 핫 루프답게 엔지니어링되어야 마땅합니다. 형식 증명이라는 거래 전체는 하나의 비대칭성 위에 서 있습니다. 증명을 찾는 데는 프런티어 모델이 세 시간 동안 사고하거나 1만 개의 에이전트가 88시간 동안 작업해야 할 수도 있지만, 그것을 검사하는 데는 마이크로초면 충분해야 합니다. 바로 그 비대칭성 덕분에 어떤 인간도 읽지 않은 결과를 신뢰하는 것이 합리적인 일이 됩니다. 이는 검사기가 실제로 확장될 때에만 성립하며, 페르마의 마지막 정리가 이제 Mathlib의 다섯 배 규모에 이르는 지금, 규모는 더 이상 가정의 문제가 아닙니다. 이제 Mathlib은 작은 라이브러리입니다.

다만 사는 사람이 주의해야 합니다(caveat emptor). nano-lean은 적절한 수준의 저수준 Rust 내공만 있으면 이것이 가능하다는 것을 보여 주기 위해 만든 개념 증명입니다. 그렇긴 하지만, 저희는 OneChronos에서 상당히 과도하게 커져 버린 시장 인프라에 관한 대규모 Lean 증명을 검사하는 데 이것을 내부적으로 실제로 사용하고 있습니다. 이것은 공식 Lean 커널만큼 신뢰할 수 있는 수준에는 한참 못 미칩니다. 공식 커널은 수년간의 검증과 전문가 커뮤니티, 그리고 지금까지 실행된 모든 Mathlib 빌드를 뒷배경으로 두고 있으며, 같은 라이브러리를 검사하는 데 약 15분이 걸립니다. 제 주장은 그보다 범위가 좁으며, 제 생각에는 더 흥미롭습니다. 이 정도 속도의 검사는 충분히 가능하므로, 우리는 몇 분이라는 시간을 신뢰의 당연한 비용으로 여기는 것을 멈추고 빠르면서도 신뢰할 수 있는 검사기를 만들기 시작해야 합니다. 미래의 Lean 컴파일러는 rustc나 clang만큼 엄청나게 빨라질 수도 있습니다.

미래의 모습

작년의 이전 글에서 저는 수학자들이 다락방에서 고군분투하는 앤드루 와일스보다는 GitHub에서 풀 리퀘스트를 처리하는 소프트웨어 엔지니어에 더 가까운 모습이 될 것이라고 예측했습니다. 역사상 단일 발표로는 가장 큰 규모의 새로운 수학은 CONTENTS.md, Lean 라이브러리, v4.34.1에 고정된 lean-toolchain 파일, 그리고 “수정 및 개정 사항은 새 버전으로 기록될 것“이라는 약속과 함께 GitHub 저장소 형태로 공개되었습니다. 그러니까, 네, 그 일은 실제로 일어났습니다.

저는 AI 시스템이 형식화된 미해결 추측 목록에 투입되어 체계적으로 최전선을 밀어붙이려 할 것이라고 예측했습니다. 8천 개의 문제를 각각 세 시간씩 다뤘습니다. 적중했습니다.

저는 리만 가설을 맡은 데이터 센터가 몇 주 뒤에 어떤 인간도 따라갈 수 없는 증명을 들고 돌아올 것이라고 예측했습니다. 우리가 얻은 것은 준리만 가설, 즉 모든 디리클레 $L$-함수가 $\Re s>7/8$에서 영점을 갖지 않는다는 결과와 Lean 페이지였으며, 이는 그토록 섬뜩하지만 않았다면 웃겼을 법한 종류의 아슬아슬한 빗나감입니다. 그리고 불가해성도 예정대로 도착했습니다. OpenAI는 열 개의 계열에 대해 “추론 요약“을 공개했는데, 알고 보니 이는 추론 트레이스 발췌문의 요약으로, 모델이 실제로 한 일로부터 두 단계나 떨어져 있는 것이었습니다.

저는 백만 달러짜리 밀레니엄 상금이 GPU 청구서의 100분의 1 정도는 메워 줄지도 모른다고 농담했습니다. 나비에-스토크스 실행에는 약 1,300억 개의 토큰이 소모된 것으로 알려졌습니다. 그러니 확실히 그렇습니다.

제가 틀린 것은 시기였습니다. 작년에 저는 “아직 그 단계에 이르지 못했습니다. 근처에도 가지 못했습니다.“라고 썼습니다. 그로부터 16개월이 걸렸습니다. 체스 비유도 아마 틀렸을 것입니다. 저는 Stockfish와 체스의 경우처럼, 기계가 수학을 덜 대중적이고 덜 접근하기 쉽게 만드는 것이 아니라 오히려 더 대중적이고 더 접근하기 쉽게 만들 것이라고 주장했습니다. 장기적으로는 그럴지도 모릅니다. 단기적으로 현업 수학자들 사이의 분위기는 실존적 위기에 더 가깝고, 미해결 문제는 경력 파이프라인, 보도자료에 연구 성과를 선점당하는 박사과정 학생들, 그리고 지금까지 만들어진 가장 강력한 수학 도구가 미공개 모델을 운영하는 소수의 민간 기업 안에 집중되는 현상에 관한 것입니다.

제가 완전히 놓친 것은 병목이 결국 배관 작업, 즉 인프라 문제로 드러나리라는 점이었습니다. 저는 괴델과 불가해한 증명의 인식론에 여러 단락을 할애했지만, 실제로 가장 먼저 부딪힌 문제는 OpenAI의 Lean 라이브러리가 수만 개의 파일에 걸쳐 소스만 1기가바이트가 넘는다는 것이었고, 그들의 README에는 Linux의 vm.max_map_count가 너무 낮아서 빌드가 실패할 수 있다고 경고하며 Lean을 -DMMAP=OFF로 다시 컴파일하는 우회 방법을 제안하는 절이 있습니다. 철학적 문제는 여전히 남아 있습니다. 하지만 지금 수학의 최전선을 가로막고 있는 것은 커널 조정 매개변수 하나입니다. 우리가 원했던 미래는 아니지만, 어쩌면 우리에게 걸맞은 미래일지도 모릅니다!

검사기는 누가 검사하는가

지금까지 제가 말한 모든 것에 대한 명백한 반론은 Lean 증명은 Lean만큼만 신뢰할 수 있다는 것입니다. 그리고 그것은 정말 맞는 말입니다!

Lean은 다른 모든 증명 보조기와 마찬가지로 작고 신뢰할 수 있는 커널과, 그 밖의 매우 크고 신뢰할 수 없는 나머지 전부(엘라보레이터, 전술 프레임워크, 컴파일러, 빌드 시스템)로 이루어져 있습니다. 설계 자체는 건전합니다. 정확해야 하는 유일한 코드는 커널이며, 커널은 읽을 수 있을 만큼 작습니다. 하지만 “읽을 수 있을 만큼 작다“는 것은 소스 코드를 설명하는 말입니다. 그것은 정확성에 대해 아무것도 보장하지 않으며, Lean의 커널에는 과거에 건전성 버그가 있었고, 이는 역사상 모든 증명 보조기의 모든 커널도 마찬가지였습니다. 역사적으로는 그것을 감내할 수 있었는데, 상대가 자기 증명이 통과되기를 바랄 뿐 False가 타입 검사를 통과하게 만드는 방법을 찾아다니는 데는 아무 관심이 없는, 굶주린 인간 대학원생이었기 때문입니다. 그 가정은 이제 낡은 것이 되었습니다.

저는 지난달에 보상 해킹에 대해 썼습니다. 보상 해킹이란 최적화기가 목표의 의도가 아니라 문자 그대로의 조건만 충족시키는 습성을 말합니다. Lean 파일을 컴파일되게 만들라는 지시를 받은 에이전트는, 충분한 연산 자원과 충분한 시도 횟수가 주어지면, 여러분의 커널을 겨냥한 극도로 부지런한 퍼저가 됩니다. 그 에이전트가 속이려는 의도를 가질 필요는 없습니다. 검사기가 받아들여서는 안 되는데도 받아들이는 항을 단 한 번만 우연히 찾아내면 충분하며, 나머지는 경사가 알아서 처리합니다. 증명기가 적대적인 최적화기라면 단일 커널은 단일 장애점이 되며, 건전성 버그는 더 이상 민망한 GitHub 이슈에 그치지 않고 가짜 정리를 대량으로 찍어 내는 장치가 됩니다.

답은 컴파일러 세계가 도달한 답과 같습니다. Csmith가 무작위 C 프로그램을 생성하고 이를 여러 컴파일러로 컴파일해 결과를 비교하기 시작하자, 수십 년간의 일상적인 사용에서도 발견되지 않았던 GCC와 LLVM의 버그 수백 개를 찾아냈습니다. 다양성과 차등 테스트(differential testing)의 조합은 단일 구현을 아무리 꼼꼼하게 검토하는 것보다도 낫습니다. 증명 검사에서 이는 서로 다른 사람들이 서로 다른 언어와 서로 다른 표현 방식으로 작성한 여러 독립적인 커널이 모두 같은 익스포트 형식을 입력으로 받고, 모두 같은 판정을 내려야 한다는 뜻입니다. Mario Carneiro의 lean4lean과 Chris Bailey의 nanoda가 이 분야를 일찍 개척했습니다. nano-lean은 세 번째 도구인 nl-mutate를 제공합니다. 이 도구는 유효한 익스포트를 받아 의미를 깨뜨리는 작은 변이를 가하고, 사용 가능한 모든 검사기를 실행한 뒤, 판정이 엇갈리는 경우를 보고하면서 각각을 재현 가능한 최소 사례로 축소합니다. 모든 판정 불일치는 누군가의 커널에 있는 버그이거나 타입 이론 명세의 모호함이며, 둘 다 GPU 팜이 대신 찾아내기 전에 미리 알아 둘 가치가 있습니다.

신뢰의 나머지 절반은 명제입니다. 잘못된 정리에 대한 증명은 아무리 완벽하게 검사되었더라도 무가치하며, 증명 검사기를 속이는 가장 효과적인 방법은 지금까지 한 번도 커널을 깨뜨리는 것이 아니었습니다. 그것은 증명 대상이 사람들이 실제로 관심을 두는 대상에서 멀어질 때까지 명제를 조용히 약화시키는 것입니다. OpenAI의 저장소가 제출된 증명을 별도로 명시된 과제 명제와 대조하여 샌드박스 안에서 검사하는 Comparator에 의존하는 것도, 바로 이곳이 이제 진정한 신뢰 경계가 놓인 자리이기 때문입니다. 모델이 완강한 목표를 붙잡고 끈질기게 씨름하는 모습을 지켜본 사람이라면, 모델이 가장 지루한 방식으로 속임수를 쓰는 고약한 경향이 있다는 것을 압니다. 모델은 마침 자신에게 필요했던 보조정리와 정확히 일치하는 axiom을 슬그머니 도입하거나, 파일 세 단계 깊숙이 sorry를 묻어 두거나, 표기법이나 매크로를 재정의하여 페이지에 적힌 명제가 더 이상 겉보기와 같은 의미를 갖지 않게 만들거나, native_decide에 손을 뻗어 컴파일러 전체를 신뢰 기반 안으로 끌어들입니다. 이러한 속임수는 커널을 우회하기 때문에 이 모든 과정에서 커널은 완벽하게 건전한 상태를 유지하며, 유일한 방어책은 명제를 독립적으로 고정하고 증명이 실제로 무엇에 의존하는지 검사하는 것입니다. 누군가는 추측을 형식화해야 하고, 누군가는 그 형식화가 영어 문장이 뜻하는 바를 그대로 뜻하는지 확인해야 합니다. 그 일은 과정의 다른 어떤 부분보다도 오래 남을 것입니다. 오히려 인간의 수학적 안목은 증명을 작성하는 일에서 벗어나 명세를 작성하고 감사하는 일로 옮겨 가게 될 것입니다.

이것이 하나의 작업 방식으로서 어떤 모습인지 그 씨앗을 보고 싶다면, Mathlib의 하위에 있는 Lean 라이브러리인 Tau Ceti를 살펴보십시오. 핵심은 바로 분업에 있습니다. 인간은 별도의 저장소에 마크다운으로 로드맵을 작성하고, 리뷰 기준표도 인간이 작성합니다. AI는 모든 코드를 작성하고, 풀 리퀘스트를 열고, AI 주도의 리뷰 과정을 거쳐 이를 이끌어 갑니다. 기준표는 명시적으로 적대적이며, 잘못된 형식화, 공허한 명제, 그리고 “카펫 아래 혹을 이리저리 밀어 옮기는 것“을 찾아내라는 지침을 담고 있습니다.

지금 Lean에 필요한 것

Lean은 탁월한 공학적 산물입니다. 하지만 Lean은 특정한 사용자, 즉 Emacs에서 택틱을 입력하고 인포뷰가 갱신되기를 기다리며 자원봉사자 커뮤니티가 풀 리퀘스트를 리뷰할 수 있는 속도에 맞춰 라이브러리를 만들어 가는 가난한 대학원생을 중심으로 설계되었습니다. 이제 사용자는 11일 만에 1,300만 줄을 작성하는 에이전트 무리입니다. 도구는 새로운 작성자들에 맞게 성숙해져야 하며, 그것이 무엇을 의미하는지에 대한 목록은 상당히 구체적입니다.

표면 포매터. Lean에는 아직도 rustfmt나 gofmt 같은 정식의, 널리 채택된 포매터가 없으며, 작성자가 수백만 줄을 생산하는 에이전트라면 에이전트마다 제각기 들여쓰기, 줄 바꿈, 전술 배치 방식을 만들어 냅니다. diff는 잡음으로 가득 차고, 리뷰는 어려워지며, 에이전트 간 중복 제거는 공백만 다른 증명들을 놓칩니다. Lean이 매우 큰 언어로 성장했기 때문에, 이는 의외로 어려운 문제입니다. Lean의 문법은 런타임에 확장할 수 있으므로, import된 파일에서 선언된 표기법, 매크로, 그리고 전술 언어 전체가 이후 파일의 파싱 방식을 바꿉니다. 포매터는 고정된 문법을 읽기만 해서는 안 됩니다. 포매터는 환경을 불러오고, 모든 구문 확장이 스코프에 있는 상태에서 실제 파서를 실행한 다음, 사용자 정의 표기법에 따라 모양이 달라지는 구문 트리를 보기 좋게 출력해야 하며, 그동안 주석을 그대로 왕복 보존하고 코드의 의미는 절대 바꾸지 않아야 합니다. 이는 진정으로 어려운 엔지니어링 과제이며, 이제는 기본 요건이 되었습니다.

공개 인터페이스로서의 안정적이고 명세된 내보내기 형식. 독립적인 커널은 C++ 런타임에 링크하고 olean을 직접 읽지 않고도 Lean에서 선언을 꺼낼 수 있는 잘 정의된 방법이 있어야만 가능합니다. lean4export와 olean-export 같은 도구는 이미 NDJSON을 생성하며, blean은 메모리 매핑을 전제로 설계된 같은 스트림의 바이너리 형식이 내보내기 비용을 거의 없앨 수 있음을 보여 줍니다. OpenAI 자체의 검증 지침도 lean4export에 의존합니다. 그 형식은 와이어 프로토콜만큼 진지하게 다루어져야 합니다. 버전이 관리되고, 문서화되고, 식의 해싱까지 명세되며, 툴체인 릴리스 간에 안정적이어야 합니다. 내보내기 형식은 신뢰가 확립되는 경계입니다. 그러니 명세를 갖출 자격이 있습니다.

일급 시민으로서의 독립 검사. 두 번째 커널을 실행하는 일은 린터를 실행하는 것만큼 평범한 일이 되어야 합니다. Mathlib CI, Comparator 워크플로, 그리고 형식적 결과를 발표하는 모든 연구소는 서로 무관한 커널을 최소 두 개 사용해 내보낸 결과를 재검사하고, 커널들의 판정이 엇갈리는 것은 무엇이든 승인을 거부해야 합니다. Mathlib 전체를 검사하는 데 1분도 걸리지 않는 지금, 이는 저렴한 일입니다.

실행 파일만이 아닌 라이브러리로서의 검사기. 증명 에이전트의 내부 루프는 이미 로드되어 준비된 환경에 대해 후보 선언 하나를 제출하고 마이크로초 단위로 판정을 받기를 원합니다. 프로세스 시작, olean 재읽기, 수 기가바이트에 달하는 환경의 재역직렬화는 사람이 1분에 한 번 저장 버튼을 누르던 시절에는 전혀 문제가 되지 않던 비용입니다. 탐색 절차가 시간당 백만 개의 후보를 검사할 때는 이러한 비용이 대부분을 차지합니다. 커널은 영속적인 환경, 선언의 점진적 추가, 그리고 탐색 하네스가 촘촘한 루프 안에서 호출할 수 있는 API를 갖추고 임베드할 수 있어야 합니다.

메모리와 규모. Mathlib을 검사하려면 수 기가바이트의 메모리가 필요합니다. FLT 형식화는 그보다 다섯 배 크며, OpenAI의 라이브러리는 이미 Linux 가상 메모리 한도를 넘어서고 있습니다. Lean은 import된 모든 모듈을 mmap하는데, 이는 수천 개 파일로 이루어진 라이브러리에는 합리적인 설계이지만 수십만 개 파일에는 불합리한 설계입니다. 항 공유, 모듈 간 해시 콘싱, 간결한 디스크상 표현, 그리고 증명이 의존하는 선언만 정확히 지연 로딩하는 것은 지루하고 화려하지 않은 엔지니어링 문제이지만, 형식 수학이 다음 자릿수의 규모로 확장될 수 있을지를 결정합니다.

진짜 비용은 정교화입니다. 커널은 빠른 부분입니다. Mathlib을 소스에서 빌드할 때 비용이 큰 부분은 단일화, 타입 클래스 해석, simp, omega, decide, 그리고 수많은 전술을 거느린 정교화기입니다. 콜드 빌드는 여전히 CPU 시간 단위로 측정되며, 후보 증명을 대규모로 정교화하는 채굴 작업은 그 비용을 계속해서 반복해 치릅니다. 병렬 및 점진적 정교화, 더 나은 타입 클래스 인스턴스 캐싱, 그리고 simp 호출 한 번에 왜 4초가 걸렸는지 알려 줄 수 있는 프로파일링 도구야말로 증명 루프에서 실제 경과 시간의 대부분이 소모되는 지점입니다.

Clippy 스타일 린터. Mathlib에는 이미 훌륭한 린터들이 갖춰져 있지만, 에이전트에게는 Rust의 clippy에 더 가까운 것, 즉 기계가 작성한 Lean이 잘못되는 특정한 방식들을 겨냥한, 크고 주관이 뚜렷한 린트 목록이 필요합니다. 엉뚱한 곳에 놓인 axiom, 깊숙이 묻힌 sorry, 불필요한 native_decide, 보조정리로 분리되어야 할 마흔 줄짜리 simp only, 가정이 서로 모순되어 공허하게 참이 되는 정리, 표준적인 무언가를 가리는 지역 표기법, 라이브러리에 이미 있는 증명을 중복하는 복사-붙여넣기 증명을 표시하십시오. 각 린트는 비용이 적게 들고, 기계가 읽을 수 있어야 하며, 수정 제안을 함께 제공해야 합니다. 사람이라면 경고를 대충 훑어보고 넘기겠지만, 이를 소비하는 쪽은 모든 경고에 대해 조치를 취할 탐색 루프이기 때문입니다. 린터는 안목을 대규모로 인코딩하는 방법이며, 안목이야말로 에이전트에게 가장 눈에 띄게 부족한 것입니다.

기계 규모의 검색. Moogle, Loogle, LeanSearch는 사람이 어렴풋이 기억하는 보조정리를 찾도록 돕기 위해 만들어졌습니다. 에이전트에게도 같은 것이 필요하지만, 그 규모는 라이브러리가 일주일에 수백만 줄씩 늘어나고, 그 안에 있는 것의 대부분을 다른 에이전트가 작성했으며 사람이 한 번도 들여다본 적이 없는 수준입니다. Anthropic이 FLT에 사용한 Prove2Me 플랫폼은 바로 에이전트들이 서로의 작업을 찾아 재사용할 수 있도록 자연어 설명이 붙은 정리 명제들의 DAG를 유지합니다. 지금까지 증명된 모든 것에 대한 살아 있는 검색 가능한 색인이라는 그 아이디어는, 각 연구소가 비공개로 다시 만드는 무언가가 아니라 공유 인프라가 되어야 합니다.

출처. 현세대 모델들은 자신이 사용하는 기법에 대해 문헌을 인용하는 데 서툴기로 악명이 높습니다. 증명 항은 자신이 어떤 보조정리에 의존하는지는 정확히 알지만, 그 아이디어가 어디에서 왔는지는 전혀 알지 못합니다. 기계가 생성한 수학이 아무도 읽지 않는 부록처럼 인간의 문헌 옆에 놓여 있는 것이 아니라 그 안에 통합되려면, 증명은 자신의 이력(어떤 모델, 어떤 실행, 어떤 선행 결과, 논증이 기대고 있는 어떤 사람이 쓴 논문)을 지니고 다녀야 합니다.

이 중 어느 것도 그리 낯선 것은 아닙니다. 이는 산업화를 거친 다른 모든 분야가 겪어 온 종류의 인프라입니다. 컴파일러는 테스트 스위트와 여러 구현을 갖추게 되었고, 네트워크 프로토콜은 RFC를 갖추게 되었으며, 데이터베이스는 형식적인 격리 수준과 Jepsen을 갖추게 되었습니다. 증명 보조기는 그 모임의 가장 새로운 구성원이며, 이전의 그 어떤 것보다도 빠르게 산업화되고 있습니다. 제가 젊고 야심 찬 프로그래머라면, 투자 대비 가장 높은 수익을 위해 초기 경력을 바로 이 분야에 집중하겠습니다.

현실 세계를 위한 커리-하워드

제가 술집에서 약속받았던 의존 타입의 미래는 소프트웨어가 명세에 맞추어 작성되고 기계가 그것이 명세를 충족하는지 검사하는 미래였습니다. 실제로 우리가 얻은 것은 그보다 더 기묘합니다. 명세는 정리 명제이고, 소프트웨어는 증명 항이며, 저자는 에이전트 무리이고, 만들어지고 있는 것은 수학의 최전선 그 자체입니다. 결국 커리-하워드는 산업 인프라였던 것으로 드러났습니다. 다만 그곳에 이르기까지 강화 학습이 필요했을 뿐입니다.

그리고 이것은 이야기의 수학적인 절반에 불과합니다. 방금 페르마의 마지막 정리를 검사한 바로 그 장치는 정확하게 진술할 수 있는 것이라면 무엇이든 검사할 것이며, 가장 분명한 다음 고객은 산업용 소프트웨어입니다. 저는 지난달에 우리가 출시하는 것 중 증명은 고사하고 명세를 갖춘 것조차 거의 없기 때문에 소프트웨어가 형편없다고 주장했습니다. 그 변명은 사라지고 있습니다. 에이전트 무리가 2주도 안 되는 기간에 검증된 수학 1,300만 줄을 만들어 낼 수 있다면, 같은 기법을 소프트웨어 공학에 적용하는 날도 머지않았습니다. 연구소들이 수학을 먼저 채굴하는 이유는 그것이 협상해야 할 지저분한 현실 세계의 명세가 없는, 가장 깔끔하게 검증 가능한 영역이기 때문입니다. 다음은 소프트웨어이며, 소프트웨어에도 똑같은 도구들, 즉 빠른 커널, 다양한 검사기, 정직한 명제, 그리고 잠들지 않는 저자를 위해 만들어진 인프라가 모두 필요할 것입니다.

그러니 그렇습니다, 수학의 미래는 몹시 기묘한 것으로 드러났고, 그것도 제가 예상했던 것보다 훨씬 이르게 찾아왔습니다. 결과는 누구도 읽을 수 없을 만큼 빠르게 쌓이고 있으며, 우리 중 많은 사람이 스스로를 설명하지 못하는 무언가가 아침 식사 전에 증명해 낸 정리들을 이해하려 애쓰며 남은 경력을 보내게 될 것입니다. 저는 그것이 불안하게 느껴지면서도, 동시에 짜릿하게 느껴집니다.

마지막으로 염치없는 홍보를 하나 하겠습니다. 수학 형식화에 관한 블로그 글을 읽기보다 그 최전선에서 직접 일하고 싶으시다면, OneChronos에서 정형 기법 엔지니어를 채용하고 있습니다. 저희는 조합 경매(combinatorial auction)로 기관 시장을 구축합니다(Milgrom과 Wilson의 2020년 노벨상에서 이어진 것입니다). 조합 경매는 트레이더가 점점 더 매우 독특하고 표현력 있는 선호를 지닌 RL 루프가 되어 가는 세상에 꼭 맞는 수학적 정식화인 것으로 밝혀졌습니다. 저희 다크 풀은 미국 주식 시장 명목 거래량의 1% 이상을 처리하고 있으며, 이미 다른 여러 글로벌 자산군으로도 확장했습니다. 입사하시면 새로 꾸려진 정형 기법 팀에 합류하여 수학자, 시장 구조 전문가와 함께 Rust와 Lean으로 코드를 작성하게 됩니다. 의존 타입, 수치 최적화, 그리고 Lean을 활용해 매일 수천억 달러를 안전하게 움직입니다. 그런 부류의 너드이시라면 연락해 주십시오.