# PhysProver: Advancing Automatic Theorem Proving for Physics

arXiv: https://arxiv.org/abs/2601.15737 · HTML: https://mlsanity.com/paper/2601.15737/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 19 of its 43 references that are in the map.
- First posted on arXiv 22 Jan 2026.

## Builds on (most cited first, 19 of 19)

- [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021)
- [GPQA: A Graduate-Level Google-Proof Q&A Benchmark](https://mlsanity.com/paper/2311.12022/) (2023)
- [HybridFlow: A Flexible and Efficient RLHF Framework](https://mlsanity.com/paper/2409.19256/) (2024)
- [OlympiadBench: A Challenging Benchmark for Promoting AGI with Olympiad-Level Bilingual Multimodal Scientific Problems](https://mlsanity.com/paper/2402.14008/) (2024)
- [RAFT: Reward rAnked FineTuning for Generative Foundation Model Alignment](https://mlsanity.com/paper/2304.06767/) (2023)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [Curriculum Reinforcement Learning from Easy to Hard Tasks Improves LLM Reasoning](https://mlsanity.com/paper/2506.06632/) (2025)
- [STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving](https://mlsanity.com/paper/2502.00212/) (2025)
- [Hilbert: Recursively Building Formal Proofs with Informal Reasoning](https://mlsanity.com/paper/2509.22819/) (2025)
- [MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving](https://mlsanity.com/paper/2503.03205/) (2025)
- [Using Large Language Model to Solve and Explain Physics Word Problems Approaching Human Level](https://mlsanity.com/paper/2309.08182/) (2023)
- [Let's Reason Formally: Natural-Formal Hybrid Reasoning Enhances LLM's Math Capability](https://mlsanity.com/paper/2505.23703/) (2025)
- [Enhancing LLMs for Physics Problem-Solving using Reinforcement Learning with Human-AI Feedback](https://mlsanity.com/paper/2412.06827/) (2024)
- [GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving](https://mlsanity.com/paper/2510.11769/) (2025)
- [Lean4Physics: Comprehensive Reasoning Framework for College-level Physics in Lean4](https://mlsanity.com/paper/2510.26094/) (2025)

## Built on by (most cited first, 3 of 3)

- [MerLean: An Agentic Framework for Autoformalization in Quantum Computation](https://mlsanity.com/paper/2602.16554/) (2026)
- [DualityCert: Verifier-Gated Language-Model Repair of Broken Duality Claims in Quantum Field Theory](https://mlsanity.com/paper/2607.23614/) (2026)
- [The Future of AI-assisted Physics: Discovering, Verifying and Organizing Results via Formalization](https://mlsanity.com/paper/2610.14059/) (2026)

## Abstract (arXiv)

The combination of verifiable languages and LLMs has significantly influenced both the mathematical and computer science communities because it provides a rigorous foundation for theorem proving. Recent advancements in the field provide foundation models and sophisticated agentic systems pushing the boundaries of formal mathematical reasoning to approach the natural language capability of LLMs. However, little attention has been given to the formal physics reasoning, which also heavily relies on similar problem-solving and theorem-proving frameworks. To solve this problem, this paper presents, to the best of our knowledge, the first approach to enhance formal theorem proving in the physics domain. We compose a dedicated dataset PhysLeanData for the task. It is composed of theorems sampled from PhysLean and data generated by a conjecture-based formal data generation pipeline. In the training pipeline, we leverage DeepSeek-Prover-V2-7B, a strong open-source mathematical theorem prover, and apply Reinforcement Learning with Verifiable Rewards (RLVR) to train our model PhysProver. Comprehensive experiments demonstrate that, using only ~5K training samples, PhysProver achieves an overall 2.4% improvement in multiple sub-domains. Furthermore, after formal physics training, we observe 1.3% gains on the MiniF2F-Test benchmark, which indicates non-trivial generalization beyond physics domains and enhancement for formal math capability as well. The results highlight the effectiveness and efficiency of our approach, which provides a paradigm for extending formal provers outside mathematical domains. To foster further research, we will release both our dataset and model to the community.