Learner-Centered Design Criteria for Classroom Proof Assistants
summary
Survey synthesizes classroom reports into actionable design rules: error messages must be clear, local, and show which premises are correct (green feedback for satisfied rules), scaffolding must force students to write required hypotheses (Hazel derivation trees) rather than let tactics or random clicking (47% in Educa) win, progression gates require demonstrated learning not blind clicks, induction tools ask for case outlines, algebraic steps may be supported but not taught, and interfaces use familiar notation for transfer to pen‑and‑paper.
AI-written summary · about
chapters (8)
- 0:00Learner-centered proof assistants
- 1:26Design criteria for proof tools
- 3:33Feedback and error handling
- 4:15Scaffolding vs support
- 6:44Bridging proof methods
- 8:31Usability challenges
- 10:38Hazel’s proof tools
- 14:29Q&A
related talks
21mA Case Study on the Effectiveness of LLMs in Verification with Proof Assistants
27mTeaching Software Specification (Experience Report)
01h 03mTactical Design
01h 01m"Design in Practice"
45mWhere AI Meets Code
50mFrom Prompt Hacking to Architectural Determinism: Engineering Reliable GenAI Systems
57mCore Software Design Principles for Programmers
42mThe four rules of simple design