Lean

Lean

패러다임	함수형 프로그래밍, 명령형 프로그래밍
계열	증명 보조기
개발자	Lean FRO
발표일	2013년(13년 전)(2013)
최근 버전	4.29.1[1]
최근 버전 출시일	2026년 4월 14일(4일 전)(2026년 4월 14일)
자료형 체계	정적, 강성, 추론
구현 언어	Lean, C++
운영 체제	크로스 플랫폼
라이선스	아파치 라이선스 2.0
웹사이트	lean-lang.org
영향을 받은 언어
ML Rocq (이전 이름 Coq) 하스켈

Lean은 증명 보조기이자 함수형 프로그래밍 언어이다.^[2] 귀납적 형식론을 포함하는 구성의 계산에 기반을 두고 있다. 깃허브에서 호스팅되는 오픈 소스 프로젝트이다. 개발은 현재 비영리 단체인 Lean Focused Research Organization (FRO)의 지원을 받고 있다.

Lean은 마이크로소프트 리서치에서, 현재는 아마존 웹 서비스에서 근무하는 레오나르도 데 모우라(Leonardo de Moura)에 의해 주로 개발되었으며, 개발 역사 동안 다른 공동 저자 및 협력자들의 상당한 기여가 있었다.

레오나르도 데 모우라가 2013년 마이크로소프트 리서치에서 출시했다.^[3] 나중에 Lean 1과 2로 알려진 언어의 초기 버전은 실험적이었으며, 나중에 폐기된 호모토피 유형 이론 기반의 기능들을 포함했다.

Lean 3 (2017년 1월 20일 첫 출시)은 Lean의 첫 번째로 안정된 버전이었다. 주로 C++로 구현되었으며 일부 기능은 Lean 자체로 작성되었다. 버전 3.4.2 이후 Lean 3은 공식적으로 지원이 종료되었고 Lean 4의 개발이 시작되었다. 이 중간 기간 동안 Lean 커뮤니티 구성원들은 비공식 버전을 3.51.1까지 개발하고 출시했다.

2021년, Lean 4가 출시되었는데, 이는 Lean 정리 증명기를 C 코드를 생성할 수 있도록 재구현한 것으로, 컴파일되어 효율적인 도메인 특정 자동화를 개발할 수 있게 되었다.^[4] Lean 4는 또한 매크로 시스템과 이전 버전보다 개선된 타입 클래스 합성 및 메모리 관리 절차를 포함한다. Lean 3과 비교하여 또 다른 이점은 프런트엔드와 코어 시스템의 다른 주요 부분을 수정하기 위해 C++ 코드를 건드릴 필요가 없다는 것이다. 이들은 이제 모두 Lean으로 구현되었고 최종 사용자가 필요에 따라 재정의할 수 있다.^[2]

Lean 4는 Lean 3과 하위 호환되지 않는다.^[5]

2023년, Lean FRO가 설립되었으며, 언어의 확장성과 유용성을 개선하고 증명 자동화를 구현하는 것을 목표로 한다.^[6]

공식 Lean 패키지에는 표준 라이브러리인 batteries가 포함되어 있으며, 이는 수학 연구와 더 일반적인 소프트웨어 개발 모두에 사용될 수 있는 일반적인 자료 구조를 구현한다.^[7]

2017년에는 연구 수준의 수학까지 가능한 한 많은 순수수학을 하나의 크고 응집력 있는 라이브러리로 디지털화하는 것을 목표로 Lean 라이브러리 mathlib를 개발하는 커뮤니티 유지 관리 프로젝트가 시작되었다.^[8][9] 2025년 5월 기준으로 mathlib는 Lean에서 210,000개 이상의 정리와 100,000개 이상의 정의를 형식화했다.^[10]

Lean은 다음들과 통합된다:^[11]

• 비주얼 스튜디오 코드
• 네오빔
• 이맥스

인터페이스는 클라이언트 확장 및 Language Server Protocol 서버를 통해 이루어진다.

Lean은 유니코드 기호를 기본적으로 지원하며, "\times"와 같이 "×"를 나타내는 LaTeX와 유사한 시퀀스를 사용하여 입력할 수 있다. Lean은 또한 자바스크립트로 컴파일되어 웹 브라우저에서 접근할 수 있으며 메타 프로그래밍에 대한 광범위한 지원을 제공한다.

자연수는 귀납적 형식으로 정의될 수 있다. 이 정의는 페아노 공리계에 기반하며, 모든 자연수는 0이거나 다른 자연수의 다음수임을 명시한다.

inductive Nat : Type
| zero : Nat
| succ : Nat → Nat

자연수의 덧셈은 패턴 매칭을 사용하여 재귀적으로 정의될 수 있다.

def Nat.add : Nat → Nat → Nat
| n, Nat.zero   => n                      -- n + 0 = n
| n, Nat.succ m => Nat.succ (Nat.add n m) -- n + succ(m) = succ(n + m)

두 명제 P와 Q (여기서 ∧ {\displaystyle \wedge } 는 논리곱이고 ⟹ {\displaystyle \implies } 는 실질적 조건문)에 대한 ( P ∧ Q ) ⟹ ( Q ∧ P ) {\displaystyle (P\wedge Q)\implies (Q\wedge P)} 의 간단한 증명은 Lean에서 전술 모드를 사용하여 다음과 같다.

theorem and_swap (p q : Prop) : p ∧ q → q ∧ p := by
  intro h            -- assume p ∧ q with proof h, the goal is q ∧ p
  apply And.intro    -- the goal is split into two subgoals, one is q and the other is p
  · exact h.right    -- the first subgoal is exactly the right part of h : p ∧ q
  · exact h.left     -- the second subgoal is exactly the left part of h : p ∧ q

용어 모드에서 동일한 증명:

theorem and_swap (p q : Prop) : p ∧ q → q ∧ p :=
    fun ⟨hp, hq⟩ => ⟨hq, hp⟩

 증명 보조기 § 주목할 만한 형식화된 증명 문서를 참고하십시오.

Lean은 토머스 헤일스,^[12] 케빈 버자드,^[13] 테런스 타오,^[14] 헤더 맥베스(Heather Macbeth)와 같은 수학자들의 주목을 받았다.^[15] 헤일스는 자신의 프로젝트인 Formal Abstracts에 이를 사용하고 있다.^[16] 버자드는 Xena 프로젝트에 이를 사용한다.^[17] Xena 프로젝트의 목표 중 하나는 임페리얼 칼리지 런던의 학부 수학 교육 과정에 있는 모든 정리와 증명을 Lean으로 다시 작성하는 것이다. 타오는 자신의 실해석학 교과서 Analysis I의 Lean 동반 버전을 출시했으며, 이는 수학 텍스트의 선택된 섹션들을 형식화한 것이다.^[18] 맥베스는 Lean을 사용하여 학생들에게 즉각적인 피드백을 통해 수학적 증명의 기본을 가르치고 있다.^[19]

2021년, 한 연구팀은 Lean을 사용하여 페터 숄체의 응축 수학 분야 증명의 정확성을 검증했다. 이 프로젝트는 최첨단 수학 연구 결과를 형식화했다는 점에서 주목을 받았다.^[20] 2023년, 테런스 타오는 Lean을 사용하여 다항식 프레이만-루즈사(PFR) 추측의 증명을 형식화했으며, 이 결과는 같은 해 타오와 공동 연구자들이 발표한 것이다.^[21]

2022년, 오픈AI와 Meta AI는 독립적으로 Lean에서 다양한 고등학교 수준의 올림피아드 문제 증명을 생성하는 AI 모델을 만들었다.^[22] Meta AI의 모델은 Lean 환경에서 공개적으로 사용할 수 있다.^[23]

2023년, 블라드 테네브(Vlad Tenev)와 투도르 아킴(Tudor Achim)은 Lean 코드를 생성하고 확인하여 AI 환각을 줄이는 것을 목표로 하는 스타트업 Harmonic을 공동 설립했다.^[24]

2024년, 구글 딥마인드는 알파프루프^[25]를 개발했으며, 이는 국제수학올림피아드 은메달 수준으로 Lean에서 수학적 명제를 증명한다. 이는 수학 올림피아드 문제에서 메달 수준의 성과를 달성한 최초의 AI 시스템이었다.^[26]

2025년 4월, 딥시크는 DeepSeek-V3를 기반으로 Lean 4에서 정리 증명을 위해 설계된 AI 모델인 DeepSeek-Prover-V2를 발표했다.^[27]

• 의존형
• 증명 보조기 목록
• Mimalloc
• 유형 이론

• Lean 웹사이트
• Lean 커뮤니티 웹사이트
• Lean FRO
• The Natural Number Game - Lean을 배우기 위한 인터랙티브 튜토리얼
• Moogle.ai - mathlib에서 정리를 찾기 위한 의미론적 검색 엔진

틀:마이크로소프트 자유 소프트웨어

틀:마이크로소프트 리서치