Lean

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

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

역사

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

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

Lean 4는 Lean 3과 하위 호환되지 않는다.

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

개요

라이브러리

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

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

편집기 통합

Lean은 다음들과 통합된다:

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

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

예시 (Lean 4)

자연수는 귀납적 형식으로 정의될 수 있다. 이 정의는 페아노 공리계에 기반하며, 모든 자연수는 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 (여기서 ∧는 논리곱이고 ⟹는 실질적 조건문)에 대한 (P∧Q)⟹(Q∧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은 토머스 헤일스, 케빈 버자드, 테런스 타오, 헤더 맥베스(Heather Macbeth)와 같은 수학자들의 주목을 받았다. 헤일스는 자신의 프로젝트인 Formal Abstracts에 이를 사용하고 있다. 버자드는 Xena 프로젝트에 이를 사용한다. Xena 프로젝트의 목표 중 하나는 임페리얼 칼리지 런던의 학부 수학 교육 과정에 있는 모든 정리와 증명을 Lean으로 다시 작성하는 것이다. 타오는 자신의 실해석학 교과서 Analysis I의 Lean 동반 버전을 출시했으며, 이는 수학 텍스트의 선택된 섹션들을 형식화한 것이다. 맥베스는 Lean을 사용하여 학생들에게 즉각적인 피드백을 통해 수학적 증명의 기본을 가르치고 있다.

주목할 만한 형식화

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

인공지능

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

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

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

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

같이 보기

각주

  1. ↑ “Release 4.35.0”. 2026년 10월 12일. 2026년 10월 13일에 확인함.
  2. 1 2 Moura, Leonardo de; Ullrich, Sebastian (2021). 〈The Lean 4 Theorem Prover and Programming Language〉 (영어). Platzer, André; Sutcliffe, Geoff (편집). 《Automated Deduction – CADE 28》. Lecture Notes in Computer Science. 12699. Cham: Springer International Publishing. 625–635쪽. doi:10.1007/978-3-030-79876-5_37. ISBN 978-3-030-79876-5.
  3. ↑ “About”. 《Lean Language》. 2024년 3월 13일에 확인함.
  4. ↑ Moura, Leonardo de; Ullrich, Sebastian (2021). Platzer, Andr'e; Sutcliffe, Geoff (편집). 《Automated Deduction -- CADE 28》. Springer International Publishing. 625–635쪽. doi:10.1007/978-3-030-79876-5_37. ISBN 978-3-030-79876-5. S2CID 235800962. 2023년 3월 24일에 확인함.
  5. ↑ “Significant changes from Lean 3”. 《Lean Manual》. 2023년 3월 15일에 원본 문서에서 보존된 문서. 2023년 3월 24일에 확인함.
  6. ↑ “Mission”. 《Lean FRO》. 2023년 7월 25일. 2024년 3월 14일에 확인함.
  7. ↑ “batteries”. 《깃허브》. 2024년 9월 22일에 확인함.
  8. ↑ “Building the Mathematical Library of the Future”. 《콴타매거진》. October 2020.
  9. ↑ “Lean community”. 《leanprover-community.github.io》. 2023년 10월 24일에 확인함.
  10. ↑ “Mathlib statistics”. 《leanprover-community.github.io》. 2025년 5월 7일에 확인함.
  11. ↑ “Installing Lean 4 on Linux”. 《leanprover-community.github.io》. 2023년 10월 24일에 확인함.
  12. ↑ Hales, Thomas (2018년 9월 18일). “A Review of the Lean Theorem Prover”. 《Jigger Wit》.
  13. ↑ Buzzard, Kevin. “The Future of Mathematics?” (PDF). 2020년 10월 6일에 확인함.
  14. ↑ Tao, Terence (2025년 5월 31일). “A Lean companion to "Analysis I"”. 《Terry Tao -- What's New》. WordPress.
  15. ↑ Macbeth, Heather. “The Mechanics of Proof”. 《hrmacbeth.github.io》.
  16. ↑ “Formal Abstracts”. 《Github》.
  17. ↑ “What is the Xena project?” (영어). 《Xena》. 2019년 5월 8일.
  18. ↑ Tao, Terence. “analysis”. 《github.com/teorth》.
  19. ↑ Roberts, Siobhan (2023년 7월 2일). “A.I. Is Coming for Mathematics, Too”. 《New York Times》.
  20. ↑ Hartnett, Kevin (2021년 7월 28일). “Proof Assistant Makes Jump to Big-League Math”. 《콴타매거진》.
  21. ↑ Sloman, Leila (2023년 12월 6일). “'A-Team' of Math Proves a Critical Link Between Addition and Sets” (영어). 《Quanta Magazine》. 2023년 12월 7일에 확인함.
  22. ↑ “Solving (some) formal math olympiad problems”. 《오픈AI》. 2022년 2월 2일. 2024년 4월 13일에 원본 문서에서 보존된 문서. 2024년 3월 13일에 확인함.
  23. ↑ “Teaching AI advanced mathematical reasoning”. 《Meta AI》. 2022년 11월 3일. 2024년 3월 13일에 확인함.
  24. ↑ Metz, Cade (2024년 9월 23일). “Is Math the Path to Chatbots That Don't Make Stuff Up?”. 《New York Times》.
  25. ↑ “AI achieves silver-medal standard solving International Mathematical Olympiad problems” (영어). 《Google DeepMind》. 2024년 5월 14일. 2024년 7월 25일에 확인함.
  26. ↑ Roberts, Siobhan (2024년 7월 25일). “Move Over, Mathematicians, Here Comes AlphaProof”. 《뉴욕 타임스》.
  27. ↑ “DeepSeek upgrades its math-focused AI model Prover”. 《야후 파이낸스》. 2025년 4월 30일. 2025년 4월 30일에 확인함.

외부 링크

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

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