The field of formal mathematical reasoning is moving towards increased automation and rigor, with a focus on developing frameworks and tools that can effectively evaluate and generate formalizations of mathematical statements. One notable direction is the development of critic-guided reinforcement learning frameworks, which aim to improve the semantic fidelity of formalizations. Another area of research is the decoupling of high-level reasoning from low-level proof generation, allowing for more powerful and general-purpose reasoning capabilities. Additionally, there is a growing interest in developing robust evaluation metrics for statement autoformalization, such as generalized tree edit distance metrics. Noteworthy papers in this regard include: CriticLean, which introduces a novel critic-guided reinforcement learning framework for mathematical formalization. Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving, which proposes a decoupled framework for automated theorem proving that successfully solves several challenging IMO problems. Generalized Tree Edit Distance, which provides a faithful evaluation metric for statement autoformalization.