The introduction of automated deduction systems in secondary schools face
several bottlenecks. Beyond the problems related with the curricula and the
teachers, the dissonance between the outcomes of the geometry automated theorem
provers and the normal practice of conjecturing and prov
自动定理证明器和形式证明助手是理论上能够证明任意难题的一般推理系统，但在实践中面临组合爆炸所以包括很多启发式算法和选择点来影响系统性能。机器学习预测器可以引导这些推理系统的工作。本文概述了几个自动推理和定理证明领域及目前对它们进行的学习和人工智能方法，包括前提选择、证明引导、协同推理和学习的 AI 系统以及符号分类问题。