探索性数学的证明接口
Proof Interfaces for Exploratory Mathematics
浏览论文内容
中文总结 AI 辅助
本文扩展Hazel Prover，构建支持多级自动化与详细度的探索性数学证明接口，并支持导出至Rocq，以案例研究验证其教育与应用价值。
中文摘要 AI 辅助
本文描述了一个旨在用于教育应用和探索性数学的数学接口。学习者和数学实践者通常使用纸笔或白板进行等式推理、操作表达式或构建证明。这些工作流程导致各种问题：转录错误、繁琐的书写和符号，以及/或证明论证标准不明确。我们扩展了Hazel Prover——Hazel实时编程环境中的一个等式推理接口——以增加探索性数学的能力，提供针对学生和专家用户的不同详细程度和自动化水平。学生在学习数学概念时需要更刻意的练习，相应地需要更详细的论证，而专家可能受益于显著的数学自动化。考虑到这一点，我们的接口支持基于重写搜索架构的多个级别的数学自动化和简化。对于专家用户，受形式方法可访问性差距的启发，我们支持将证明导出到Rocq定理证明器，将此重写搜索扩展到证明策略。本文最后以几个涵盖小学到大学水平数学的案例研究作结。
英文摘要
This paper describes a mathematics interface intended for both educational applications and exploratory mathematics. Both learners and mathematics practitioners often use pen and paper or a whiteboard to perform equational reasoning, manipulate expressions, or construct proofs. These workflows lead to a variety of problems: transcription errors, tedious writing and notation, and/or unclear standards for proof justification. We extend the Hazel Prover, an equational-reasoning interface in the Hazel live programming environment, to add capabilities for exploratory mathematics, with varying levels of verbosity and automation aimed at both students and expert users. Students require more deliberate practice when learning mathematical concepts and correspondingly more verbose justifications, while experts may benefit from significant mathematical automation. With this in mind, our interface supports multiple levels of mathematical automation and simplification, grounded in a rewrite search architecture. For expert users, motivated by a gap in the accessibility of formal methods, we support proof export to the Rocq theorem prover, extending this rewrite search to proof tactics. This paper closes with several case studies covering elementary- to college-level mathematics.
发表机构
- University of Michigan（密歇根大学）
机构由 AI 辅助整理，请以论文原文为准。
