1. 소개

1.1. 시작하기

이 책의 목표는 Lean 4 대화형 증명 보조기를 사용하여 수학을 형식화하는 방법을 가르치는 것입니다. 이 책은 독자가 어느 정도 수학을 안다고 가정하지만, 많은 지식을 요구하지는 않습니다. 정수론에서 측도론과 해석학에 이르기까지 다양한 예제를 다루겠지만, 해당 분야가 익숙하지 않더라도 진행하면서 자연스럽게 익힐 수 있도록 각 분야의 기초적인 측면에 초점을 맞출 것입니다. 또한 형식 기법에 대한 배경지식도 전제하지 않습니다. 형식화는 일종의 컴퓨터 프로그래밍으로 볼 수 있습니다. 우리는 수학적 정의, 정리, 증명을 프로그래밍 언어처럼 엄격하게 규정된 언어, 즉 Lean이 이해할 수 있는 언어로 작성할 것입니다. 그 대가로 Lean은 피드백과 정보를 제공하고, 표현식을 해석하여 그것이 올바른 형태임을 보장하며, 궁극적으로 우리 증명의 정확성을 인증합니다.

Lean에 대해서는 Lean 프로젝트 페이지와 Lean 커뮤니티 웹 페이지에서 더 자세히 알아볼 수 있습니다. 이 튜토리얼은 크고 계속 성장하고 있는 Lean의 라이브러리인 Mathlib에 기반합니다. 아직 가입하지 않으셨다면 Lean Zulip 온라인 채팅 그룹에 가입하실 것을 강력히 권장합니다. 그곳에서 질문에 기꺼이 답해 주고 정신적인 응원을 보내 주는, 활기차고 따뜻한 Lean 애호가 커뮤니티를 만나실 수 있습니다.

이 책은 온라인에서 pdf나 html 버전으로도 읽을 수 있지만, VS Code 편집기 안에서 Lean을 실행하며 상호작용적으로 읽도록 만들어졌습니다. 시작하려면 다음과 같이 하십시오:

이 설치 안내에 따라 Lean 4와 VS Code를 설치하십시오.
VS Code 오른쪽 위 모서리에 있는 ∀(forall) 기호를 클릭하여 저장소를 가져온 다음 Open Project, Download Project, Mathematics in Lean을 차례로 선택하십시오.
이 책의 각 절에는 예제와 연습 문제가 담긴 Lean 파일이 딸려 있습니다. 이 파일들은 MIL 폴더에 장별로 정리되어 있습니다. 이 폴더를 복사한 다음, 그 복사본에서 실험하고 연습 문제를 풀 것을 강력히 권장합니다. 이렇게 하면 원본이 그대로 유지되고, 저장소가 바뀔 때 업데이트하기도 쉬워집니다(아래 참조). 복사본의 이름은 my_files로 하거나 원하는 대로 정하면 되며, 이 복사본을 사용하여 자신만의 Lean 파일을 만들 수도 있습니다.

이제 다음과 같이 VS Code의 사이드 패널에서 교재를 열 수 있습니다:

ctrl-shift-P를 입력하십시오(macOS에서는 command-shift-P).
나타나는 입력줄에 Lean 4: Docs: Show Documentation Resources를 입력한 다음 Enter 키를 누르십시오. (메뉴에서 이 항목이 강조 표시되면 바로 Enter 키를 눌러 선택할 수 있습니다.)
열리는 창에서 Mathematics in Lean을 클릭하십시오.

또는 Codespaces를 사용하여 클라우드에서 Lean과 VS Code를 실행할 수도 있습니다. 그 방법에 대한 안내는 Github에 있는 Mathematics in Lean 프로젝트 페이지에서 찾을 수 있습니다. 이 경우에도 앞에서 설명한 대로 MIL 폴더의 사본에서 작업하기를 권장합니다.

이 교재와 관련 저장소는 아직 작업이 진행 중입니다. mathematics_in_lean 폴더 안에서 git pull을 입력한 다음 lake exe cache get을 입력하면 저장소를 업데이트할 수 있습니다. (이는 MIL 폴더의 내용을 변경하지 않았다고 가정한 것이며, 사본을 만들어 두라고 권한 이유도 이 때문입니다.)

설명, 안내, 힌트가 담긴 교재를 읽으면서 MIL 폴더에 있는 연습 문제를 풀어 보기를 바랍니다. 본문에는 다음과 같은 예제가 자주 나옵니다:

#eval "Hello, World!"

관련 Lean 파일에서 해당 예제를 찾을 수 있을 것입니다. 해당 줄을 클릭하면 VS Code가 Lean InfoView 창에 Lean의 피드백을 보여 주며, #eval 명령 위에 커서를 올리면 VS Code가 이 명령에 대한 Lean의 응답을 팝업 창에 보여 줍니다. 파일을 직접 수정하고 자신만의 예제를 시도해 보십시오.

또한 이 책에는 여러분이 직접 풀어 볼 만한 도전적인 연습 문제가 많이 실려 있습니다. 이 문제들을 서둘러 건너뛰지 마십시오! Lean은 수학에 대해 읽기만 하는 것이 아니라 대화식으로 수학을 직접 하는 것입니다. 연습 문제를 풀어 나가는 과정이 이 경험의 핵심입니다. 모든 문제를 다 풀 필요는 없습니다. 관련 기술을 충분히 익혔다는 확신이 들면 얼마든지 다음으로 넘어가십시오. 여러분의 풀이는 언제든지 각 절에 딸린 solutions 폴더에 있는 풀이와 비교해 볼 수 있습니다.

1.2. 개요

간단히 말해, Lean은 의존 타입 이론이라고 알려진 형식 언어로 복잡한 표현식을 구성하는 도구입니다.

모든 표현식에는 타입이 있으며, #check 명령을 사용하여 이를 출력할 수 있습니다. 어떤 표현식은 ℕ 또는 ℕ → ℕ 같은 타입을 가집니다. 이들은 수학적 대상입니다.

#check 2 + 2

def f (x : ℕ) :=
  x + 3

#check f

어떤 표현식은 Prop 타입을 가집니다. 이것들은 수학적 명제입니다.

#check 2 + 2 = 4

def FermatLastTheorem :=
  ∀ x y z n : ℕ, n > 2 ∧ x * y * z ≠ 0 → x ^ n + y ^ n ≠ z ^ n

#check FermatLastTheorem

어떤 표현식은 P 타입을 가지는데, 여기서 P 자체는 Prop 타입을 가집니다. 그러한 표현식은 명제 P의 증명입니다.

theorem easy : 2 + 2 = 4 :=
  rfl

#check easy

theorem hard : FermatLastTheorem :=
  sorry

#check hard

FermatLastTheorem 타입의 표현식을 구성하는 데 성공하고 Lean이 이를 그 타입의 항으로 받아들인다면, 여러분은 정말 대단한 일을 해낸 것입니다. (sorry를 사용하는 것은 반칙이며, Lean도 그 사실을 알고 있습니다.) 이제 여러분은 이 게임이 무엇인지 알게 되었습니다. 남은 것은 규칙을 배우는 일뿐입니다.

이 책은 Lean의 기반이 되는 논리 체계와 핵심 구문을 더 철저하게 소개하는 자매 튜토리얼 Theorem Proving in Lean을 보완합니다. Theorem Proving in Lean은 새 식기세척기를 사용하기 전에 사용 설명서를 처음부터 끝까지 읽는 편을 선호하는 사람들을 위한 책입니다. 시작 버튼부터 누르고 냄비 세척 기능을 켜는 방법은 나중에 알아내는 편을 좋아하는 사람이라면, 여기서 시작하고 필요할 때마다 Theorem Proving in Lean을 참고하는 편이 더 합리적입니다.

Mathematics in Lean이 Theorem Proving in Lean과 구별되는 또 다른 점은 이 책이 택틱의 사용을 훨씬 더 강조한다는 것입니다. 복잡한 표현식을 만들려 한다는 점을 고려하면, Lean은 이를 위한 두 가지 방법을 제공합니다. 표현식 자체(즉, 그것에 대한 적절한 텍스트 서술)를 직접 적을 수도 있고, Lean에게 그것을 어떻게 구성할지에 대한 지시를 제공할 수도 있습니다. 예를 들어, 다음 표현식은 n이 짝수이면 m * n도 짝수라는 사실의 증명을 나타냅니다:

example : ∀ m n : Nat, Even n → Even (m * n) := fun m n ⟨k, (hk : n = k + k)⟩ ↦
  have hmn : m * n = m * k + m * k := by rw [hk, mul_add]
  show ∃ l, m * n = l + l from ⟨_, hmn⟩

이 증명 항은 한 줄로 압축할 수 있습니다:

example : ∀ m n : Nat, Even n → Even (m * n) :=
fun m n ⟨k, hk⟩ ↦ ⟨m * k, by rw [hk, mul_add]⟩

반면 다음은 같은 정리에 대한 택틱 스타일 증명이며, --로 시작하는 줄은 주석이므로 Lean이 무시합니다:

example : ∀ m n : Nat, Even n → Even (m * n) := by
  -- Say `m` and `n` are natural numbers, and assume `n = 2 * k`.
  rintro m n ⟨k, hk⟩
  -- We need to prove `m * n` is twice a natural number. Let's show it's twice `m * k`.
  use m * k
  -- Substitute for `n`,
  rw [hk]
  -- and now it's obvious.
  ring

VS Code에서 이러한 증명을 한 줄씩 입력하면, Lean은 별도의 창에 증명 상태를 표시하여 이미 확립한 사실이 무엇이고 정리를 증명하기 위해 남은 과제가 무엇인지 알려 줍니다. Lean은 커서가 있는 지점의 증명 상태를 계속 보여 주므로, 줄을 하나씩 따라가며 증명을 재생해 볼 수 있습니다. 이 예에서는 증명의 첫 줄이 m과 n을 도입하고(원한다면 그 시점에 이름을 바꿀 수도 있었습니다), 가설 Even n을 k와 n = 2 * k라는 가정으로 분해한다는 것을 볼 수 있습니다. 두 번째 줄 use m * k는 m * n = 2 * (m * k)임을 보여서 m * n이 짝수임을 보이겠다고 선언합니다. 다음 줄은 rw 택틱을 사용하여 목표의 n을 2 * k로 바꾸고(rw는 “rewrite”의 약자입니다), ring 택틱이 그 결과로 얻은 목표 m * (2 * k) = 2 * (m * k)를 해결합니다.

작은 단계로 증명을 구성하면서 그때그때 피드백을 받을 수 있다는 점은 매우 강력합니다. 그래서 택틱 증명은 증명 항보다 작성하기가 더 쉽고 빠른 경우가 많습니다. 둘 사이에 뚜렷한 구분이 있는 것은 아닙니다. 위 예제에서 by rw [hk, mul_add]라는 구절로 그렇게 했듯이, 택틱 증명을 증명 항 안에 넣을 수 있습니다. 반대로 택틱 증명 중간에 짧은 증명 항을 넣는 것이 유용한 경우도 많다는 것을 보게 될 것입니다. 그렇기는 하지만, 이 책에서는 택틱 사용에 중점을 둘 것입니다.

이 예제에서는 택틱 증명을 한 줄로 줄일 수도 있습니다:

example : ∀ m n : Nat, Even n → Even (m * n) := by
  rintro m n ⟨k, hk⟩; use m * k; rw [hk]; ring

여기서는 택틱을 사용하여 작은 증명 단계를 수행했습니다. 하지만 택틱은 상당한 수준의 자동화를 제공할 수도 있으며, 더 긴 계산과 더 큰 추론 단계를 정당화할 수도 있습니다. 예를 들어, 홀짝성에 관한 명제를 단순화하는 특정 규칙과 함께 Lean의 단순화기를 호출하여 우리의 정리를 자동으로 증명할 수 있습니다.

example : ∀ m n : Nat, Even n → Even (m * n) := by
  intros; simp [*, parity_simps]

두 입문서의 또 다른 큰 차이점은 Theorem Proving in Lean은 Lean 핵심부와 그 내장 택틱에만 의존하는 반면, Mathematics in Lean은 강력하고 계속 성장하고 있는 Lean의 라이브러리인 Mathlib 위에 구축되어 있다는 점입니다. 그 결과, 저희는 라이브러리에 있는 몇몇 수학적 대상과 정리, 그리고 매우 유용한 몇몇 택틱을 사용하는 방법을 보여 드릴 수 있습니다. 이 책은 라이브러리 전체를 개관하는 용도로 만들어진 것이 아닙니다. 커뮤니티 웹 페이지에 방대한 문서가 있습니다. 오히려 저희의 목표는 그 형식화의 바탕에 깔린 사고방식을 소개하고, 기본적인 출발점을 짚어 드려서 여러분이 라이브러리를 편안하게 둘러보고 필요한 것을 스스로 찾을 수 있도록 하는 것입니다.

대화형 정리 증명은 좌절감을 줄 수 있으며, 학습 곡선도 가파릅니다. 하지만 Lean 커뮤니티는 새로 온 사람들을 매우 반갑게 맞이하며, Lean Zulip 채팅 그룹에는 질문에 답해 줄 사람들이 24시간 내내 있습니다. 그곳에서 여러분을 만나기를 바라며, 머지않아 여러분도 그런 질문에 답하고 Mathlib 개발에 기여할 수 있게 되리라 확신합니다.

그러니 여러분이 받아들이기로 한다면, 여러분의 임무는 다음과 같습니다. 뛰어들어 연습 문제를 풀어 보고, 질문이 있으면 Zulip에 찾아오고, 즐기십시오. 하지만 미리 경고해 두겠습니다. 대화형 정리 증명은 수학과 수학적 추론을 근본적으로 새로운 방식으로 생각하도록 여러분에게 도전을 안겨 줄 것입니다. 여러분의 삶은 다시는 예전과 같지 않을지도 모릅니다.

감사의 글. 이 튜토리얼을 VS Code에서 실행할 수 있도록 인프라를 구축해 준 Gabriel Ebner와 Lean 4에서 이식하는 작업을 도와준 Kim Morrison, Mario Carneiro에게 감사드립니다. 또한 다음 분들의 도움과 수정에도 감사드립니다: Takeshi Abe, Julian Berman, Alex Best, Axel Boldt, Thomas Browning, Bulwi Cha, Hanson Char, Bryan Gin-ge Chen, Steven Clontz, Mauricio Collaris, Johan Commelin, Mark Czubin, Alexandru Duca, Pierpaolo Frasa, Denis Gorbachev, Winston de Greef, Darij Grinberg, Mathieu Guay-Paquet, Rik Heurter, Marc Huisinga, Benjamin Jones, Julian Külshammer, Victor Liu, Jimmy Lu, Martin C. Martin, Giovanni Mascellani, John McDowell, Joseph McKinsey, Bhavik Mehta, Sebastian Miele, Isaiah Mindich, Kabelo Moiloa, Hunter Monroe, Pietro Monticone, Oliver Nash, Emanuelle Natale, Filippo A. E. Nuccio, Pim Otte, Nicolas Rolland, Keith Rush, Yannick Seurin, Guilherme Silva, Bernardo Subercaseaux, Pedro Sánchez Terraf, Matthew Toohey, Alistair Tucker, Floris van Doorn, Veniamin Viflyantsev, Eric Wieser 외 여러분께도 감사드립니다. 이 작업은 Hoskinson Center for Formal Mathematics로부터 일부 지원을 받았습니다.