Lean은 함수형 프로그래밍과 수학적 증명을 결합한 독창적인 언어로, 프로그램의 모든 요소를 수학적 표현식으로 취급하여 부작용 없는 계산을 지향합니다. 이 글은 Lean 입문자를 위해 에디터 통합 환경에서의 실시간 피드백 활용법과 표현식 평가를 위한 #eval, 타입 확인을 위한 #check 등 기초 명령어를 상세히 소개합니다. Lean의 핵심인 강력한 타입 시스템을 바탕으로 자연수(Nat)와 정수(Int)의 차이부터 시작하여, 구조체(structure)를 통한 데이터 그룹화와 귀납적 자료형(inductive datatype)을 활용한 합 타입 및 재귀적 구조를 깊이 있게 다룹니다. 특히 데이터를 안전하게 분해하는 패턴 매칭과 논리적 일관성을 위해 종료가 보장되어야 하는 구조적 재귀의 원리를 명확히 설명하며, 타입 인자를 통한 다형성(polymorphism)과 암시적 매개변수 같은 고급 기능이 코드의 재사용성을 어떻게 높이는지 보여줍니다. 나아가 익명 함수, 네임스페이스, 문자열 보간과 같은 현대적 편의 기능을 통해 Lean이 제공하는 프로그래밍 경험의 전반을 아우릅니다. 이 포스팅은 단순한 언어 습득을 넘어 논리적으로 완결된 코드를 작성하고 시스템의 견고함을 추구하는 개발자들에게 Lean의 기초 패러다임을 이해하는 필수적인 출발점이 될 것입니다.