Interactive Theorem Provers for Proof Education
summary
A study invites 17 students (8 responded) to use Coq in-class and reports 75% positive experience, 62.5% interested in future use, but also that 50% find the interface and commands hard to learn. A case study formalizes and successfully proved five exercises in Coq and Lean, with Lean matching pen‑and‑paper forward reasoning better while Coq forces more tactic‑oriented steps. Nielsen heuristic analysis finds unclear, low‑level error messages (one hides an invalid hyphen), poor example support, and recommends clearer errors, example‑driven docs, and LLM assistance.
AI-written summary · about
chapters (17)
- 0:00Interactive provers in education
- 1:25Project goals and methodology
- 2:45How ITPs work
- 4:50Literature review on ITPs
- 5:31User study design
- 6:55Key findings from study
- 8:17Usability challenges
- 9:21Case study: Lean and Rocq
- 10:23Pen-and-paper vs Lean proofs
- 12:07Rocq forward reasoning limits
- 13:09Heuristic evaluation framework
- 14:12System vs real-world proofs
- 15:34Recognition over recall in ITPs
- 16:15Error recovery in ITPs
- 17:16ITPs: potential and limits
- 17:58Future work for tools
- 19:20Q&A
related talks
01h 00mIntroduction to Coq - Part 1 of 2
21mA Case Study on the Effectiveness of LLMs in Verification with Proof Assistants
01h 03mImproved Assistance for Interactive Proof
01h 01mDiscussion
01h 02mHow can Machine Learning Help Formal Proving ?
01h 16mCoding Agents: New opportunities for formal methods?
38mAutomatically Synthesising Programs that We Can Trust
17mNeuro-Symbolic Proof Generation for Scaling Systems Software Verification