The field of automated theorem proving and formal verification is witnessing significant developments with a focus on enhancing the accuracy and robustness of large language models (LLMs) in mathematical reasoning and proof construction. Researchers are exploring innovative approaches to integrate LLMs with formal verification techniques, such as combining LLMs with theorem provers and using retrospective step-aware formal verification frameworks. These advancements aim to mitigate the limitations of current LLM-based systems, including hallucinated logical steps and unverifiable reasoning. The integration of symbolic proof tree supervision, reinforcement learning loops, and iterative self-correction modules is showing promising results in improving proof accuracy and formal verifiability. Noteworthy papers in this area include: ProofNet++, which proposes a neuro-symbolic framework for formal proof verification with self-correction, and Safe, which introduces a retrospective step-aware formal verification framework for identifying hallucinations in mathematical reasoning. Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations also presents significant improvements in autoformalisation and explanation refinement. These developments have the potential to revolutionize the field of automated theorem proving and formal verification, enabling more accurate and reliable mathematical reasoning and proof construction.