증명보조기

증명보조기(proof assistant, interactive theorem prover)는 수학적 증명을 형식화하고 검사하기 위한 소프트웨어이다.