2024년 여름, AI가 국제 수학 올림피아드(IMO)의 문제를 풀어 은메달 상당의 성적을 거두었습니다. Google DeepMind의 AlphaProof입니다.

이 뉴스에서 간과되기 쉬운 사실이 하나 있습니다 ── AlphaProof가 답안을 작성한 언어는 영어도 중국어도 아닌, Lean 4(린 포)라는 프로그래밍 언어였다는 점입니다.

같은 시기, 수학계에서도 조용한 혁명이 진행되고 있습니다. 핵심이 되는 용어를 하나 먼저 설명하겠습니다. 형식화(Formalization)란, 인간의 언어와 수식으로 쓰인 수학적 증명을 기계가 한 줄씩 검사할 수 있는 프로그래밍 언어 코드로 번역하여 옮겨 적는 것을 말합니다.

수학 세계에서는 지금, 이 형식화가 최전선 연구자들의 도구가 되어가고 있습니다 ── 필즈상 수상자인 Terence Tao는 자신의 최신 연구 성과를 발 빠르게 Lean 4로 형식화했으며, 영국에서는 「페르마의 마지막 정리의 증명을 통째로 형식화하는」 수년이 걸리는 프로젝트가 가동되었습니다.

인류 수학의 도달점을 기계가 검사할 수 있는 형태로 옮겨 적는 ── 그 공통의 무대가 바로 Lean 4입니다.

그리고 2026년 봄에는 일본에서도 큰 뉴스가 전해졌습니다.

교토대학 수리과학연구소의 Mochizuki Shinichi 교수의 우주간 타이히뮤러 이론(IUT 이론) ── 발표 후 10년 이상, 정오를 둘러싸고 세계 수학자들의 의견이 계속 갈려온 거대 이론 ── 을, Lean 4의 형식화를 통해 중립적인 입장에서 검증하는 국제 프로젝트 LANA가, ZEN 대학의 ZEN 수학 센터로부터 발표되었습니다.

이 프로젝트를 이끄는 것은 Kato Fumimoto 교수이며, 멤버로는 후술할 Liquid Tensor Experiment를 주도한 형식화의 일인자들이 이름을 올리고 있습니다. 인간 사이의 논의로는 결론이 나지 않았던 오랜 논쟁에 기계 검사라는 새로운 심판을 세우는 ── 그 심판대에 선택된 것 또한 역시 Lean 4였습니다.

Lean 4란 무엇인가. 왜 수학자와 AI 연구자가 나란히 이 언어로 모여드는가. 그리고 수학자도 AI 연구자도 아닌 일반적인 소프트웨어 엔지니어에게 배울 가치가 있는가.

본 기사는 이 질문에 정면으로 답하는 입문 기사입니다. 사전 지식은 필요하지 않습니다. 프로그래밍은 Python 경험만을 상정하며, 논리학도 대학 수학도 배우지 않았다는 전제하에 모든 전문 용어를 처음 등장하는 곳에서 설명하며 진행합니다.

Lean 4는 수학적 주장을 타입(Type)으로 쓰고, 그 증명을 프로그램으로 쓸 수 있는 언어입니다. 게다가 증명을 뒷받침하는 도구(Tactic)도, 언어의 확장도 모두 Lean 4 스스로 작성할 수 있다는 철저한 자기 기술(Self-describing) 설계를 가지고 있습니다.

이 설계와 Mathlib(매스립)라는 인류 최대 규모의 형식화 수학 라이브러리의 존재가, 수학자의 공동 작업과 AI의 학습·검증 양쪽 모두에 이상적인 토양을 제공했습니다. 수학의 형식화와 AI × 정리 증명(Theorem Proving)의 현재 주전장은 Lean 4입니다 ── 이것이 본 기사의 결론입니다.

여기에 등장하는 용어는 모두 본문에서 설명합니다.

제1부 (기초편) ── 사전 지식 제로 상태에서 다음 4단계로 토대를 만듭니다.

1. 먼저 「정리 증명계(Theorem Prover)」 ── 수학적 증명을 기계가 뒷받침하는 메커니즘 ── 을 3분 만에 파악하기

2. 다음으로, Lean 4라는 언어의 개성(자기 기술)을 알기

3. 그리고 「타입이 주장이 된다」는 사고방식을 하나의 예시로 체험하기

4. 마지막으로, Mathlib ── 수학의 거대한 공유 도서관 ── 알기

제2부 (본편) ── Lean 4의 역사, 실제 구동 체험, 업무 현장(요건부터 증명까지의 4단계와 5가지 사례), 수학자의 5가지 타입, 수학의 최전선, AI 현장, 세계의 흐름과 일본의 현재 위치, 소프트웨어 현장, 타 언어와의 구분 사용 순으로 깊이 있게 다룹니다.

제3부 (응용편) ── 솔직한 질문(Rocq와 Lean 4 중 무엇을 배울 것인가), 「기계가 검증 완료함」을 읽는 리터러시, 학습 리소스, 대화편, 발전 칼럼(접기)으로 이어집니다.

동일한 경로를 한 장의 그림으로 정리해 둡니다.

본 기사는 단독으로 읽을 수 있습니다. 필자는 지금까지 형식 검증(Formal Verification)의 세계를 다른 각도에서 소개해 왔습니다.

λProlog란 무엇인가 ── AI가 수학을 증명하는 시대, 정리 증명계 Rocq의 내부에서 작동하는 알려지지 않은 언어 ── Lean 4와 나란히 하는 주요 정리 증명계 Rocq의 내부 언어 이야기입니다

F*(F Star)란 무엇인가 ── 검증된 코드가 그대로 제품에서 작동하는, 또 다른 방식입니다

• 형식 증명은 「사양이 인간의 의도를 반영하고 있는가」를 보장하지 않는다 ── 본 기사의 대화편에 등장하는 두 편의 기초 기사입니다

• 지금까지 Python만을 사용해 온 엔지니어

• AlphaProof나 「AI가 수학 올림피아드에서 은메달을 획득」했다는 뉴스의 배경을 알고 싶은 분

• 정리 증명계 (Theorem Prover; Lean 4, Rocq, Isabelle, Agda 등)를 배운 적이 없는 분

• 수학을 좋아했지만, 대학 수학이나 논리학은 배우지 않은 분

• Lean과 Lean 4의 차이, Rocq (구 Coq)와의 차이가 궁금한 분

• AI와 수학·형식 검증 (Formal Verification)의 접점에 관심이 있는 분

• Lean 4란 무엇인지, 왜 지금 수학자와 AI 연구자들의 주전장인지 알 수 있게 된다

• 「타입 (Type)이 주장 (Claim)이 되고, 프로그램이 증명 (Proof)이 된다」는 발상을 실제로 동작하는 코드로 체험할 수 있게 된다

• Mathlib이라는 인류 최대 규모의 수학 라이브러리의 규모와 구조를 파악할 수 있게 된다

• 테렌스 타오 (Terence Tao)의 형식화나 페르마의 마지막 정리 프로젝트 등, 수학 현장의 최전선을 알 수 있게 된다

• AlphaProof나 DeepSeek-Prover 등, AI × 정리 증명의 조류 속에서 Lean 4의 위치를 알 수 있게 된다

• Rocq, Isabelle, Agda, F*와의 차이점 및 용도 구분 기준을 얻을 수 있다

• AI나 타인이 작성한 「Lean으로 검증 완료된」 성과물을 받았을 때 확인해야 할 3가지 검토 지점 (sorry, 공리 (Axiom), 주장문 (Statement))을 익힐 수 있다

• 코드의 어느 부분이 자유롭게 붙인 이름이고, 어느 부분이 Lean 4의 규칙인지 구분할 수 있게 되어, 처음 보는 코드라도 골격을 읽을 수 있게 된다

• 언어의 장단점이 토대가 되는 논리·공리계와 타입 시스템에 의해 어떻게 결정되는지, 16개 언어의 비교와 「Lean 4가 원리적으로 할 수 없는 것」에 대한 해명까지 포함하여 통찰할 수 있다

(이 절의 전문 용어는 모두 본문에서 설명하겠습니다)

• Lean 4는 정리 증명계인 동시에 범용 프로그래밍 언어이기도 하다. 두 가지가 하나의 언어에 통합되어 있다

• 가장 큰 개성은 자기 기술 (Self-description) ── Lean 4의 컴파일러도, 증명 도구도, 언어 확장도 Lean 4 자체로 작성되어 있다

• Mathlib은 수백 명의 기여자가 육성하는 형식화 수학의 거대 라이브러리로, 수학의 공동 사업으로서뿐만 아니라 AI의 학습과 검증의 토대로서도 기능하고 있다

• 실무에서의 사용법은 4단계 ── 업무 요구사항을 언어화하고, 적합해 보이는 수학적 구조를 교양과 LLM의 지원을 통해 좁히고, 가설을 Lean 4의 타입으로 작성하며, 기계가 증명 또는 반증한다

• 타입을 선택하는 것은 연산의 의미를 선택하는 것이다 (Nat의 뺄셈은 0에서 멈춘다). 본 기사에서 사용하는 택틱 (Tactic)은 10개뿐이며, 응용편에 목록을 부록으로 두었다

• 수학 현장에서는 테렌스 타오의 연구 형식화나 페르마의 마지막 정리 형식화 프로젝트가 Lean 4로 진행 중이다

• AI 현장에서는 AlphaProof (IMO 은메달 수준)를 비롯하여, 증명 AI의 상당수가 Lean 4를 답안지로 채택하고 있다. 2025년에는 자연어로 문제를 푸는 AI가 IMO 금메달 수준에 도달했으나, 인간 채점자를 필요로 하는 자연어 답안과 커널 (Kernel)이 검사하는 형식화된 답안은 별개다 ── AI가 증명을 양산하는 시대일수록, 기계가 채점할 수 있는 답안지의 가치는 올라간다

• 「Lean으로 검증 완료된」 성과물을 받았다면, sorry의 개수를 세고, 공리를 세고, 주장문을 읽어라 ── 커널의 보증은 주장문 직전에서 멈추며, 주장문의 검토는 인간의 업무로 남는다

• 소프트웨어 검증의 전통적 자산에서는 Rocq에, 제품으로의 직결에서는 F*에 강점이 있어 목적에 따라 나누어 사용한다. 수학의 형식화와 AI의 조류를 탄다면 입문으로는 Lean 4가 제1순위 후보이다

• 언어의 장단점은 토대가 되는 논리·공리계와 타입 시스템에 의해 원리적으로 결정된다 ── 예를 들어 Lean 4는 증명 상호 간을 구별하지 않는 설계 덕분에 가볍고 빠르지만, 여러 개의 동일성을 다루는 수학 (HoTT)은 원리적으로 할 수 없으며, 그 영역은 Cubical Agda 등이 담당한다

• Lean 4와 Mathlib 모두 무료 오픈 소스 (Apache License 2.0)이다. 일본어 커뮤니티 lean-ja가 교과서 번역과 스터디를 진행하고 있어 일본어만으로도 학습을 시작할 수 있다

• Lean 공식 사이트 ── https://lean-lang.org/

• 공식 북 (Official Books)
  "Theorem Proving in Lean 4", "Functional Programming in Lean", "Mathematics in Lean" (모두 공식 사이트에서 무료로 읽을 수 있습니다)

• Lean 4 GitHub 리포지토리 ── https://github.com/leanprover/lean4

• Mathlib GitHub 리포지토리 ── https://github.com/leanprover-community/mathlib4

• 브라우저 실행 환경 Lean 4 Web ── https://live.lean-lang.org/

정리증명계 (Theorem Prover)란, 수학적 증명을 컴퓨터 상에 작성하고 그 정당성을 기계가 검사하도록 하는 소프트웨어입니다.

증명이란, 어떤 주장이 옳다는 것을 미리 인정된 추론 규칙만을 사용하여 한 단계씩 보여주는 경로를 의미했습니다. 인간이 종이 위에 쓰는 증명에는 행간의 비약이나 짐작이 섞여 들어갈 수 있습니다. 정리증명계 위에서 작성하는 증명은 한 걸음 한 걸음이 모두 기계에 의해 검사되기 때문에, 검사를 통과한 주장에는 비약도 속임수도 남아 있지 않습니다.

그리고 검사를 담당하는 파수꾼은 커널 (Kernel)이라 불리는 작은 핵심 부품입니다. 아무리 방대한 증명이라도 마지막에는 반드시 커널의 검사를 통과해야만 정리 (Theorem)로 인정받습니다. 이 "작은 파수꾼이 모든 것을 최종 검사한다"는 태도는 Lean 4에서도, 자매 기사에서 소개한 Rocq에서도 공통된 설계입니다.

Lean (린)은 Microsoft Research의 연구원 레오나르도 데 모우라 (Leonardo de Moura)가 2013년에 개발하기 시작한 정리증명계입니다. 버전을 거듭하며 성장하여, 2023년에 정식 출시된 현행 버전이 Lean 4입니다.

현재는 개발을 전문으로 담당하는 비영리 조직인 Lean FRO가 중심이 되어 개발을 주도하고 있습니다.

Lean 4의 가장 큰 개성은 철저한 자기 기술 (Self-description)에 있습니다. Lean 4의 컴파일러는 Lean 4로 작성되어 있습니다. 증명을 진행하는 도구 (택틱 (Tactic); 후술하겠습니다)도 Lean 4로 작성합니다. 언어의 문법을 확장하는 메커니즘도 Lean 4 안에 있습니다. 즉, Lean 4를 배우면 그 언어를 개조하는 언어까지 동시에 손에 넣게 되는 것입니다.

이 점은 자매 기사의 $\lambda$Prolog 이야기와 대조적입니다.

Rocq는 "메타프로그래밍 (프로그램을 조작하는 프로그램을 작성하는 것)을 위해서는 그 전용으로 강력한 $\lambda$Prolog를 손님으로 맞이한다"라는 설계를 택했고, Lean 4는 "자신의 일은 전부 스스로 작성한다"라는 설계를 택했습니다.

같은 과제에 대한 두 가지 설계 해법입니다.

또 하나, 놓칠 수 없는 개성이 있습니다. Lean 4는 정리증명계인 동시에, 아주 평범하게 사용할 수 있는 범용 프로그래밍 언어이기도 하다는 점입니다. 웹 서버도, 커맨드라인 도구도 작성할 수 있습니다.

"수학적 증명"과 "일상적인 프로그래밍"이 별개의 도구가 아니라 하나의 언어가 가진 두 가지 얼굴이 되어 있다 ── 이것이 Lean 4 설계 사상의 핵심입니다.

Python의 타입 힌트 (Type hint) int는 "이 변수에는 정수 중 하나가 들어간다"는 것밖에 말할 수 없습니다. Lean 4의 타입 (Type)은 훨씬 더 많은 것을 말할 수 있습니다. "모든 자연수 $n$에 대하여 $n + 0 = n$이 성립한다"라는 수학적 주장 그 자체를 타입으로 작성할 수 있습니다.

theorem add_zero' (n : Nat) : n + 0 = n := rfl

읽는 법은 다음과 같습니다. theorem은 정리의 선언. add_zero'는 직접 붙인 이름.

콜론 오른쪽의 (n : Nat) : n + 0 = n이 타입이며, 동시에 증명하고 싶은 주장입니다 (Nat는 자연수, 즉 0 이상의 정수 타입).

그리고 := rfl이 증명의 본체 ── rfl은 reflexivity (반사성; 같은 것은 같다)의 약자로, "좌변과 우변은 정의대로 계산하면 같습니다"라는 가장 짧은 증명입니다.

Lean 4 코드를 처음 접하시는 분들을 위해, 이 첫 한 줄을 교재 삼아 읽는 법의 기초를 하나만 익혀둡시다.

코드에 나타나는 단어는 예약어 (Reserved word), 라이브러리 이름 (Library name), 프로그래머가 임의로 붙인 이름 중 하나입니다.

이 세 가지 구분을 할 수 있게 되면, 처음 보는 코드라도 골격을 따라갈 수 있게 됩니다.

• 예약어와 기호: 이 줄에서는 theorem, 괄호, :, **:=**가 해당합니다. 이는 Lean 4의 문법에 의해 정해진 표기법이므로, 한 글자라도 바꾸면 에러가 발생합니다. Python의 def나 return에 해당합니다.

• 라이브러리 이름: 이 줄에서는 **Nat**와 **rfl**이 해당합니다. 거슬러 올라가면 Lean 4의 개발자들이 과거에 임의로 붙였던 이름이 지금은 라이브러리에 등록되어 있는, 그런 유래를 가진 단어들입니다.

Lean 4 코드를 작성할 때는 정식 라이브러리 이름을 단 한 글자라도 잘못 입력하면, "그런 이름은 알 수 없습니다"라는 에러가 발생합니다.

• 프로그래머가 임의로 이름을 붙일 수 있는 부분: 이 행에서는
  **add_zero'**와 n이 이에 해당합니다.

프로그래머가 그 자리에서 결정한 이름이므로, taro나 my_first_theorem이어도 상관없습니다.

끝에 붙은 ' (아포스트로피) 또한 이름에 사용할 수 있는 일반적인 문자로, 여기서는 Mathlib를 불러온 환경에 존재하는 add_zero라는 라이브러리 이름과 충돌하지 않도록 미리 붙여둔 것입니다.

한 가지 유념해 두셔야 할 점이 있습니다.

프로그래머가 임의로 붙인 이름은 머지않아 라이브러리 이름과 같은 지위를 갖게 됩니다.

add_zero' 역시 이름을 붙이는 순간 이 파일 안에서는 등록된 이름이 되며, 이후에는 정확한 철자로 불러야만 합니다.

요컨대, 언어 설계자가 정한 단어인가, 작성자 스스로가 정한 단어인가

── 두자의 차이는 그것뿐입니다.

누가 이름을 붙였든 간에, 일단 이름이 붙은 후에는 단 한 글자의 오차도 허용되지 않습니다.

본 기사에서는 코드를 제시할 때마다 어떤 단어가 예약어(Reserved word)이고, 어떤 것이 라이브러리 이름이며, 어떤 것이 프로그래머가 붙인 이름인지 짧게 덧붙이도록 하겠습니다.

덧붙여, 주장을 타입(Type)으로 쓰고, 그 타입을 가진 값(프로그램)을 만드는 것이 증명이 된다.

이 대응 관계에는 **커리-하워드 대응 (Curry-Howard Correspondence)**이라는 이름이 붙어 있습니다.

자세한 내용은 아래의 기사를 참조해 주세요.

Lean 4를 이야기할 때, 언어 본체만큼이나 중요한 존재가 **Mathlib (매스립)**입니다.

Mathlib는 전 세계의 수학자와 엔지니어가 공동으로 키워나가고 있는 형식화된 수학의 거대 라이브러리입니다.

고교 수학부터 대학원 수준의 현대 수학까지, 수십만 건의 정리와 정의가 백십만 행이 넘는 규모로 기계 검증이 완료된 형태로 수록되어 있습니다.

기여자(Contributor)는 수백 명에 달하며, 지금도 매일 성장하고 있습니다.

예를 들어 "(a + b)의 제곱 전개"와 같은 교과서적인 정리는 모두 수록되어 있습니다.

Mathlib를 불러오면 다음과 같이 코드를 작성할 수 있게 됩니다.

import Mathlib
example (a b : ℝ) : (a + b)^2 = a^2 + 2*a*b + b^2 := by ring

ring (링)은 "환 (Ring, 덧셈과 곱셈의 세계)의 등식을 자동으로 처리해 줘"라는 태크틱 (Tactic)으로, 전개와 정리 모두 기계가 수행합니다.

이 코드 안에서는 import가 예약어, Mathlib (도서관 전체의 이름)와 ℝ (실수의 타입. Mathlib가 정한 기호이며, Real이라고 써도 동일함)과 ring (태크틱)이 라이브러리 이름이며, a와 b가 프로그래머가 붙인 이름입니다.

수학자들이 Mathlib에 모이는 이유도, AI가 Lean 4를 답안지로 선택하는 이유도, 궁극적으로는 이 도서관의 존재로 귀결됩니다 ── 거인의 어깨가 기계 검증이 완료된 형태로 공개되어 있기 때문입니다.

Lean의 발자취를 빠르게 따라가 보겠습니다.

• 2013년 ── Microsoft Research의 Leonardo de Moura가 Lean 개발을 시작. de Moura는 F*의 파트너로서 자매 기사에도 등장했던 SMT 솔버 Z3의 제작자이기도 합니다.

• 2017년 ── Lean 3가 공개되어 수학자 커뮤니티에 의한 라이브러리 mathlib의 성장이 시작됩니다.

• 2021~2023년 ── 언어를 근본부터 다시 작성한 Lean 4가 단계적으로 공개되어 2023년에 정식 출시되었습니다. mathlib도 전면 이식되어 현재의 Mathlib (Lean 4 버전)가 됩니다.

• 2023년 ── 개발을 전문으로 담당하는 비영리 연구 조직 Lean FRO가 발족. Microsoft의 한 연구 프로젝트에서 독립된 기반을 가진 커뮤니티 언어로 발걸음을 내딛습니다.

웹상에는 Lean 3 시대의 해설 기사가 많이 남아 있습니다.

Lean 3와 Lean 4는 문법도 라이브러리도 크게 다르기 때문에, Lean을 이제부터 배우려는 분들은 "Lean 4"라고 명시된 자료를 선택해 주세요 (본 기사의 코드는 모두 Lean 4입니다).

참고로 Lean 4 본체와 Mathlib 모두 오픈 소스 (Apache License 2.0)이며, 무료로 상업적 이용이 가능합니다.

공식 브라우저 실행 환경인 Lean 4 Web(https://live.lean-lang.org/)을 열면, 계정 등록이나 설치 없이 지금 바로 Lean 4를 실행할 수 있습니다.

그럼, 우선 가볍게 몸풀기부터 해봅시다.

#eval 2 + 2 -- 4라고 표시됨
#eval "こんにちは、" ++ "Lean 4"
def double (x : Nat) : Nat := 2 * x
...

#eval은 "계산해서 보여줘"라는 명령이고, def는 함수 정의입니다. 여기까지는 일반적인 프로그래밍 언어와 같은 모습입니다.

내역 ── 자유로운 이름: double과 x. 언어의 규칙: #eval, def, :=, 주석 기호 --. 등록된 이름: Nat와 문자열 연결 ++ (연산자도 등록된 이름의 일종입니다).

일반적인 언어라고 생각하고 다루다 보면, 가장 먼저 놀라게 되는 부분이 바로 이것입니다.

#eval (5 - 10 : Nat) -- 0
#eval (5 - 10 : Int) -- -5

**$Nat$ (자연수)**는 **$0$ 이상의 수의 타입 (Type)**이므로, 결과가 음수가 되는 뺄셈은 $0$에서 멈춘다고 정의되어 있습니다.

이것은 버그가 아니라, 타입 정의 그 자체의 동작입니다.

여기에 중요한 교훈이 하나 있습니다 ── 타입을 선택한다는 것은 연산의 의미를 선택한다는 것입니다.

나중에 이어질 「업무 현장」 절에서 금액 계산에 Int (정수)를 사용하는 이유는 바로 이 함정을 피하기 위해서입니다.

참고로, (5 - 10 : Nat) 부분에서 "이 식을 Nat로 읽어라"라는 타입 지정(Type Annotation)을 하고 있습니다. 이 :의 사용법 또한 예약어 및 기호의 일종입니다. Int (정수 타입)는 라이브러리 이름입니다.

example : 2 + 2 = 4 := rfl -- 통과
example : 2 + 2 = 5 := rfl -- 빨간색 에러

example은 "이름을 붙이지 않은 정리 (Theorem)"의 선언입니다. 첫 번째 줄은 조용히 수락되지만, 두 번째 줄은 거부됩니다. 이러한 가차 없음이 정리 증명계 (Theorem Prover)의 힘의 원천입니다.

내역 ── example은 언어의 규칙이며, 이름을 붙이지 않기 때문에 종류 3(자유로운 이름)이 등장하지 않는 선언입니다.

한편, Lean 4와 어깨를 나란히 하는 대표적인 정리 증명계로 Rocq (록. 구 명칭 Coq (콕))가 있습니다.

"$x + 0 = x$"를 Rocq에서 증명하려고 하면, rfl만으로는 끝나지 않고 귀납법 (Induction)이 필요합니다.

그 이유는 덧셈이라는 함수의 정의 방식에 있습니다.

Lean 4의 덧셈은 "오른쪽 숫자를 하나씩 깎아 나가는" 형태로 정의되어 있습니다.

$x + 0$의 경우, 오른쪽이 $0$이므로 "깎아낼 것이 아무것도 없다. 답은 $x$이다"라고, 정의를 읽는 것만으로 즉시 결정됩니다. 그래서 rfl 한 마디로 통과하는 것입니다.

Rocq의 표준 덧셈은 이와 반대로 "왼쪽 숫자를 하나씩 깎아 나가는" 형태로 정의되어 있습니다.

$x + 0$의 왼쪽은 $x$, 즉 내용을 알 수 없는 변수이므로, 정의만으로는 한 발짝도 계산이 진행되지 않습니다.

$x$가 $0$인 경우, $1$인 경우, $2$인 경우... 와 같이 모든 경우에 성립함을 귀납법으로 보여줄 수밖에 없습니다.

즉, 이 차이는 언어의 우열 문제가 아닙니다.

덧셈을 어느 쪽 인자 (Argument)로 정의했느냐라는 언어 설계의 차이가, 그대로 증명의 수고로움의 차이로 나타나고 있는 것입니다.

같은 정리라도 언어가 다르면 보이는 풍경이 다르다 ── 그 첫 번째 사례입니다.

Lean 4에서는 다음과 같이, rfl 한 마디만 적으면 충분합니다.

theorem add_zero' (n : Nat) : n + 0 = n := rfl -- 한 마디로 끝남
theorem zero_add' (n : Nat) : 0 + n = n := by -- 이쪽은 한 마디로 끝나지 않음
induction n with
...

비밀을 밝히자면, Lean 4의 덧셈은 "오른쪽 인자를 분해하여 계산하도록" 정의되어 있기 때문에, $n + 0$은 정의대로 계산하기만 하면 $n$이 됩니다 (그래서 rfl).

하지만 좌우를 바꾼 $0 + n = n$은 정의만으로는 진행되지 않으며, 귀납법 ── "$0$인 경우를 보이고, $k$에서 성립한다면 $k + 1$에서도 성립함을 보이는" 증명 방식 ── 이 필요합니다.

두 번째 증명을 해독해 보겠습니다.

by는 "여기서부터 택틱(tactic)으로 증명하겠습니다"라는 의미의 신호입니다.

**택틱 (tactic)**이란, 증명의 중간 과정(골, goal)을 한 수씩 변형해 나가는 지시를 말합니다.

induction n with는 "$n$에 대하여 귀납법으로 경우를 나누라"는 지시입니다.

zero의 경우는 rfl,

succ($k$의 다음 수)의 경우는, **rw (rewrite, 재작성)**로 식을 정리한 후, 귀납법의 가정인 ih를 사용하여 마무리

── 마치 장기의 한 수와 같은 지시의 축적으로 증명이 완성되어 갑니다.

참고로, 본 기사에 등장하는 택틱은 총 10개입니다.

이 기사의 「응용편」 끝부분에 복습용 일람표를 부록으로 마련해 두었습니다.

여기서는 택틱을 외우려 하지 말고, 분위기만 파악한 채 다음으로 넘어가시기 바랍니다.

이 코드에서 프로그래머가 직접 원하는 이름을 붙인 부분은 zero_add', n, k, 그리고 ih입니다.

ih는 **induction hypothesis (귀납법의 가정)**의 앞 글자를 딴 이름으로, Lean 4 프로그래머들이 관습적으로 이렇게 명명하지만, 이름 자체는 자유롭게 정할 수 있으므로 kasetsu라고 써도 통합니다.

by, induction, with, |, =>는 예약어(reserved word)와 기호입니다.

rfl과 rw는 택틱의 이름입니다.

Nat.add_succ는 "$n + (m + 1) = (n + m) + 1$"이라는 보조정리(lemma)에 라이브러리 개발자가 붙인 이름으로, 모두 라이브러리 이름입니다.

주의가 필요한 부분은 zero와 succ입니다.

이 두 가지는 언뜻 보면 직접 선택할 수 있는 이름처럼 보이지만, 그렇지 않습니다.

$Nat$라는 타입 (type) 자체가 "zero와 succ라는 두 가지 방식으로 만들어진다"라고 정의되어 있기 때문에, 경우 나누기의 가지에는 그 정의에 따른 철자를 그대로 써야 합니다.

이 부분을 jiro 등으로 바꾸면 에러가 발생합니다.

위의 귀납법 증명을 Lean 4 Web에 붙여넣으면, 에디터 오른쪽(Infoview라고 불리는 영역)에 지금 증명해야 할 남은 주장 ── 골(goal)이라고 부릅니다 ── 가 표시됩니다.

커서를 한 줄씩 움직이면, 택틱을 한 수 둘 때마다 골이 변형되어 가는 모습을 관찰할 수 있습니다.

succ의 가지를 실황하면 다음과 같습니다.

induction n with 직후:
ih : 0 + k = k ← 귀납법의 가정 (사용 가능한 기지의 사실)
⊢ 0 + (k + 1) = k + 1 ← 지금 보여야 할 골 (⊢의 오른쪽)
...

한 수를 둘 때마다 판(골)이 바뀐다 ── 이것이 대화형 정리 증명계(interactive theorem prover)의 "대화"의 정체입니다. 증명을 쓴다는 것은 문장을 단번에 써 내려가는 것이 아니라, 기계와 판을 사이에 두고 한 수씩 두어 나가는 것입니다.

또 하나, 초보자의 강력한 아군을 소개합니다.

sorry입니다.

theorem zero_add'' (n : Nat) : 0 + n = n := by
sorry -- "이 부분은 나중에 채우겠습니다"라는 보류 선언

sorry는 "이 부분의 증명은 보류"라는 공식적인 선언이며, Lean은 경고를 띄우면서도 일단 이를 받아들여 줍니다.

거대한 증명에 도전할 때는 먼저 전체를 sorry로 뼈대를 잡아두고, 한 곳씩 진짜 증명으로 교체해 나간다 ── 이것이 정석적인 진행 방식입니다.

단, sorry가 하나라도 남아 있는 정리는 당연하게도 증명 완료라고 부를 수 없습니다.

이 점은 응용편에서 다시 한번 다루겠습니다.

sorry는 Lean 4 언어에 정의된 예약어입니다.

**zero_add''**는 프로그래머가 임의로 붙일 수 있는 이름을 기술한 부분입니다.

위의 샘플 코드에서는 이미 정의된 zero_add'와 이름이 충돌하지 않도록 '를 하나 더 붙여 다른 이름으로 만들었습니다. 여기에는 완전히 다른 이름을 붙여도 아무런 상관이 없습니다.

뼈대 이야기는 여기까지 하고, 이 절에서 증명한 두 식을 다시 나열해 보겠습니다.

rfl 한 마디로 끝난 "$n + 0 = n$"과, 귀납법까지 필요했던 "$0 + n = n$"입니다.

수학적으로는 둘 다 "자명"해 보이는 두 식이, 기계의 입장에서는 난이도가 다른 별개의 문제가 됩니다.

여기에 「정의대로 계산할 수 있는 것」과 「증명이 필요한 것」의 경계선이 나타나 있습니다.

이 감각을 잡았다면, 당신은 이미 정리 증명계 (Theorem Proving System)의 입구에 서 있는 것입니다.

Mathlib에 수십만 개의 정리가 있더라도, 원하는 하나를 찾아내지 못한다면 보물도 쓸모가 없게 됩니다.

Lean 4에는 이를 해결하는 메커니즘이 언어 측면에 갖춰져 있습니다.

바로 exact?라는 택틱 (tactic) 입니다.

import Mathlib
example (a b : Nat) : a + b = b + a := by
exact? -- 이 골 (goal)을 닫을 수 있는 정리를 Mathlib에서 탐색

실행하면 Lean은 라이브러리를 검색하여, "exact Nat.add_comm a b로 닫을 수 있습니다"라고 제안합니다 (**Nat.add_comm**은 덧셈의 교환 법칙 정리에 대한 이름입니다).

본래라면 인간이 먼저 라이브러리 중에서 사용할 만한 정리를 찾아내고, 그 이름을 사용하여 증명을 작성합니다.

exact?를 사용하면 이 순서가 반대가 됩니다.

인간은 증명하고 싶은 주장만을 작성하고, 이에 맞는 기존 정리가 Mathlib에 존재하는가?

Mathlib에 존재한다면 어떤 정리인지, 기계 (Lean 4)가 찾아오는 것입니다.

exact?는 택틱 (tactic)의 이름입니다.