一句话：通过情境访谈观察 30 名 Rocq 和 Lean 用户，揭示证明助手实际使用中的迭代、对话、外部资源与超越 QED 的设计诉求。
本文关注交互式定理证明器虽重要却难用，设计改进缺乏以用户为中心的理解。作者采用情境访谈（contextual inquiry）方法，观察 30 名参与者在日常工作中使用 Rocq 和 Lean，并对其经验做定性分析。研究提炼出四点观察：证明者根据证明助手反馈反复迭代；证明进展常表现为与证明助手进行有挑战的“对话”；证明构建依赖广泛外部资源；证明者还受“得到 QED”之外的设计考量指引。这些发现刻画了当前证明助手使用的真实面貌，并指出研究者改进可用性时可考虑的潜在机会。
Interactive theorem provers, or proof assistants, are important tools across many areas of computer science and mathematics, but even experts find them challenging to use effectively. To improve their design, we need a deeper, user-centric understanding of proof assistant usage. We present the results of an observation study of proof assistant users. We use contextual inquiry methodology, observing 30 participants doing their everyday work in Rocq and Lean. We qualitatively analyze their experiences to surface four observations: that proof writers iterate on their proofs by reacting to and incorporating feedback from the proof assistant; that proof progress often involves challenging conversations with the proof assistant; that proofs are constructed in consultation with a wide array of external resources; and that proof writers are guided by design considerations that go beyond “getting to QED.” Our documentation of these themes clarifies what proof assistant usage looks like currently and identifies potential opportunities that researchers should consider when working to improve the usability of proof assistants.
@article{paperbot3179,
title = {QED in Context: An Observation Study of Proof Assistant Users},
author = {Jessica Shi and Cassia Torczon and Harrison Goldstein and Benjamin C. Pierce and Andrew Head},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA1},
year = {2025},
doi = {10.1145/3720426}
}