定理证明器

人给出证明思路，机器检查每一步是否严格成立。能处理无限状态。