대화형 정리 증명기
사람과 컴퓨터가 협력하여 수학적 정리를 증명하는 도구이다. 사용자가 증명 단계(Tactic)를 입력하면 컴퓨터의 신뢰할 수 있는 커널(Kernel)이 각 단계의 논리적 타당성을 즉시 검증하여 오류 없는 증명을 완성하도록 돕는다.