Analysis I의 Lean 컴패니언

• 테렌스 타오가 집필한 실해석학 교재 Analysis I의 핵심 내용을 Lean 증명 보조기로 옮긴 프로젝트임
• 이 프로젝트는 기본 수 체계의 구성과 증명 논리 등, 엄밀성을 강조하는 원서의 목표와 잘 맞는 구조를 가짐
• Mathlib 표준 라이브러리를 활용하되, 주요 개념을 직접 구축하고 독자들이 직접 증명하는 연습이 포함됨
• Lean 코드상 빈칸(sorry) 을 직접 채우며 연습할 수 있어, 공식 해설은 제공하지 않고 포크(fork)로 확장 가능함
• Lean 입문자 및 실해석학 학습자 모두에게 Mathlib과 Lean의 실제 활용법을 체험할 기회로 유용함

개요

• 테렌스 타오가 쓴 실해석학 교재 "Analysis I"를 Lean 증명 보조기 도구로 재구성한 오픈소스 프로젝트임
• 이 교재는 기존 다른 해석학 책들보다 자연수, 정수, 유리수, 실수의 구성 과정, 그 과정에서 필요한 집합론 및 논리적 도구에 더 초점을 맞춤
• 책의 많은 부분이 체계적인 엄밀 증명 능력 개발에 초점을 두고 있어, Lean 같은 증명 보조기와 궁합이 잘 맞는 구조임

Lean 컴패니언 프로젝트의 특징

• 원서의 정의, 정리, 연습문제를 Lean 형식으로 "번역"해 제공함
• 이 Lean 파일들에는 연습문제 풀이에 해당하는 빈칸(sorry) 이 많이 포함되어 있으며, 이를 독자가 직접 채우는 방식으로 학습 가능함
• 공식적인 해설(풀이)은 제공하지 않지만, 독자가 레포지토리를 포크해 자신의 해답 버전을 만들 수 있음

Mathlib와의 연계 및 차별성

• Mathlib(Lean의 표준 수학 라이브러리)에 이미 구현된 개념(예: 자연수)은 일부러 별도로 직접 구축해보고, 이후 Mathlib 버전과의 동형성(등가성)을 증명해 보는 과정도 구성함
• 예시로, Chapter2.Nat에서는 Mathlib의 자연수와 구분되는 자체 정의 natural numbers를 처음부터 구축하고, 주요 결과를 직접 다룬 후, 마지막에 두 버전이 동등함을 Lean에서 연습하도록 함
• 이후 장부터는 Mathlib의 정의와 기능을 점점 더 많이 활용하는 흐름임

학습 및 활용 방법

• 이 Lean 컴패니언은 해석학 학습뿐 아니라, Lean 및 Mathlib에서의 수학 공식화 방법에 대한 입문서 역할도 수행함
• "Natural number game"처럼, Lean 환경에서 수학적 객체를 직접 정의·연습해 볼 수 있는 구조적 연습이 포함됨
• 코드 자체는 Lean에서 컴파일이 가능하지만, 모든 연습문제(sorry)가 실제로 풀 수 있는지 완전 검증은 되지 않았으며, 이런 점에서 플레이테스트 및 피드백이 필요함

오픈소스 및 기여

• 레포지토리는 오픈소스로 누구나 참고·포크·기여할 수 있음
• 공식 솔루션은 따로 제공하지 않으며, 복수의 풀이 버전 생성을 지원함
• 5월 31일 기준, 프로젝트는 별도 독립 레포지토리로 이전됨