[*] Roadmap: Comprehensive Lean 4 Mastery for Math Lab

[Limax314]

Is your feature request related to a problem? Please describe.
현재 math-lab 프로젝트의 목표인 "수학 문제의 디지털화 및 Lean 4를 이용한 엄밀한 증명"을 달성하기 위해, 체계적인 Lean 4 학습 로드맵이 필요합니다. 단순한 도구 사용법을 넘어 수학적 사고를 코드로 옮기는 과정을 단계별로 관리하고자 합니다.

Describe the solution you'd like
다음과 같은 단계별 학습 목표를 설정하고 진행 상황을 체크리스트로 관리합니다.

Phase 1: Interactive Learning (Intuition & Tactics)

이론보다는 게임을 통해 Lean 4의 전술(Tactics)과 논리 구조에 익숙해지는 단계입니다.

• Lean Game Server (Natural Number Game) 클리어
• 기초적인 Propositional Logic 전술 익히기 (intro, apply, exact, rw 등)

Phase 2: Formal Foundations (Theory & Documentation)

Lean 4의 핵심 개념과 함수형 프로그래밍 언어로서의 특성을 이해하는 단계입니다.

• Theorem Proving in Lean 4 학습
• 의존 유형 이론(Dependent Type Theory)의 기초 이해
• 구조체(Structures) 및 클래스(Type Classes) 활용법 익히기

Phase 3: Practical Application (Math Lab Integration)

실제 수학 문제를 Lean 4 파일로 옮기고 증명하는 단계입니다.

• 고등학교 수준의 대수/기하 문제 5개 이상 형식화 (problems/ 폴더 내)
• LaTeX 문서와 Lean 4 증명 코드 간의 연결 구조 확립

Describe alternatives you've considered

• YouTube 강의 시청 (개념 파악에는 좋으나 실습이 부족함)
• 단발성 문제 풀이 (체계적인 문법 습득이 어려움)

Additional context

• 테렌스 타오의 Lean 활용 사례를 참고하여, 실제 연구 수준으로 확장 가능한 기초 체력을 기르는 것을 최종 목표로 합니다.