计算机辅助证明和自动化方法在数学教育中的应用

本调查论文是2022年8月在以色列海法举办的ThEdu'22研讨会的邀请主题报告的扩展版本。在简短介绍计算机代数系统（CAS）、动态图形系统（DGS）和其他有用技术的发展后，我们展示了这些技术对数学教育和更广泛的STEAM教育框架的影响。特别是，我们讨论了将数学教育转变为探索-发现-推测-证明的模式，避免将其用作黑箱。这个模式很好地适应了21世纪教育的所谓4C's。沟通与合作不仅在人与人之间，还包括机器之间，以及人与机器之间。在输出的特定特征中增强了批判性思维的需求。我们讨论了用于探索和发现的自动化指令的使用，并提到存在的限制。我们用参数积分（描述数学概念的“认知邻域”）、平面几何和曲线研究（包络线、等光线曲线）中的例子来说明这一主题。其中一些例子已完整演示，其他例子进行了说明并提供了参考。