本文综述自动推理在几何教学与定理证明中的进展：分析中学引入自动推理的瓶颈，介绍基于推理规则的几何猜想证明；提出合一逻辑与约束求解框架，用于补全不完整猜想和草图证明；描述整合各类几何证明工具的Open Geometry Prover；利用机器智能在数学数据中发现模式并生成不等式猜想；介绍可自动合成证明题并提供个性化练习的GeoTutor；讨论GeoGebra Discovery中ShowProof等改进；提出用学习技术生成引理辅助证明并解决长期难题；发布arXiv2Formal基准以推动自动形式化；探索用自动规划构建抽象代数基础证明。