Lean

린(Lean)은 2013년 마이크로소프트 리서치의 레오나르도 데 모우라(Leonardo de Moura)가 개발한 증명 보조기(proof assistant)이자 함수형 프로그래밍 언어다.

Tactics

택틱은 증명을 구성하는 방법에 대해 설명하는 명령 또는 지침이다. 수학적 증명을 시작할 때는 "정의를 전개하고, 이전 보조정리를 적용하고, 단순화하라"고 설명할 수 있다. 택틱은 이러한 지침과 같은 역할을 한다.