CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization

Zhongyuan Peng, Yifan Yao, Kaijing Ma +16

Translating natural language mathematical statements into formal, executable code is a fundamental challenge in automated theorem proving. While prior work has focused on generatio…