Lean
린
소개
Lean은 Microsoft Research의 레오나르도 데 모우라가 시작해 현재 비영리 Lean FRO가 유지하는 오픈소스 정리 증명 보조기(proof assistant)이자 의존 타입 함수형 프로그래밍 언어다. 21만 개 이상의 정리를 담은 Mathlib 라이브러리, 메타프로그래밍을 통한 도메인 특화 전술, grind 자동화 등으로 수학·소프트웨어 형식 검증을 지원한다. Google DeepMind의 AlphaProof, DeepSeek-Prover-V2 등 AI 정리 증명 모델이 Lean 4를 표준 백엔드로 활용하면서 AI 수학 연구의 핵심 인프라로 자리 잡았다.
장점
- •Apache 2.0 오픈소스로 개인·연구·상업 사용이 모두 무료다.
- •21만 개 정리·10만 개 정의를 담은 Mathlib 라이브러리로 신규 증명 작성 부담이 작다.
- •Google DeepMind AlphaProof·AWS Cedar 등 산업·연구에서 검증된 형식 증명 인프라다.
- •VS Code·Neovim·Emacs LSP 통합으로 익숙한 에디터에서 바로 증명 작성이 가능하다.
- •메타프로그래밍과 grind 전술로 도메인 특화 자동화를 사용자가 확장할 수 있다.
단점
- •공식 사이트·문서·오류 메시지가 모두 영어 전용으로 한국어 학습 자료가 부족하다.
- •의존 타입·형식 증명 학습 곡선이 매우 가팔라 일반 SW 개발에는 과한 도구다.
- •AI 자동 증명은 AlphaProof 등 외부 모델 의존이며 Lean 자체 내장 AI 기능은 없다.
핵심 기능
형식 증명 커널
최소한의 신뢰 커널이 수학 증명·소프트웨어·하드웨어 검증의 절대 정합성을 보장한다.
Mathlib 라이브러리
21만 개 이상의 정리와 10만 개 이상의 정의를 담은 커뮤니티 수학 라이브러리를 기본 제공한다.
메타프로그래밍
도메인 특화 표기법과 증명 자동화 전술을 사용자가 직접 확장해 만들 수 있다.
grind 자동 증명 전술
패턴 매칭·부등식 풀이를 자동화한 grind 전술로 반복적 증명 부담을 줄인다.
에디터 LSP 통합
VS Code·Neovim·Emacs에서 Language Server Protocol로 실시간 타입 검사·증명 상태 확인이 가능하다.
AI 정리 증명 백엔드
DeepMind AlphaProof·DeepSeek-Prover-V2 등 AI 정리 증명 모델이 Lean 4를 표준 백엔드로 활용한다.
공식 사이트 2026-06-23 검증
요금제
2026-06-23 기준
오픈소스
Free
- Apache 2.0 라이선스
- 개인·연구·상업 사용 무료
- Mathlib 라이브러리 포함
사용자 리뷰
불러오는 중...