TLDR: Lean4PHYS is a new framework for formalizing college-level physics problems in Lean4. It includes LeanPhysBench, a 200-statement benchmark, and PhysLib, a foundational library for physics units and theorems. Experiments show current LLMs struggle with formal physics reasoning, but PhysLib significantly improves their performance, highlighting the need for specialized tools beyond math-focused provers.
A new research paper introduces Lean4PHYS, a groundbreaking framework designed to bring college-level physics problems into the world of formal reasoning using Lean4, a powerful proof assistant. This initiative aims to make the reasoning process behind physics problems verifiable and robust, moving beyond traditional natural language explanations.
The core of Lean4PHYS consists of two main components: LeanPhysBench and PhysLib. LeanPhysBench is a new benchmark dataset comprising 200 carefully crafted and peer-reviewed physics statements. These statements are derived from university textbooks and physics competition problems, covering a wide range of topics including mechanics, waves, thermodynamics, electromagnetism, optics, and modern physics. This benchmark is the first of its kind to evaluate the capabilities of Large Language Models (LLMs) in formal physics reasoning within the Lean4 environment.
To support this ambitious goal, the researchers also developed PhysLib, a community-driven repository. PhysLib provides a foundational library for formal physics reasoning, including fundamental unit systems and essential theorems. Unlike mathematics, which has extensive libraries like Mathlib, physics requires specialized infrastructure for units and domain-specific laws. PhysLib addresses this gap by establishing a robust unit system (covering time, length, mass, electric current, temperature, amount of substance, and luminous intensity) and developing topic-based theorem systems for various physics fields.
The framework tackles a significant challenge: bridging the gap between natural language physics problems and their formal Lean4 representations. The researchers developed a pipeline to transform natural language questions into verifiable Lean4 theorems. This involves aligning the problem format from question-answering to proof statements, extracting key conditions and physical laws, and defining explicit proving targets. This process enables LLMs to learn domain-specific laws and reasoning patterns that go beyond standard math-oriented theorem provers.
Experiments conducted with Lean4PHYS revealed interesting insights into the current state of LLMs. Both open-source and closed-source models, including expert Lean4 provers and general-purpose LLMs like GPT-4o, Claude-Sonnet-4, and Gemini-2.5-Pro, showed suboptimal performance on the LeanPhysBench. The best performance achieved was 39.5% by Gemini-2.5-Pro, which is notably lower than what these models achieve in similar natural language math tasks. This highlights the challenging nature of formal physics reasoning for current AI models.
A key finding was the effectiveness of PhysLib. When LLMs were provided with PhysLib in their context, their performance consistently improved by an average of 11.75%. This suggests that PhysLib helps models better understand the unit system and select relevant theorems, enabling them to use more advanced proof tactics. Without PhysLib, models were limited to basic simplification tactics, indicating a lack of inherent understanding of physics-specific formalisms.
The study also observed that expert math provers, despite their strong performance in mathematical Lean, did not necessarily transfer these capabilities effectively to physics problems. In fact, large general models sometimes outperformed expert provers, especially in college-level and easy competition problems. However, expert provers showed an advantage in “competition-hard” problems, which demand extremely long and complex deductions, suggesting their strength in intricate logical steps.
Also Read:
- A Two-Stage Curriculum for General LLM Reasoning
- Assessing Large Language Models’ Chess Understanding with ChessQA
This research marks a significant step towards extending LLM-based formal reasoning from mathematics to broader scientific domains. By open-sourcing PhysLib and LeanPhysBench, the team aims to foster community collaboration and further advance the field of verifiable AI reasoning in physics. For more details, you can read the full research paper here.
