통합된 수학 라이브러리
각자 별도로 증명을 만드는 것을 넘어 함께 활용할 수학 지식을 모으는 노력이다. Lean 증명 도구 안에서 정의와 정리를 연결해 더 큰 형식화를 구축할 기반을 마련한다.
종속 타입에 기반한 구성
라이브러리는 종속 타입을 기초로 한다. 소개 논문은 이러한 기반이 다른 증명 도구의 라이브러리와 구별되는 주요 설계 요소라고 설명했다.
구조의 계층과 자동화
폭넓은 수학 구조의 계층을 두고 큰 단위와 작은 단위의 자동화를 함께 사용한다. 공통 구조를 체계적으로 조직하며 증명 작업의 반복을 줄이려는 구성이다.
공동체의 설계와 운영
논문은 라이브러리의 구조와 설계 결정뿐 아니라 이를 만든 분산된 공동체의 조직도 다뤘다. 형식화한 지식을 함께 축적하려면 수학적 표현과 협업 방식이 모두 중요하다는 사례다.
관련 문서
Lean 증명 도구 / LeanDojo / 논리학 / 수학 / 프로그래밍 / Z3