1.1. 컴퓨터와 정리 증명🔗

형식 검증은 정밀한 수학적 항으로 표현된 주장을 확립하기 위해 논리적·계산적 방법을 사용하는 것을 말합니다. 이러한 주장에는 일반적인 수학 정리뿐만 아니라, 하드웨어나 소프트웨어, 네트워크 프로토콜, 기계 시스템 및 하이브리드 시스템이 각자의 명세를 충족한다는 주장도 포함될 수 있습니다. 실제로는 수학의 한 부분을 검증하는 것과 시스템의 정확성을 검증하는 것 사이에 뚜렷한 구분이 없습니다. 형식 검증을 하려면 하드웨어와 소프트웨어 시스템을 수학적 항으로 기술해야 하며, 그렇게 하고 나면 그 정확성에 관한 주장을 확립하는 일은 일종의 정리 증명이 됩니다. 반대로, 수학 정리를 증명하는 데 긴 계산이 필요할 수도 있으며, 이 경우 정리가 참임을 검증하려면 그 계산이 의도한 대로 수행되는지를 검증해야 합니다.

수학적 주장을 뒷받침하는 최고의 기준은 증명을 제시하는 것입니다. 20세기 논리학의 발전은 여러 기초 체계 가운데 어느 것을 택하더라도 관례적인 증명 방법의 대부분, 어쩌면 전부를 소수의 공리와 규칙으로 환원할 수 있음을 보여 줍니다. 이러한 환원 덕분에 컴퓨터는 두 가지 방식으로 주장을 확립하는 데 도움을 줄 수 있습니다. 하나는 애초에 증명을 찾는 것을 돕는 것이고, 다른 하나는 증명이라고 제시된 것이 올바른지 검증하는 것을 돕는 것입니다.

자동 정리 증명은 “찾기”라는 측면에 초점을 맞춥니다. 도출(resolution) 정리 증명기, 태블로(tableau) 정리 증명기, 고속 충족 가능성 솔버 등은 명제 논리와 1차 논리에서 논리식의 타당성을 입증하는 수단을 제공합니다. 다른 시스템들은 정수나 실수에 대한 선형 또는 비선형 표현식과 같은 특정 언어와 영역을 위한 탐색 절차와 결정 절차를 제공합니다. SMT("satisfiability modulo theories”, 이론 모듈로 충족 가능성)와 같은 아키텍처는 영역 일반적인 탐색 방법과 영역 특화 절차를 결합합니다. 컴퓨터 대수 시스템과 특화된 수학 소프트웨어 패키지는 수학적 계산을 수행하거나, 수학적 한계를 확립하거나, 수학적 대상을 찾는 수단을 제공합니다. 계산 역시 증명으로 볼 수 있으며, 이러한 시스템들 또한 수학적 주장을 입증하는 데 도움을 줍니다.

자동 추론 시스템은 성능과 효율을 추구하며, 그 과정에서 건전성 보장을 희생하는 경우가 많습니다. 이러한 시스템에는 버그가 있을 수 있으며, 시스템이 내놓는 결과가 올바른지 보장하기 어려울 수 있습니다. 이와 대조적으로 대화형 정리 증명은 정리 증명의 “검증” 측면에 초점을 맞추며, 모든 주장이 적절한 공리적 기반 위의 증명으로 뒷받침될 것을 요구합니다. 이는 매우 높은 기준을 세웁니다. 모든 추론 규칙과 계산의 모든 단계는 앞서 제시된 정의와 정리에 근거하여 정당화되어야 하며, 이는 기본 공리와 규칙에 이르기까지 끝까지 이어집니다. 실제로 이러한 시스템 대부분은 다른 시스템에 전달되어 독립적으로 검사될 수 있는, 완전히 정교화된 “증명 객체”를 제공합니다. 이러한 증명을 구성하려면 일반적으로 사용자의 입력과 상호작용이 훨씬 더 많이 필요하지만, 그 대신 더 깊고 복잡한 증명을 얻을 수 있습니다.

Lean 정리 증명기는 사용자 상호작용과 완전히 명세된 공리적 증명의 구성을 지원하는 프레임워크 안에 자동화된 도구와 방법을 배치하여, 대화형 정리 증명과 자동 정리 증명 사이의 간극을 메우는 것을 목표로 합니다. 그 목표는 수학적 추론과 복잡한 시스템에 관한 추론을 모두 지원하고, 두 영역 모두에서 주장을 검증하는 것입니다.

Lean의 기반 논리에는 계산적 해석이 있으며, Lean은 프로그래밍 언어로도 똑같이 볼 수 있습니다. 더 정확히 말하면, Lean은 정확한 의미론을 갖춘 프로그램을 작성하고 그 프로그램이 계산하는 함수에 대해 추론하는 시스템으로 볼 수 있습니다. Lean에는 자기 자신의 메타프로그래밍 언어로 쓰일 수 있는 메커니즘도 있습니다. 즉, Lean 자체를 사용하여 자동화를 구현하고 Lean의 기능을 확장할 수 있습니다. Lean의 이러한 측면은 무료 온라인 책인 Functional Programming in Lean에서 다루지만, 이 시스템의 계산적 측면은 이 책에서도 등장할 것입니다.

1.2. Lean 소개🔗

Lean 프로젝트는 2013년 Microsoft Research Redmond에서 Leonardo de Moura가 시작했습니다. 이는 현재 진행 중인 장기적인 노력이며, 자동화의 잠재력 중 상당 부분은 시간이 지남에 따라 점진적으로만 실현될 것입니다. Lean은 Apache 2.0 라이선스로 배포됩니다. 이 라이선스는 다른 사람들이 코드와 수학 라이브러리를 자유롭게 사용하고 확장할 수 있도록 허용하는 관대한 오픈 소스 라이선스입니다.

컴퓨터에 Lean을 설치하려면 Quickstart 안내를 참고하십시오. Lean 소스 코드와 Lean 빌드 안내는 https://github.com/leanprover/lean4/에서 확인할 수 있습니다.

이 튜토리얼은 Lean 4라고 불리는 Lean의 현재 버전을 설명합니다.

1.3. 이 책에 대하여🔗

이 책은 Lean에서 증명을 작성하고 검증하는 방법을 가르치기 위해 만들어졌습니다. 이를 위해 필요한 배경 지식의 대부분은 Lean에만 국한된 것이 전혀 아닙니다. 우선 여러분은 Lean의 기반이 되는 논리 체계를 배우게 됩니다. 이 체계는 의존 타입 이론의 한 버전으로, 거의 모든 통상적인 수학 정리를 증명할 수 있을 만큼 강력하며 이를 자연스러운 방식으로 해낼 수 있을 만큼 표현력이 풍부합니다. 더 구체적으로 말하면, Lean은 귀납적 타입을 갖춘 구성 계산법(Calculus of Constructions)이라는 체계의 한 변형에 기반을 두고 있습니다. Lean은 의존 타입 이론에서 수학적 대상을 정의하고 수학적 주장을 표현할 수 있을 뿐만 아니라, 증명을 작성하기 위한 언어로도 사용할 수 있습니다.

완전히 상세한 공리적 증명은 매우 복잡하기 때문에, 정리 증명에서 해결해야 할 과제는 컴퓨터가 세부 사항을 가능한 한 많이 채워 넣게 하는 것입니다. 의존 타입 이론에서 이를 뒷받침하는 다양한 방법을 배우게 됩니다. 예를 들어 항 재작성이 있고, 항과 표현식을 자동으로 단순화하는 Lean의 자동화된 방법이 있습니다. 마찬가지로 정교화와 타입 추론 방법도 있으며, 이는 유연한 형태의 대수적 추론을 뒷받침하는 데 사용할 수 있습니다.

마지막으로, 시스템과 소통하는 데 사용하는 언어와 복잡한 이론 및 데이터를 관리하기 위해 Lean이 제공하는 메커니즘을 비롯하여 Lean에만 있는 기능에 대해 배웁니다.

본문 전반에 걸쳐 아래와 같은 Lean 코드 예제를 볼 수 있습니다:

이 책의 모든 코드 예제 옆에는 “Copy to clipboard”라고 적힌 버튼이 있습니다. 이 버튼을 누르면 코드가 올바르게 컴파일되는 데 필요한 주변 맥락과 함께 예제가 복사됩니다. 예제 코드를 VS Code에 붙여 넣어 수정할 수 있으며, 입력하는 동안 Lean이 결과를 계속 검사하고 피드백을 제공합니다. 이어지는 장들을 공부하면서 예제를 실행해 보고 코드를 직접 실험해 보기를 권장합니다. VS Code에서 “Lean 4: Docs: Show Documentation Resources” 명령을 실행하고, 열리는 탭에서 “Theorem Proving in Lean 4”(Lean 4로 하는 정리 증명)를 선택하면 이 책을 열 수 있습니다.

1.4. 감사의 글🔗

이 튜토리얼은 Github에서 관리되는 오픈 액세스 프로젝트입니다. 많은 분들이 수정 사항, 제안, 예제, 본문을 제공하며 이 작업에 기여해 주셨습니다. 기여해 주신 Ulrik Buchholz, Kevin Buzzard, Mario Carneiro, Nathan Carter, Eduardo Cavazos, Amine Chaieb, Joe Corneli, William DeMeo, Marcus Klaas de Vries, Ben Dyer, Gabriel Ebner, Anthony Hart, Simon Hudon, Sean Leather, Assia Mahboubi, Gihan Marasingha, Patrick Massot, Christopher John Mazey, Sebastian Ullrich, Floris van Doorn, Daniel Velleman, Théo Zimmerman, Paul Chisholm, Chris Lovett, Siddhartha Gadgil께 감사드립니다. 훌륭한 기여자분들의 최신 목록은 lean prover와 lean community에서 확인하십시오.