전술
정리 증명기에서 복잡한 증명 목표를 더 작은 하위 목표로 분해하거나 해결하기 위해 사용하는 고수준 명령이다. LLM은 이 전술 시퀀스를 생성함으로써 기계가 이해할 수 있는 증명 스크립트를 작성한다.