LeanForPhysics: Comprehensive Reasoning Framework for University-level Physics in Lean4

We present Lean4PHYS, a comprehensive reasoning framework for college-level physics problems in Lean4. Lean4PHYS includes LeanPhysBench, a college-level benchmark for Lean4 formal physics reasoning, which contains 200 hand-crafted and peer-reviewed statements formalized from university textbooks and physics competition problems. To establish a solid foundation for formal reasoning in physics, we also launch PhysLib, a repository that contains fundamental unit systems and theorems essential for formal physics proving, which aims to be community-driven and long-term maintained. Based on the LeanPhysBench and PhysLib we composed in Lean4PHYS, we perform exhaustive experiments of baseline results using major expert Math Lean4 provers and state-of-the-art closed-source models, and provide an analysis of their performance. In the experiment, we identify that most expert provers do not outperform general models as they did in the math domain. This indicates a potential overfitting of the math domain rather than learning formal reasoning for formal provers. We also conduct a comprehensive experiment showing that with PhysLib in the context, LLMs' performance on LeanPhysBench increases by 11.90\% on average, proving the effectiveness of our repository in assisting LLMs to solve the Lean4 physics problem. To the best of our knowledge, we are the first study to provide a physics benchmark in Lean4.