ProofBuddy：用于学习与监测的证明辅助工具

证明能力，即书写与检验（数学）证明的能力，是计算机科学中的一项重要技能，但对许多学生而言却是一大难题。主要问题在于形式语言的正确使用，以及确定证明（尤其是学生自己的证明）是否完整且正确。许多学者建议采用证明辅助工具来辅助证明能力的教学，但该方法的成效尚不明朗。为改善现状，我们推出 ProofBuddy：一个基于 Web、使用 Isabelle 证明辅助工具的平台，它使研究者能够通过收集关于学生与证明辅助工具交互方式的细粒度数据，来研究在教育中运用证明辅助工具之方法的成效。我们已在丹麦技术大学对 ProofBuddy 进行了初步的可用性研究。