연구과정에서 ITP나 ATP같은 proof assistant 사용함??

아니면 사용하는거 본적 있음?  
LEAN 같은거