Pinpointing the Learning Obstacles of an Interactive Theorem Prover. - Sára Juhosová; Andy Zaidman; Jesper Cockx (ICPC, 2025)