요약
Lean이 독립 커널 네 개를 함께 배포하며, 그중 두 개는 정확성이 증명됐습니다.
Lean과 Z3를 만든 레오나르도 드 모라가 쓴 글입니다. AI 에이전트가 Lean 커널(증명이 맞는지 최종 판정하는 검사기)의 허점을 잘 찾아내면서 8월에만 건전성 사고 보고서가 두 번 나왔습니다. 그래서 여러 커널로 증명을 다시 검사하는 체계를 내놓았습니다.
왜 중요한가
- 커널 하나의 구현 실수가 모든 증명의 신뢰를 흔들 수 있는데, 서로 다른 커널이 교차 검사해 그 위험을 줄입니다.
- 핵심 커널을 Claude가 구현하고 증명했습니다. AI가 만든 증명을 믿을 근거인 검사기까지 AI로 검증한 셈입니다.
- 수천만 줄짜리 증명이 나오면서 지금의 외부 커널 재검사 방식은 규모의 한계에 부딪혔습니다.
핵심 내용
- con-leche는 Lean으로 쓰고 일관성(받아들인 모든 정리가 집합론 모형을 갖는 성질)을 증명한 첫 커널입니다.
- con-leche는 Lean FRO의 요아힘 브라이트너가 감독했고, Mathlib 전체를 8스레드로 약 100초에 검사합니다.
- con-ron은 con-leche를 Rust로 옮긴 커널로, Aeneas로 같은 알고리즘임을 증명해 Lean 컴파일러 버그까지 견제합니다.
- Lean v4.35.0의
lake check --paranoid는 추가 커널 네 개와 메모리 손상 시 바로 멈추게 강화한 공식 커널로 모두 검사합니다. - 앤트로픽의 페르마의 마지막 정리 증명이 1,300만 줄에 이르자, 이진 내보내기와 증분 검사를 개발하고 있습니다.
HN 반응
- Lean만 있었다면 올해 수학 성과가 가능했겠느냐는 질문에, 형식화 경험자들은 사람 손으로는 10~1000배 느려 어렵다고 답했습니다.
- 수학 표기가 괜히 난해하다는 주장에는, 간결한 표기가 오히려 구조를 드러내고 형식화된 증명이 더 읽기 쉽지도 않다는 반론이 맞섰습니다.
Lean이 지금 수준으로 15년 전에 있었고, 수학계가 열성적으로 공용 코드 저장소에 대거 기여하기 시작했다고 가정해 봅시다. 올해 답이 나온 수학의 돌파구와 오랜 난제 중 얼마나 많은 것을 그때 풀었을 거라고 보시나요?
달리 말해, 올해의 진전 중 얼마만큼이 Lean을 쓰는 LLM 덕분이고, 얼마만큼이 영어와 LaTeX보다 Lean이 일부 수학 분야에서 훨씬 생산적인 언어이기 때문일까요?
올해 형식화된 양을 보면 이런 일이 더 일찍 일어날 수 없었다는 게 믿기 어렵습니다.
후속 질문입니다. 수학계의 이런 급격한 변화가 GitHub에서 인간들이 공을 나눠 가지며 집단으로 이뤄낸 결과였다면, 같은 결과를 거대 언어 모델이 만들어 냈을 때만큼 수학자들이 화를 냈을까요?
다시 말해 수학자들이 화난 건 거대 언어 모델 때문일까요, 아니면 형식화와 대규모 협업이 아주 효과적이라는 게 드러나면서, 문을 걸어 잠그고 혼자 사색하는 영웅적인 수학자의 이미지가 무너진 게 진짜 이유일까요?
한번 생각해 볼 거리입니다.
얼마 전 동료가 Lean은 C나 Python과 어깨를 나란히 하는, 모든 프로그래머가 읽을 줄 알아야 할 새로운 기초 언어 계열 같다고 하더군요. 저도 반박하기 어렵다고 생각합니다. 다음 세대 모델들은 점점 더 Lean으로 강화학습을 받을 겁니다. 경쟁사와의 수학 전쟁에서 이기는 데 도움이 되니까요. 그 덕은 Lean을 수학에 쓰는 사람뿐 아니라 범용 프로그래밍 언어로, 또 다른 DSL의 토대로 쓰는 사람도 보게 될 겁니다. 예를 들어 Sparkle(Lean 기반 HDL) 같은 것은 2026년과 그 이후에 충분히 의미가 있다고 봅니다.
https://github.com/Verilean/sparkle
(전직 수학 대학원생입니다. 수학 교재나 논문을 쓰는 전문 수학자라면 자명하다고 넘어갈 보조정리("일반성을 잃지 않고 ...라고 가정할 수 있다", "...임은 분명하다")를 Lean으로 형식화하느라 몇 주를 통째로 쓴 적도 있습니다.)
아마 거의 없거나 전혀 못 풀었을 겁니다.
이런 시스템은 (대체로) 새로운 수학을 발견하도록 도와주지 않습니다. 형식화를 위한 도구입니다.
그런데 이걸 LLM과 결합하는 것이 비법이었던 거죠. LLM은 창의성이 꽤 있지만 실수를 많이 합니다. Lean 타입 검사기는 절대 실수하지 않지만 창의성이 없습니다. 둘을 반복 루프로 함께 돌리면 지금 우리가 보는 결과가 나옵니다.
저는 수학과 학부생이고 Lean을 써 봤습니다. 아마 익숙함의 문제겠지만, 저는 여전히 Lean 증명이 자연어 증명보다 읽기 어렵습니다. 수학 교육이 (꼭 Lean이 아니더라도) 형식 언어로 완전히 바뀌면 어떻게 될지 궁금합니다.
모델에게(dsv4.1 flash가 이런 용도로 아주 좋습니다) 증명을 설명해 달라고 해서 먼저 전체 개념과 구조를 잡아 보세요. 형식화된 수학은 시각 피질이 없는 Lean이 처리하기 쉽도록 수학을 특정한 방식으로 인코딩하는 경향이 있고, 그래서 사람에게는 오히려 더 어렵습니다.
저도 수학과 출신(이자 개발자)인데, Lean이 증명을 읽기가 아니라 쓰기에 최적화되어 있다는 점이 늘 거슬렸습니다. 그래서 증명을 읽는 데 최적화된 언어를 만지작거리고 있습니다.
https://github.com/ityonemo/2b4m
그 대신 더 장황하지만, 이 언어를 모르는 사람도 증명을 제대로 해독할 수 있습니다.
이 언어를 시험해 보려고 Claude에게 온라인 대수학 교재를 형식화시켜 보고 있습니다.
https://github.com/ityonemo/2b4m/tree/main/aata
어떻게 생각하시는지 알려 주세요.
Claude 특유의 문체는 일단 제쳐 두고요.
비교 대상이 전술(tactic) 위주 언어뿐인데, 바로 그게 마음에 안 드신다는 거잖아요. Agda, Idris, Mikan 같은 것도 한번 보세요. 이쪽은 정의뿐 아니라 증명에도 패턴 매칭을 써서 유도 과정이 훤히 드러납니다.
그쪽 틈새시장에 가치가 없다는 말이 아니라, 거기서 흥미로운 아이디어를 얻을 수 있을 거라는 얘기입니다.
감사합니다, 좋은 조언이네요!
여담인데, Claude 특유의 문체는 어느 정도 일부러 그런 겁니다. 이 프로그래밍 언어는 Claude가 쓰고 Claude가 읽도록 만든 거라서요.
"수학은 보통 전달하기 쉬운 기호적이고 구체적인 형태로 설명되고 기록될 뿐, 일단 전달된 뒤에 이해하기 쉬운 개념적 형태로 설명되고 기록되지 않는다. 개념에서 구체적·기호적 형태로 옮기는 번역은 그 반대 방향의 번역보다 훨씬 쉽고, 그래서 기호적 형태가 개념적 이해의 형태를 대체하는 경우가 많다."
https://mathoverflow.net/questions/43690/whats-a-mathematician-to-do
그건 처음부터 혼자 시작하셨기 때문 아닐까요?
리눅스 커널 규모의 프로젝트를 상상해 보세요. 수천 명의 수학자가 잘 정리되고 주석이 충실한 코드를 쌓아 가며 서로의 어깨 위에 올라서는 겁니다.
(수학자는 아니고 취미로 Lean을 만져 봤습니다.) 아니요, 그런 건 이미 있었어요. Lean 표준 라이브러리가 사실상 그런 것이었고, 수백 명의 수학자가 협력해서 지금까지 알려진 수학의 기초를 형식화했습니다. 다만 사람에게는 이게 너무 느립니다.
(학부 수준이 아닌 실제 연구 수준의) 증명 하나를 형식화하려고 연구 그룹 전체가 달라붙은 사례도 있었던 걸로 기억하고, 페르마의 마지막 정리(FLT) 같은 건 지금은 형식화가 아예 불가능하다는 글을 읽은 기억도 있습니다.
한마디로, Lean은 새로운 수학을 발견하는 도구가 아니었습니다.
아닙니다. 케빈 버자드(Kevin Buzzard)가 이끄는 프로젝트가 FLT를 형식화하려고 몇 년째 진행 중입니다. 지난달 앤트로픽이 먼저 해냈지만, 그의 프로젝트는 단순히 형식 증명을 만드는 것 이상의 일을 합니다. https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/
앤트로픽이 FLT를 11일 만에 형식화했습니다: https://www.anthropic.com/research/formalizing-fermats-last-theorem
마지막 명제를 살짝만 바꿔도 여전히 성립하지 않나요?
덜 유용합니다. 사람은 실수가 더 적은 대신 생각을 Lean으로 옮기는 데 시간이 더 걸리니까요. 대부분의 수학자는 문제를 비형식적으로 생각하고 직접 이리저리 찔러 본 다음, 아이디어에 확신이 생기는 만큼 반복해서 형식화하며 더 빈틈없이 다듬을 때 성공률이 더 높을 겁니다.
이건 실증적으로 측정할 수 있나요?
속도가 엄청나게 중요합니다. 게다가 LLM이 상당히 창의적이 되어 가는 것 같기도 하고요.
요점은 검증해 볼 아이디어가 먼저 있어야 한다는 겁니다. Lean은 그걸 주지 않습니다.
그래도 LLM을 쓰는 인간이 LLM 혼자보다 훨씬 더 창의적이지 않을까요? 아니면 이 시스템에서는 인간이 오히려 창의성을 깎는다고 보시나요?
그렇다고 봅니다. 다만 제가 답했던 질문은 Lean과 함께 일하는 인간이 더 창의적이었을까 하는 것이었습니다.
네. 인간은 느리니까요.
단 하나도 못 풀었을 겁니다. 저는 LLM 이전 시대에 손으로 수학을 형식화해 본 경험이 좀 있는데, 형식 증명부터 만들며 시작한 적은 한 번도 없습니다. 너무 어렵거든요. 자연어 증명 대신 형식 증명으로 시작하는 수학자 이야기는 들어 본 적이 없는 것 같습니다. 자연어 증명 말고 형식 증명부터 시작하는 건 수레를 말 앞에 두는 격입니다.
자연어 증명이 없으면, 하다못해 자연어 증명을 어떻게 쓸지 감이라도 없으면 형식 증명을 쓰기가 매우 어렵습니다. 눈 감고 비행하는 거나 마찬가지예요. 전술을 맹목적으로 적용할 수는 있어도, 형식 증명을 이끌어 줄 큰 그림이 없으면 아주 사소한 증명이 아닌 이상 진척을 내기가 거의 불가능합니다. 중요한 증명이 자연어 증명보다 먼저 형식화된 적은 한 번도 없었다고 생각합니다.
예전에 형식 증명을 쓰는 일이 얼마나 노동집약적이었는지 사람들이 제대로 실감하지 못하는 것 같습니다. 사람이 형식 증명을 쓰는 데는 자연어 증명보다 시간이 10배에서 1000배는 쉽게 듭니다. 어떤 분야는 학부 수학 교재 한 권을 손으로 형식화하는 것조차 전문 수학자가 맡아도 몇 년짜리 프로젝트로 여겨졌습니다.
새 논문 하나를 형식화하는 데는, 이미 형식화된 정리 위에 쌓는 경우라도, 자연어 증명이 손에 있어도 몇 달이 걸릴 수 있습니다.
오픈AI가 형식 증명보다 자연어 증명을 먼저 공개하는 것도 놀랍지 않습니다. 아마 LLM에게도 같은 난이도 차이가 적용되겠죠.
오픈AI의 자연어 증명이 Lean 증명보다 먼저 나왔다면, 자동으로 검증할 수 없는 증명을 믿어야 했다는 얘기가 됩니다. Lean 증명이 나중에 공개되는 건 그게 덜 중요한 구현 세부 사항으로 여겨져서일 수도 있고, 시간이 걸리는 정리 단계가 있어서일 수도 있겠네요.
아니요, Lean으로의 변환은 자연어 증명이 끝난 뒤에 하는 두 번째 단계라고 이미 명시되어 있습니다. 그래서 400편이나 되는 논문 묶음 중 일부에 Lean 증명이 없는 겁니다.
Lean으로 변환하기 전에 증명이 맞다는 걸 어떻게 확신하는지 궁금하네요. LLM이 유효한 해답에 도달하도록 강제하는 작업 루프는 어떻게 짜여 있을까요? 그게 가능하다는 게 Lean을 쓰는 가장 큰 장점이라고 생각했거든요.
제 가설도 이것과 같습니다. 저는 매일 LLM과 일합니다. 최전선 모델을 늘 쓰고, 자체 특화 모델을 학습시키는 스타트업에서 일하고요. 일하는 내내 초인적 지능이라 할 만한 건 본 적이 없습니다. 제가 보는 건 초인적 멍청함, 즉 어떤 인간도 따라가지 못할 정도로 수십 배 극단적인 멍청함입니다. 그렇다면 초인적인 수학 결과는 어디서 나오는 걸까요? 간단합니다. 번역입니다. 저는 오래전부터 수학은 일부러 난해하게 만든 분야이고 프로그래밍으로 옮기면 훨씬 이해하기 쉬워진다고 생각해 왔습니다. 그러니 수학을 프로그래밍으로 번역하는 데 엄청난 연산 자원을 쏟아붓도록 기계를 훈련시키면, 사실상 난독화가 풀린 분야는 속수무책으로 무너집니다. 수학 증명은 일종의 불투명성에 기댄 보안이었던 겁니다. 정말로 엄청나게 어려운 게 아니라, 이 분야에 매달리는 사람이 전 세계에 극소수이고 그들의 작업이 심하게 난해했을 뿐인데, 난독화 해제 기계가 나타나 그 부분을 하찮게 만들어 버리니 갑자기 허울이 무너지는 겁니다. 인간이 난독화 해제를 했더라면 이 모든 게 훨씬 전에 이뤄졌을 거라고 생각합니다. 다만 프로그래밍과 수학 두 분야에 모두 정통한 전문성도, 그걸 발전시킬 금전적 유인도 충분하지 않았을 뿐이죠.
수학자들이 하는 말은 전혀 그렇지 않습니다. 수학자들은 LLM이 증명을 더 난해하게 만든다고 말합니다. 수학자들이 증명을 일부러 모호하게 쓴다는 건 말이 안 됩니다. 말씀하신 대로 수학을 난독화 해제하려면 머리를 크게 써야 하고, 난독화 해제에는 이해가 필요한데 그건 시간이 더 오래 걸립니다. 그래서 새 증명이 나오자마자 교과서가 나오지 않는 겁니다. 소화해서 핵심 부분을 가려내는 데 시간이 걸리니까요.
수학은 언어이고, 언어를 배우려면 시간이 걸립니다. 제가 일본어를 못 읽거나 영어만큼 빨리 읽지 못한다고 해서 일본인이 일부러 자기네 언어를 난해하게 만들었다고 말하는 것과 같습니다.
LLM은 수학에서 형식적 조작에 해당하는 부분을 자동화하고 있습니다. 컴퓨터는 형식적 조작에서 인간보다 훨씬 뛰어납니다. 수학적 계산에서 훨씬 뛰어난 것과 같은 이치죠. 이 분야의 큰 변화는 바로 그것입니다. 하지만 현역 수학자라면 누구나 형식적 조작은 연구의 일부일 뿐이라고 말할 겁니다.
수학의 강력한 점은 형식적 조작 덕분에 인간이 "공짜로" 더 멀리 갈 수 있다는 것입니다. 기초만 이해하면, 형식 체계가 알아서 새로운 결과를 계산해 주기 때문에 그 결과를 다시 이해할 필요가 없습니다.
수학을 어디까지 공부하셨는지 정말 궁금합니다. 너무나 아는 게 없어 보여서요.
확실히 '독특한' 관점이긴 하네요.
아주 후하게 읽어 주자면, 지금 AI의 강점 중 상당수는 (a) 거의 모든 것을 읽었다는 점, (b) 지치거나 지루해하지 않고 수많은 접근법을 기꺼이, 그리고 실제로 시도해 볼 수 있다는 점에서 나오는 것 같다고 말할 수 있습니다. 초인적인 끈기만으로도 따먹을 수 있는 낮은 가지의 열매가 이렇게 많은 이상, 아직은 초인적 지능까지 필요하지 않은 거죠.
독특하지 않습니다. 저는 동의하는데요. 수학이 난해한 건 수학자들이 이해하기 쉬운 것보다 지면에서 간결한 것을 우선하기 때문입니다. 그 결과 헷갈리는 표기법(한 글자짜리 변수 이름, 생략된 곱셈, 생략된 괄호)과 수많은 생략된 단계가 생깁니다.
저는 어떤 수학을 이해하고 싶으면 늘 먼저 코드로 옮깁니다. 요즘 코드(배열 언어는 제외)에는 글자 수를 줄이려는 문화가 더는 없고, "뻔한" 단계를 생략하는 것도 불가능합니다. LLM은 원래 자연어 번역용으로 설계된 아키텍처(트랜스포머)를 기반으로 하니, 이런 일을 잘하는 게 저는 놀랍지 않습니다.
간결한 표기와 생략된 단계는 가독성을 높이려고 있는 겁니다. 저자가 중요하지 않다고 일부러 알려 주는 것에 집중하고 계신 거고, 정작 저자가 말하려는 것(예컨대 변수 이름이나 아주 구체적인 의미가 아니라 식의 "모양")은 놓치고 있을 가능성이 큽니다. Lean의 어려운 점 중 하나는 정말로 말하려는 바가 전달되게 쓰려면 훨씬 많은 노력이 든다는 것입니다.
수학 글쓰기는 기호와 단어일 뿐 아니라 그림이기도 하다고 생각해야 합니다. 눈앞의 것에서 패턴을 보라고 있는 거죠. 그림이 되려면 짧은 이름이 필요합니다. 짧은 이름이 없으면 그림이 보이지 않아요. 개별 픽셀까지 확대해 들여다보는 것과 같습니다. 정보는 전부 거기 있지만 그렇게 해서는 결코 의미를 파악할 수 없습니다. 이름이 짧은 자리표시자로 되어 있는 "축소된" 시야로 읽어야 하는 겁니다.
Lean을 써 보거나 읽어 본 사람이라면 누구나 말해 줄 겁니다. 복잡한 수학 증명을 이해하는 일이 완전히 형식화된다고 해서 꼭 쉬워지는 건 아니라고요.