An Evaluation Benchmark for Autoformalization in Lean4. - Jasdeep Sidhu; Shubhra Mishra; Aryan Gulati; Devanshu Ladsaria; Brando Miranda (Tiny Papers @ ICLR, 2024)