Lean은 의존 타입 이론(dependent type theory)에 기반한 대화형 정리 증명기이자 범용 프로그래밍 언어로 설계된 현대적인 순수 함수형 언어입니다. Microsoft Research에서 시작되어 현재 Lean FRO에서 개발 중인 이 언어는 프로그램과 증명을 하나의 세계로 통합하며, Lean 자체를 Lean으로 구현할 만큼 높은 자기 완결성을 자랑합니다. 프로그래밍 언어로서 Lean은 실행 전 인자값을 계산하는 엄격성(strictness)과 부수 효과를 명시적으로 관리하는 순수성(purity)을 핵심 원칙으로 삼고 있으며, 특히 타입이 프로그램의 일급 객체가 되는 의존 타입을 통해 정교한 로직 설계를 지원합니다. 이 과정은 함수형 언어에 익숙하지 않은 일반 프로그래머나 증명 자동화 도구를 작성하려는 수학자들을 위해 Lean의 기본 개념과 도구 체계인 elan 및 lake의 활용법을 상세히 다룹니다. 저자 David Thrane Christiansen의 풍부한 경험이 녹아든 유니코드 기반의 수학적 표기법과 단계별 연습 문제는 독자가 함수형 사고방식을 자연스럽게 체득하도록 이끕니다. 수학적 엄밀함과 실용적인 소프트웨어 개발의 접점을 탐구하는 이 여정은 독자가 복잡한 시스템을 더 깊이 이해하고 결함 없는 프로그램을 구축하는 데 필요한 강력한 기술적 토대를 제공합니다.