주장과 증명을 정확하게 쓰기
형식 검증은 주장을 수학적으로 명확히 표현하고 논리적·계산적 방법으로 확인한다. Lean은 수학 정리뿐 아니라 프로그램이 명세를 만족하는지에 관한 추론도 같은 틀에서 다루려 한다.
상호작용과 자동화의 결합
사용자는 증명을 구성하면서 자동화 도구의 도움을 받을 수 있다. 계산이나 추론의 세부 사항을 보조하되 최종적으로는 공리적 기반에 맞는 완전한 증명을 구성하는 것이 목표다.
종속 타입과 프로그램
기반 논리는 귀납적 타입을 포함하는 구성 계산 계열의 종속 타입 이론이다. 수학적 대상과 명제 및 증명을 표현할 수 있고 프로그램의 함수에 관해서도 추론할 수 있다.
도구 자체의 확장
Lean은 메타프로그래밍 언어로도 사용할 수 있다. Lean으로 자동화 기능을 구현하고 표기나 동작을 확장해 더 복잡한 이론과 증명을 관리하도록 지원한다.