1. 소개

1.1. 시작하기

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

Lean에 대해 더 알아보려면 Lean project page와 Lean community web pages를 참고하십시오. 이 튜토리얼은 Lean의 크고 계속 성장하는 라이브러리인 Mathlib을 기반으로 합니다. 아직 가입하지 않았다면 Lean Zulip online chat group에 가입하는 것을 강력히 권장합니다. 그곳에서 여러분은 Lean 애호가들의 활기차고 친절한 커뮤니티를 만나게 될 것이며, 그들은 기꺼이 질문에 답하고 정신적 지지를 보내줄 것입니다.

이 책의 pdf나 html 버전을 온라인으로 읽을 수도 있지만, 이 책은 VS Code 편집기 안에서 Lean을 실행하며 대화식으로 읽도록 설계되었습니다. 시작하려면 다음과 같이 하십시오:

다음 installation instructions를 따라 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를 입력한 다음 엔터를 누르십시오. (메뉴에서 항목이 강조 표시되는 즉시 엔터를 눌러 선택할 수 있습니다.)
열리는 창에서 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의 근간이 되는 논리 체계와 핵심 문법을 더 철저하게 소개하는 보조 튜토리얼인 Lean에서의 정리 증명을 보완합니다. Lean에서의 정리 증명은 새 식기세척기를 사용하기 전에 사용 설명서를 처음부터 끝까지 읽는 것을 선호하는 사람들을 위한 책입니다. 만약 여러분이 시작 버튼을 먼저 누르고 나중에 포트스크러버 기능을 활성화하는 방법을 알아내는 것을 선호하는 부류의 사람이라면, 여기서부터 시작한 뒤 필요할 때마다 Lean에서의 정리 증명을 참고하는 편이 더 합리적입니다.

Mathematics in Lean을 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 채팅 그룹에서 사람들이 하루 종일 질문에 답해줍니다. 우리는 여러분을 그곳에서 만나기를 바라며, 머지않아 여러분도 그런 질문에 답할 수 있게 되고 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의 부분적인 지원을 받았습니다.