Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs. - Terry Jingchen Zhang; Wenyuan Jiang; Rongchuan Liu; Yisong Wang; Junran Yang; Ning Wang; Nicole Ni; Yinya Huang; Mrinmaya Sachan (CoRR, 2025)