【2026년판】Lean 4 및 형식 증명 입문 추천! 전 26개 기사를 무료 Book으로 정리했습니다

중학생도 이해하는 Lean 4: 아주 쉬운 형식 증명 입문서

Lean 4(리안 4)와 형식 증명을 배우고 싶은 분들을 위해 추천할 만한 무료 입문서가 완성되었습니다. 수학적 증명, 정리 증명 지원계(proof assistant), 형식 검증(formal verification), 그리고 생성형 AI의 답변을 신뢰하는 방법론까지 다룹니다. 중학생도 이해할 수 있는 쉬운 시작점부터 대학생 및 사회인, AI 연구/개발 현장에서 중요하게 다뤄지는 논점들로 이어지는 책입니다.

"수학적 증명이란 정확히 무엇을 확인하고 있는 걸까?"
"생성형 AI가 '증명했습니다'라고 말한다면, 어디까지 믿어야 할까?"

이러한 의문에서 시작된 『중학생도 이해하는 Lean 4』 연재 시리즈가 #00부터 #25까지 총 26개 기사를 거치며 한 단계를 마쳤습니다.

이에 따라 이번에 연재 내용을 책 한 권처럼 순차적으로 읽을 수 있도록 재편집하여, **무료 Zenn Book 『중학생도 이해하는 Lean 4――아주 쉬운 형식 증명 입문』**으로 정리했습니다.

무료 북은 여기에서 확인하세요: 『중학생도 이해하는 Lean 4――아주 쉬운 형식 증명 입문』 읽기

Lean 4란 무엇인가?

Lean 4는 **대화형 정리 증명 지원계(interactive theorem prover)**인 동시에 함수형 프로그래밍 언어이기도 합니다. 수학적 명제나 프로그램에 대해, 형식적으로 작성된 주장과 그 증명을 검사하는 데 사용됩니다. 공식 용어로는 theorem proving, formal proofs, formal verification 등이 등장하며, 한국어로는 '정리 증명', '형식 증명', '형식 검증', '증명 지원계' 등의 용어가 있습니다.

• Lean 공식 웹사이트 — Lean 개요 및 활용 사례
• Lean Language Reference — 종속형 이론(dependent type theory), 커널(kernel), 언어 사양의 공식 레퍼런스
• Theorem Proving in Lean 4 — Jeremy Avigad, Leonardo de Moura, Soonho Kong, Sebastian Ullrich 등이 작성한 증명 학습 교재
• Lean JA (Lean 언어 일본어 커뮤니티) — 한국어로 '증명 지원계', '수학적 증명의 검증' 등을 해설하는 자료
• Mathematics in Lean — Lean과 mathlib을 사용해 수학을 형식화하는 법을 배우는 교재

이 자료들은 Lean 자체를 이해하기 위한 1차 자료 및 학습 자료입니다. 본서는 이러한 공식성을 빌린 것이 아니라, 전문적인 교재에 들어가기 전에 '무엇이 증명되었는지' 읽어보는 한국어 입문점으로 위치하고 있습니다.

예를 들어, "어떤 자연수 n에 대해서도 n + 0 = n이 성립한다"라는 주장을 Lean이 검사할 수 있는 형태로 작성할 수 있습니다.

example (n : Nat) : n + 0 = n := by
simp

여기서 중요한 것은, Lean이 확인하는 것은 실제로 작성된 명제와 증명 그 자체라는 점입니다. 이름이 아무리 거창하고 설명문이 설득력이 넘치더라도, 거기서부터 증명의 의미가 마음대로 확장되는 것은 아닙니다.

'형식 증명'과 '형식 검증'은 어려워 보이나요?

물론 전문적인 연구나 소프트웨어 검증에는 깊은 수학적 지식과 컴퓨터 과학 지식이 필요할 때가 있습니다.

하지만 입문점은 훨씬 더 가까운 곳에 있습니다.

• "절대적으로 옳다"는 주장에 반례를 하나 찾아낸다면 어떨까요?
• '정의했다'와 '증명했다'는 같은 의미일까요?
• 프로그램 테스트가 통과되었다고 해서 모든 입력값에서 올바른 결과를 보장할 수 있을까요?
• AI가 만든 Lean 코드가 통과되었다고 해서 현실 세계의 주장이까지 맞는 걸까요?

본서에서는 이러한 질문들을 일반적인 한국어와 작은 예시들로부터 생각하며, 조금씩 Lean 4 코드 쪽으로 나아갑니다. 어려운 이야기를 지우는 것이 아니라, 그곳에 도달하는 계단을 늘리는 방식을 취하고 있습니다.

26개 기사에서 한 권의 무료 북으로

연재 시리즈에서는 독자들이 특정 기사만 읽고 와도 이해할 수 있도록 이전 내용 요약이나 기사 간 링크를 넣어 구성했습니다.

하지만 Book은 처음부터 순서대로 읽는 것을 전제로 하여 장의 흐름을 정리했습니다. 총 26개 기사에 대응하는 내용을 포함하여, 체크 카드와 용어집, 그리고 다음 학습 가이드까지 준비했습니다.

전체적인 학습 경로는 다음과 같습니다.

• 증명과 논변: 논파(refutation), 반례(counterexample), '옳다'는 의미를 생각하기
• Lean 4의 입문: 명제(proposition), 정의(definition), 형식 증명, 커널(kernel)을 통한 검사 이해하기
• 증명의 한계: 이름이나 설명, 면책 조항으로 증명의 범위가 확장되지 않음을 배우기
• 수학과 현실: 모델에 작성된 내용과 실제로 말하고 싶은 것을 구분하기
• 생성형 AI와 검증: AI가 만든 후보를 읽고, 의심하며, 감사(audit)하고, 재현성을 생각하기
• 일상으로 돌아가기: 의견과 사람, 실수와 패배, 모르는 상태를 구별하기

단순히 Lean 4의 문법집이 아닙니다. '증명되었다'는 말을 스스로 확인할 수 있게 되는 입문서입니다.

중학생부터 대학생, 직장인, AI 연구·개발 현장까지

본서는 독자의 연령이나 직업을 한정하지 않습니다. 중학생·고등학생에게는 수학 증명이나 논리의 입문으로, 대학생에게는 명제·정의·형식화의 기초로, 직장인이나 엔지니어에게는 사양(仕様)·테스트·증명의 차이를 생각하는 계기로 추천합니다.

AI 연구·AI 개발에 관련된 사람들에게는 AI가 작성한 증명 후보와 Lean이 실제로 검사한 내용을 나누어 읽는 시점을. 생성형 AI를 일상적으로 사용하는 사람들에게는 AI 리터러시—그럴듯한 답변을 근거와 확인 범위로 나누어 생각하는 힘을 기르는 입구를 마련했습니다.

다루는 주제의 폭이 넓은 것과, 이것 한 권으로 전문적인 실무 능력이 완성되는 것은 별개입니다. 우선 '무엇이 확실하게 증명되었고, 무엇은 아직 증명되지 않았는지'를 읽는 능력부터 시작합니다.

이런 사람에게 추천하고 싶습니다

수학을 잘하지 못해도, 프로그래밍 경험이 없어도 괜찮습니다. 중학교에서 배운 정도의 일본어와 수학부터 순서대로 생각할 수 있도록 작성했습니다.

물론, 생성형 AI를 업무나 학습에 사용하는 사람, 프로그램의 품질이나 형식 검증에 관심 있는 엔지니어에게도 다른 입구로 읽어주시면 좋겠습니다.

다만, 본서를 읽는 것만으로 실무의 형식 검증이 가능해진다고 보장하는 것은 아닙니다. 실제로 개발 환경을 만들고 코드를 작성하고 빌드하고 재현하는 실습적인 학습은 별도의 단계입니다.

무료로 볼 수 있습니다

『중학생도 아는 Lean 4—아주 쉬운 형식 증명 입문』

가격은 무료입니다. 공개 후에는 연재를 따라가지 못했던 분들도 Book의 처음부터 쭉 읽을 수 있습니다.

우선 '증명이 애초에 무엇인지?'라는 부분부터요. Lean 4나 형식 증명이라는 단어가 궁금한 사람들에게 첫걸음으로 전해드리면 좋겠습니다.

연재 총 26개 기사 목록

Book으로 쭉 읽기 전에, 관심 있는 주제만 보고 싶은 분들은 여기서 확인하세요. 각 기사는 단독으로도 읽을 수 있습니다.

• #00｜'증명되었다'는 어디까지 진실일까?
• #01｜논파하면 맞는 걸까?
• #02｜당신은 이미 증명을 하고 있다
• #03｜반례—'절대'를 하나의 예로 부수기
• #04｜첫 형식 증명
• #05｜일본어를 Lean의 언어로 번역하기
• #06｜Lean은 어떻게 증명을 확인할까?
• #07｜'정의했다'와 '증명했다'는 다르다
• #08｜이름을 강력하게 하면 정리도 강해질까?
• #09｜동어반복(トートロジー)을 '대발견'처럼 보여주기
• #10｜AI는 '증명의 내용'과 '강해 보이는 이름'을 나누어 읽을 수 있을까?
• #11｜면책 조항을 쓰면 무슨 말을 해도 괜찮을까?
• #12｜Lean으로 증명했다. 하지만, 무엇이 증명된 걸까?
• #13｜수학으로 하면 맞게 될까?
• #14｜틀린 문제를 완벽하게 증명하기
• #15｜AI+수학+Lean이면 만능일까?
• #16｜AI가 작성하고, Lean이 검사한다
• #17｜AI의 증명을 부숴보자
• #18｜스스로 작은 정리를 만들어 보자
• #19｜나의 증명을 감사(AUDIT)하자
• #20｜남이 재현할 수 있는 형태로 만들자
• #21｜'모른다'는 나쁜 답이 아니다
• #22｜틀리는 것과 지는 것을 구분하기
• #23｜사람과 의견을 구분하기
• #24｜논파에서 검증으로
• #25｜AI 시대의 '확인 방법'

토론(Discussion)