1.1. 컴퓨터와 정리 증명🔗

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

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

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

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

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

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

1.2. Lean 소개🔗

Lean 프로젝트는 2013년 마이크로소프트 리서치 레드먼드에서 레오나르도 데 무라(Leonardo de Moura)에 의해 시작되었습니다. 이는 현재도 진행 중인 장기 프로젝트이며, 자동화의 잠재력 대부분은 시간이 지남에 따라 점진적으로 실현될 것입니다. Lean은 Apache 2.0 라이선스 하에 배포되는데, 이는 다른 사람들이 코드와 수학 라이브러리를 자유롭게 사용하고 확장할 수 있도록 허용하는 관대한 오픈 소스 라이선스입니다.

컴퓨터에 Lean을 설치하려면 빠른 시작 안내를 사용하는 것을 고려해 보십시오. Lean 소스 코드와 Lean 빌드 방법에 대한 안내는 https://github.com/leanprover/lean4/에서 확인할 수 있습니다.

이 튜토리얼은 Lean 4로 알려진 Lean의 현재 버전을 설명합니다.

1.3. 이 책에 대하여🔗

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

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

마지막으로, 시스템과 소통하는 데 사용하는 언어와 복잡한 이론 및 데이터를 관리하기 위해 Lean이 제공하는 메커니즘을 포함하여 Lean에 특화된 기능에 대해 배우게 됩니다.

본문 전체에서 아래와 같은 Lean 코드 예제를 찾아볼 수 있습니다:

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

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를 참고하시기 바랍니다.