REFACTOR: Learning to Extract Theorems from Proofs - Zhou, Jin; Wu, Yuhuai; Li, Qiyang; Grosse, Roger (International Conference on Learning Representations, 2024)