The field of automated theorem proving and mathematical reasoning is moving towards increased automation and scalability. Researchers are exploring new approaches to generate challenging theorem-proof pairs, leveraging theoretical computer science as a source of rigorous proof problems. This has led to the development of frameworks that can automatically synthesize problems with parallel formal and informal specifications, creating a scalable pipeline for generating verified proof challenges. Additionally, there is a growing interest in data-driven approaches to evaluate mathematical results, using graph-based methods to capture citation relationships and compute influence scores. Another area of focus is the advancement of autoformalization, with the proposal of reinforcement learning frameworks that can efficiently autoformalize mathematical concepts with minimal labeled data. Noteworthy papers include:

• Lean Meets Theoretical Computer Science, which demonstrates a scalable approach to generating theorem-proof pairs.
• FormaRL, which proposes a simple yet efficient reinforcement learning framework for autoformalization.
• Connected Theorems, which introduces a graph-based approach to evaluating mathematical results.