(write your synopsis here)
Research under this umbrella topic explores how modern automated theorem proving and reasoning systems are transitioning toward agentic, verifier-guided architectures that combine high-level planning with fine-grained tactic execution. To navigate complex formal state spaces, these frameworks leverage adaptive retrieval of project premises and structural proof patterns, interleave formal symbolic verification directly into text generation, and employ lifelong learning strategies that continuously generalize across expanding mathematical domains. In parallel, step-level verification has advanced through generative process reward models (PRMs) that execute explicit chain-of-thought reasoning before scoring proof steps, derive unsupervised step scores directly from language model token probabilities, and utilize verifiable counterfactual error injection to train robust verifiers. Theoretical developments complement these empirical advances by demonstrating that outcome supervision can match the statistical efficiency of process supervision while revealing that policy optimization algorithms like GRPO implicitly embed process reward mechanisms. Finally, to bypass manual annotation bottlenecks, reinforcement learning paradigms are increasingly powered by intrinsic self-certainty signals, multi-agent zero-sum self-play, and task transformations that convert open-ended problems into self-verifiable proxy environments.
1. Kumarappan, A., Tiwari, M., Song, P., George, R. J., Xiao, C., & Anandkumar, A. (2024). LeanAgent: Lifelong Learning for Formal Theorem Proving. arXiv:2410.06209.
2. Thompson, K., Saavedra, N., Carrott, P., Fisher, K., Sanchez-Stern, A., Brun, Y., Ferreira, J. F., Lerner, S., & First, E. (2024). Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification. arXiv:2412.14063.
3. Liu, H., Sun, J., Li, Z., & Yao, A. C. (2025). ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis. arXiv:2501.18310.
4. Jia, Z., Rakhlin, A., & Xie, T. (2025). Do We Need to Verify Step by Step? Rethinking Process Supervision from a Theoretical Perspective. arXiv:2502.10581.
5. Rajaee, S., Pratik, K., Cesa, G., & Behboodi, A. (2025). Local Look-Ahead Guidance via Verifier-in-the-Loop for Automated Theorem Proving. arXiv:2503.09730.
6. Zhao, J., Liu, R., Zhang, K., Zhou, Z., Gao, J., Li, D., Lyu, J., Qian, Z., Qi, B., Li, X., & Zhou, B. (2025). GenPRM: Scaling Test-Time Compute of Process Reward Models via Generative Reasoning. arXiv:2504.00891.
7. Khalifa, M., Agarwal, R., Logeswaran, L., Kim, J., Peng, H., Lee, M., Lee, H., & Wang, L. (2025). Process Reward Models That Think. arXiv:2504.16828.
8. Zhao, X., Kang, Z., Feng, A., Levine, S., & Song, D. (2025). Learning to Reason without External Rewards. arXiv:2505.19590.
9. Liu, B., Guertler, L., Yu, S., Liu, Z., Qi, P., Balcells, D., Liu, M., Tan, C., Shi, W., Lin, M., Lee, W. S., & Jaques, N. (2025). SPIRAL: Self-Play on Zero-Sum Games Incentivizes Reasoning via Multi-Agent Multi-Turn Reinforcement Learning. arXiv:2506.24119.
10. Sullivan, M., & Koller, A. (2025). GRPO is Secretly a Process Reward Model. arXiv:2509.21154.
11. Yang, Z., Shen, W., Li, C., Chen, R., Wan, F., Yan, M., Quan, X., & Huang, F. (2025). SPELL: Self-Play Reinforcement Learning for Evolving Long-Context Language Models. arXiv:2509.23863.
12. Schrader, T. P., Lange, L., Kaminski, T., Razniewski, S., & Friedrich, A. (2025). A Solver-in-the-Loop Framework for Improving LLMs on Answer Set Programming for Logic Puzzle Solving. arXiv:2512.17093.
13. Wang, J., Zhang, J., Guo, Q., Guo, L., Li, R., Zhang, C., et al. (2026). LongCat-Flash-Prover: Advancing Native Formal Reasoning via Agentic Tool-Integrated Reinforcement Learning. arXiv:2603.21065.
14. Ahn, Y., Yeo, S., Im, G., Lee, J., Yeo, J., & Kim, J. (2026). PROMISE: Proof Automation as Structural Imitation of Human Reasoning. arXiv:2604.05399.
15. Liu, C., Yin, Y., Yuan, Y., Xie, J., Li, B., Li, S., Shen, J., Xu, Y., Shang, L., & Zhang, M. (2026). Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4. arXiv:2604.15839.
16. Sun, Y., Shi, C., Lyu, H., & Xiong, Y. (2026). On Reasoning-Centric LLM-based Automated Theorem Proving. arXiv:2604.19558.
17. Chi, Y., & Wang, Y. (2026). Verifiable Counterfactual Supervision for Process Reward Models. arXiv:2605.02395.
18. Gadetsky, A., Kodryan, M., Panigrahi, S. S., Guo, H., & Brbic, M. (2026). Unsupervised Process Reward Models. arXiv:2605.10158.
19. Wang, Q., Shi, J., Wang, H., Wan, K., Wu, Y., Liu, B., Wu, Q., Li, H. H., Chen, Y., Zhao, H., & Zhao, W. (2026). From RLVR to RLSVR: Task Transformation Induces Self-Verifiable Rewards for Open-Ended LLM Self-Improvement. arXiv:2607.23802.
20. Shen, H., Guo, J., Cui, T., Xiao, Y., & Zhi, L. (2026). MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4. arXiv:2608.02295.
21. Hu, J., Zhang, J., Zhao, Y., & Ringer, T. (2025). HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement. arXiv:2505.15740.
