QED in Context: An Observation Study of Proof Assistant Users
summary
An observational study watches 30 proof assistant users (half Rocq and Lean) for ~1 hour each and surfaces four concrete findings: proofs evolve nonlinearly with frequent context switching that relies on the prover resupplying state; much time is spent resolving tiny precision errors and confusing proof states; users routinely reuse mechanized proofs and search lemmas (including a few cases of Copilot — three participants); and authors care about maintainability and style, not just reaching QED.
AI-written summary · about
chapters (8)
- 0:00QED study introduction
- 1:41Study methodology overview
- 3:04Proofs in motion
- 4:29Frictions with provers
- 5:52Leveraging proof sources
- 6:53Beyond QED values
- 8:16Tool design implications
- 9:20Q&A
related talks
24mTowards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by(…)
21mLive Verification in an Interactive Proof Assistant
56mMy Journey to the Dark Side: Under-Approximation, Incorrectness, Proof
57mCoffee-break with EngX Experts
23mHow Novices Perceive Interactive Theorem Provers (Extended Abstract)
01h 10mMedium-scale automation for proof assistants
26mIntegrating graphical proofs in Coq
21mEnhancing Proof Stability