Lean4Physics: Comprehensive Reasoning Framework for College-level Physics in Lean4
Authors: Yuxin Li
Minghao LIU
Ruida WANG
JI WenZhao
Zhitao He
Rui Pan
Junming Huang
Tong Zhang
Yi R. Fung
Venue: ICLR 2026 Poster (2026)
Keywords: Lean4
Reasoning
AIforScience
Primary area: datasets and benchmarks
TL;DR: This paper presents Lean4PHYS, a reasoning framework for college-level physics problems in Lean4. It includes LeanPhysBench, the first benchmark in the field, and PhysLib, a community-driven repository that sets the foundation for the field.

Abstract: We present **Lean4PHYS**, a comprehensive reasoning framework for college-level physics problems in Lean4. To establish a solid foundation for formal reasoning in physics, **Lean4PHYS** launches *PhysLib*, a repository containing fundamental unit systems and essential theorems to formulate physics proofs in Lean4. It will be community-driven and long-term maintained. Lean4PHYS also includes *LeanPhysBench*, a college-level benchmark for evaluating LLMs' Lean4 formal physics reasoning capability. It contains 200 hand-crafted and peer-reviewed Lean4 theorem statements formalized from university textbooks and physics competition problems. Based on the *PhysLib* and *LeanPhysBench* we composed in **Lean4PHYS**, we perform exhaustive experiments of baseline results using major expert Math 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 suggests potential overfitting to 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 in solving the Lean4 physics problem. To the best of our knowledge, we are the first study to provide a physics benchmark in Lean4.

Published as a conference paper at ICLR 2026
COMPREHENSIVE FRAMEWORK FOR COLLEGE-LEVEL PHYSICS IN LEAN4
LEAN4PHYSICS:
REASONING
Yuxin Li"; Minghao Liu'; Ruida Wang"; Wenzhao Ji', Zhitao He', Rui Pan', Junming Huang'. Tong Zhang". Yi R. (May) Fung! 'Hong Kong University of Science and Technology,
University of Illinois Urbana- Dabana-Champpign,
'Princeton University
*MMSense Lab
[yling, m1 mumbmy wjiab, whebuuecoonecct (ewnneect..nooooooooo ust.
(ruidaw, ruip))ew,oipp edu jumminghaang$ppinnctoo.. edu tongghaangetonggzhang- ml. org yrfungeust.hk
ABSTRACT
We present Lean4PHYS, a comprehensive reasoning framework for college- level physics problems in Lean4. To establish solid foundation for formal reasoning in physics, Lean4PHYS launches PhysLib, a repository containing fundamental unit systems and essential theorems formulate physics proofs Lean4. It will be community-driven and long-term maintained. Lean4PHYS also includes LeanPhysBench, college-level benchmark for evaluating LLMss Lean4 formal physics reasoning capability. It contains 200 hand-crafted and peer-reviewed Lean4 theorem statements formalized from university textbooks and physies competition problems. Based on the PhysLib and LeanPhysBench we composed in Lean4PHYS, we perform exhaustive experiments of baseline results using major expert Math provers and state-of-the-arr closed-soure mod- els, and provide an analysis their performance. In the experiment, we iden- tify that most expert provers do not outperform general models they did in the math domain. This suggests potential overfitting to the math domain rather than learning formal reasoning for formal provers. We also conduct a prehensive experiment showing that, with PhysLib in the context, LLMs' per- formance on LeanPhysBench increases by 11.90% fectiveness of our repository in assisting LLMs in solving the Lean4 physics problem. To the best of our knowledge, we are the first study provide a physics benchmark in Lean4. The code for this project will soon be released in htttp:://gituu. com/ http://iiieeyy...ii/ieeeaaaaeeae
average, proving the ef-
INTRODUCTION
Formal thinking capability has always been considered cornerstone of human intelligence and key objective of machine learning. With the emergence of Large Language Models (LLMs), many studies explore diverse ways to apply LLMs perform various reasoning tasks. This includes general reasoning (Wang et al. 2024b; Suzgun et al.] 2022 Talmor et al. 2018). math reason- ing (Hendrycks al. | 2021 1 Cobbe et al. 2021 Guo al. 2025) natural science reasoning (Saikh) et al., [2222] [dwards et al. 2025), and many other domains (He et al. [2025a] (Su et al.) 2025). However, most works handle reasoning
pure Natural Language (NL) task that relies on the
swer checking to judge the correctness of reasoning, while being unable to verify the intermediate reasoning steps.
Fiist Authors
"orresponding Author

---

Published as a conference paper at ICLR 2026
(6) Formal Data Conseraction
Natural Langsage Stalemeni
Platen Tew Sweul molee shaeet "eoestue amas
Formal Languagr Natement
LomnAlysfoncc
Craditioo
Poatees Namae cody by
Hypsthoa
Prening lorget Fatraciee
undiuell to ieloee bucn ard
Ballard
Optis
PL franslation with PlyxL.
Waver
Quoeriiss
Siego
Mechanics
Waves
nagretism
Electro-
Therma- synamic
Duve as in we
Calcalation Support Layer (SI Derivation)
Geal
Therandyyani
System
toe to plctees 2o pi
Elatrsnggation
Unit
LLMs &ennolist and PlysLik Prompt
Verification
Mixed Statement
Proff
Statument
Statement
LEN
FL Statement
faaae und Syndeatyy Hamt
Mixed Statement
Proof
Evalustion Results
Performance Evalustion
Figure I: Overview of the Lean4PHYS framework: (a) Benchmark and Library Construction: The benchmark and library are developed using a bottom-up principle. We first establish the founda- tional units and SI system of PhysLib, then compose the calculation support, and finally construct the field-related theorems. For the benchmark, NI. questions are transformed from a guestion-answeriin format to proof problems and subsequently formalized into Lean4 statements. (b) LLM Performance Evaluation: We evaluate the formal physics reasoning capabilities of major open and closed-soures LLMs on Lean BeanPhysBench, both with and without PhysLib. After inference is completed, Lean4 auto-verification evaluates model performance and highlights the utility of PhysLib.
To make the reasoning process verifiable, researchers attempted to ground the reasoning procedure formal logical systems, enabling the automatic verification of both the reasoning process and its results through Formal Languages (FI.s. Through this idea, many FLs are developed, including Lean (De Moura et al. 2015 Moura & Ullrich 2021). Coq (Cog) 1996). Isabelle (Paulson) 1994). and HOL (Harrison) 2009). Among them, Lean4 has received superior attention from both the academic and industry in recent days, making it one of the most well-studied formal languages in recent years. There are numerous benchmarks (Zheng al.
2021: Gulati et al. 2024 Azerbayev
et al. 2023), dataset (Dong & Ma 2025 Wang et al. 2024a
Ying et al. 2024). 4), and provers (Polu
al.
2022 Wang al. [024aa] Xin et al. 2024 Wang et al.
2025c Lin al. 2025b Dong & Ma
2025
Xin et al. 20255 Ren et al. 2025) have been proposed.
However, current studies in formal reasoning primarily focus on the mathematical domain, leaving other domains that can also be formalized, such as physics, largely understudied. Moreover, most of the state-of-the-art expert provers claim their capability in formal reasoning by showing superior results in Lean4 math benchmarks. This raises concerns about whether such formal capability can be transferred to other domains, like physies problems represented using similar Lean syntax, or current provers overfit to mathematical reasoning.
To answer the problems above, we propose Lean4PHYS, a comprehensive reasoning framework for college-level general-domain physics problems in Lean4. Lean4PHYS aims to provide a foun- dation for LLM-based formal physics reasoning in Lean4. The overview of Lean4PHYS is pre- sented in Figure 1 The framework launches PhysLib, foundation repository that supports formal physics reasoning. It includes a systematic treatment of physical units through a dedicated UnitsSys- tem, enabling dimensionally consistent symbolic computation, along with growing collection of extendable formalized physics theorems. Based on the PhysLib, we develop LeanPhysBench, a college-level benchmark evaluate L.Mss' performance in Lean4 physics reasoning. The bench-
2

---

Published as a conference paper at ICLR 2026
mark contains 200 manually-cratee Lean4 formal theorems whose difficulty level varies from stan- dard university exercises to Olympiad-style competition problems. We construct the benchmark by systematically transforming natural-language problems into Lean4 theorems: extracting key condi- tions and relevant physical laws, defining explicit proving targets, restating the problems in logical form, and integrating them into verifiable Lean4 statements. To the best of our knowledge, Lean- PhysBench is the first benchmark that evaluates LLMs' formal physics reasoning capability.
We summarize our contributions follows:
1. We introduce Lean4PHYS, a comprehensive Lean4-based framework for formal physics reasoning. It provides PhysLib, a modular physics library supporting unit-aware calcula- tions and extensible physical theorems.
2. Our framework innovates by bridging natural-language physics problems with formal Lean4 representations, enabling LLMs to learn domain-specific laws and reasoning pat- terns beyond standard math-oriented theorem provers.
3. We use LeanPhysBench evaluate the leading model's performance in formal physics rea- soning. The experiments suggest that all current expert math provers and general models, regardless of their size, achieve suboptimal performance. Furthermore, we demonstrate that after integrating PhysLib, the models exhibit consistent performance enhancements. The results also indicate the potential for overfitting to the math dataset for the current ex- pert Lean provers. When testing only on the hard dataset, we found that all models perform poorly, indicating the current limitations for formal physics, especially statements involv- ing complex calculation- based mathematical operations such integrals and derivatives.
Moreover, to the best of our knowledge, Lean4PHYS is the first work that tries to extend the LLM- based formal reasoning from math to a more general domain, which offers new direction that attempts to formalize progressively more subjects.
2 THE LEAN4PHYS FRAMEWORK
In this section, we introduce the design and implementation of the Lean4PHYS framework detail. The core idea of our framework is to provide foundation and then evaluate the LLMs' formal physics reasoning capabilities. We firstly initiate PhysLib, a community collaborative foundation repository for Lean4 physics reasoning in Section 2. Subsequently, present the details of how we construct LeanPhysBench, (to the best of our knowledge) the first benchmark for formal physics reasoning.
2.1 PHYSLIB
In this paper, we introduce PhysLib,, a community-driven repository designed to support rigorous and machine-verifiable Lean4 formal physics reasoning. We build the library a bottom-up manner for both the conceptual level of knowledge and the technical level of implementation. The current version of PhysLib contains the foundation of physics unit systems (Section 2.1.I), practical theo- rems to in proving (Section 2.1.2. and guideline for community development and extension (Section 2.1.3
2.1.1 FOUNDATION OF PHYSICS: UNIT SYSTEM
The central challenge of formalizing physics from scratch is identify the unchanged kernel that supports all the reasoning in the field. Unlike mathematics, where every basic building block is purely based on definition, physics, as well as other natural sciences, are primarily supported by empirical rules induced from experiments, which are naturally not clearly defined mathematics. For physics, we identify such a kernel as the unit system. Thus, we lay the foundation for physics reasoning by establishing the unit system.
In the implementation, we build the unit system by extending Mathlib (mathlib Community 2020) with the International System of Units (SI) following Tao (2025). The system contains seven basic units, including time, length, mass, electric current, thermodynamic temperature, amount sub- stance, and unit of luminous intensity (Newell et al. 2019). Based the unit system foundation,

---

Published as a conference paper at ICLR 2026
introduce the first-order derivative over the most general and commonly used sections, namely, length, taking the derivative over time, introducing velocity.
2.1.2 TOPIC-BASED THEOREM DEVELOPMENT
Building upon the cross-topic kernel foundation system of units, we introduce topic-based theorem systems according different needs in specific kinds of problems. Specifically, the current version of PhysLib splits problems into six major topics, namely: mechanics, waves & acoustics, thermo- dynamics, electromagnetism, optics, and modern physics. The topic split is inspired by Young & Freedman 2019). Our implementation principle for this section of PhysLib is to first create differ- ent namespaces and independent Lean files for each topic. Subsequently, we add topic-specific unit types and constants in the topic namespace. Then, we implement basic physies rules summarized from experiments as definitions. Finally, we implement theorems with their proofs that are practical to the topic the final layer. We implement the mechanics field in detail as example and set basic foundation for other topics. We present the design process to the community and launch this project for collaborative development of the field.
2.1.3 COMMUNITY-DRIVES AND EXTENSIBILITY
As mentioned before, PhysLib is designed to be community-drivve and collaborative work like Mathlib (mathlib Community 2020), and we make our best effort to ensure other researchers can easily read and extend the system while maintaining consistency. In general, we organize PhysI.ib in a three-layer hierarchy: (1) Foundation unit system, which should be consistent with changes only necessary. (2) Topic-specific unit system, which should be added when formalizing theorem statements where current units are unable to support the construction.
(3) Topic-specific theorems, which include most of the practical theorems to support proof implementation and should be regu- larly updated.
The current version contains a relatively comprehensive implementation of the repository in me- chanics, serving which are distributed under the Apache-2.0 license, and the same license applies newly added content. We will strongly encourage contributions of new statements and proofs, and will continu- ously maintain the repository in the future.
example for the community. Phys/ib inherits components from Tao (2025),
Beyond the current repository we are implementing, such layered design is applicable to the for- malization of other domains, such as the natural and social sciences, and alternatively extended to general proving systems based the same logic.
2.2 LEANPHYSBENCH
With the current trend of utilizing LLMs to perform formal reasoning, it is crucial to evaluate their formal physics reasoning capability. However, to the best of our knowledge, there is no dataset for benchmarking the Lean4 physics reasoning capability for LLMs. Thus, propose (to the best of our knowledge) the first benchmark for Lean4 physics reasoning. In this section, we detail the process of creating this benchmark. We firstly present the data collection process in Section [.2. then detail how we created the benchmark in Section 2.2.2 and report the benchmark statistics in Section 2.2.3
2.2.1 DATA COLLECTION & PREPROCESSING
Corresponding the bottom-up principle, when we design the PhysLib, when creating the dataset, we follow a basic-to-advanced principle. Our benchmark primarily consists of two levels of data: the high school dlympiad-competition collected from competition-relatee exercise books. This level of data focuses on testing the model's capability to perform multi-step reasoning within a specific field of knowledge. On the other hand, the college-level problems are collected from the elementary university physics textbooks. These problems are selected to cover a deeper range of concepts with easier reasoning steps that focus on testing the LLM's reasoning when the topics span multiple physics models. For questions accom- panied by figures, we extract the information from the figures and describe it in natural language, alongside the problems.
level and the college level. The Olympiad data are
4

---

Published as a conference paper at ICLR 2026
College Level
Competition Level
theoren
theorem corpetition www.mmechhhhcceecc. Ch2_g92
0x.0x Hlenghh)
(eaM) (R (R: (eenttnn :R) (p:espee) RR Poroe)
(bupos:0 m.va
g3a1)
(h_sin_ccs ocs: Real.sin :...nnoos:Rea..ii
Resllcos
(e:Acceleratior)
de Reallain 8-))
:cngth
RLooriz 0 Res.cccs0...
(c0::_0=0-=eccon))
y
(t1:tt_144
vert :Real.ooe
beel.sin@--fr
[0::dt=t_3-__00
(F_aet: =m "Boaliic 0..11.00000
(b::s=0y_1~__00mr)
Reslicss 0111////11)
(w::V,.fttvv.04
6-
(vi:v_1=vtttt)
Roal.cin x112///1
(hx: (n: 2:0 -
(tric (tric__aound pound peanddllswwall [[sssllll S [[xxal]]::
Y 20,
Ve=-l)--
2-moter/secorat
== a- --------222
(Rea [--ee (R) " Reslicos gg
(2-6 =0tta//sccoood2
(Rcalisin 8 BB
neter// cecond))
(Rcal.cos (e:e::) :R) Realisin
ba sorry
by sorry
Figure 2: Two examples from LeanPhysBench demonstrating different difficulty levels.
Following PhysLib's design, further divided the topic of the LeanPhysBench into mechanics, waves acoustics, thermodynamics, electromagnetism, optics, and modern physics. After the data collection, have the base natural language statement for formulating LeanPhysBench.
2.2.2 FORMALIZATION PIPELINE
Following the collection and preprocessing of the NL data, apply strict pipeline to transform the NL data into verifiable Lean4 theorems. The overview of the formalization pipeline is shown in Figure a)). Formally, if we denote physies problem want formalize by P. the original problem we have is Poriginal. the target is to obtain the Lean4 version of the problem PLean. The formalization process is follows:
NL Format Alignment According previous work in formalizing mathematical state- ments (Wang et al. 2025b Zheng et al.) (02T), there is a significant representation gap between Lean4 statements and their corresponding NL problems in the original datasets. Specifically, in NL problems, it is typical for the problems to be in question-answa answerins format, where the target is to find a specific numerical or formulaic answer. However, Lean4, problem type a closed-end proof rather than a specific answer, which leads to gap in the statement. Inspired by Wang et al.) style physics problem
(2025b), we perform format alignment to transform the into a proof statement.
The first step in format alignment is to restate the question-answering problem in a proof format. Specifically. transform the question part of "Finding the answer answer is following Zheng et al. (202I). Subsequently, to better model the physical process and relations, require the LLM write step-by-step solution to the question. Based on the solution, we extract the physics laws used in the problems and all the initial conditions for composing statements. Finally, define the proving target for the problem. We split the target of proof into three categories, namely, numerical value, physical expression, or logical formula describing physical state and such targets assist the process of Lean4 code writing. After this step, align the NL drestton-answelde problem to a provable question with extracted physics laws, initial conditions, and proving target.
into "Prove that the
Lean4 code writing & Verification After we obtain aligned NI problems, the Lean code writing is split into the formalization of conditions and goals. During the process of writing Lean4 con- ditions for the problem, we add the necessary physics laws to PhysLib as well as properly present such laws in Lean code. In formalizing goals, we write the corresponding Lean4 expression of the proving targets as goals for the Lean4 proof. After we obtain the Lean4 code, it submitted to the verifier to verify whether it compiles successfully. Additionally, ask experts for physics and Lean to check the completeness of the theorem. Each statement requires one expert to formalize and at least two experts to verify.
5

---

Published as a conference paper at ICLR 2026
The above pipeline ensures that problems in LeanPhysBench accurately capture the underlying physics semantics from NL descriptions. We present two examples of Lean4 statements we for- malized in Figure In the example, relatively simple operations a broader range of topics. Competition- statements emphasize derivations of formulas using more advanced math tools in concentrated field of physics.
clearly that the college-level problems focus
2.2.3 BENCHMARK STATISTICS
The detailed statistics for the LeanPhysBench are presented in Figure 3 In total, LeanPhys- Bench contains 200 physics statements formal- ized in Lean4. Among them, 104 statements the college-level and 96 are the com- petition level. The competition level is fur- ther divided into easy (62 problems) and hard (34 problems) categories. Where easy prob- lems focus more on mathematical deduction with looser conditions, and hard problems fo- cus more on physics problem deductions with more physies formulas and tighter conditions.
17%
Thor Mhreaaeanki
Coline 57%
Corpetioniiiy
Wales
you
Modaako
Figure 3: Statistics of LeanPhysBenck: The dis- tribution of 200 Lean4 physics statements across difficulty levels and topics.
EXPERIMENT
We conduct comprehensive experiments Lean4PHYS demonstrate the significance of proposed LeanPhysBench and the effectiveness of Physl.ib. In particular, we demonstrate the per- formance of major expert Lean provers and general models on LeanPhysBench and prove the effec- tiveness of PhysLib in Section 3.2 We study the problem format of LeanP SounPhysBench in Section 3.3
and in Section 3.4 we perform case studies address important concerns of the main results.
3.1 EXPERIMENT SETUP
We evaluate the LLMs' Lean4 physies reasoning capabilities by applying them to write proofs for the PhysLib. Specifically, the task for the LLMs is to compose Lean4 proofs with provided NL statements and Lean4 statements. To ease the load of LLMs in proving, manually configure all the imports and namespaces. Furthermore, unless otherwise specified, we allow the LLM to use Long Chain-of of-Tuutght capability perform deeper reasoning. We apply the pass @ 16 metric to evaluate the performance.
To better demonstrate current LLMs' formal physical reasoning capability, we select the most rep- resentative closed-source and open-source models to evaluate. Namely, for closed-source general LLMs, we select GP (OpenAl et al.) 2024). Claude-Sonnets AAthhrpiic (2025), and Gemini- 2.5-Pro (Comanici et al. 2025) baselines. For open-source models, we present both the results of gegeral-purposs models, including DeepSeek-RI R1-522 (Guo et al. 2025) and Qwen3-8B (Team) 2025). as well expert Lean4 provers such Moodel-Proverr V2-8B (Lin et al.) (025b), Kimina- Prover WWan et al. 2025a), and SreeSeck-Prrveer V2 (Ren et al. 2025
Furthermore, to demonstrate the effectiveness of PhysLib, we test the LLM's capability under modes that have or do not have PhysLib in the generated context. summary, we test the LeanPhysBench conducted using the initial
eight major LLMs in two modes. We note that the experiments version of PbysLib and all reported results correspond to the initial version. Both the initial version and the updated version of PhysLib will be publicly released. The implementation details of experiments can be found in Appendix B
3.2 MAIN RESULT
We demonstrate our main experiment result in Table T The result demonstrates that LLMs that are larger in size and have better coding capabilities, such as Gemini and Claude, perform better in for- mal physics reasoning. With PhysLib in context, Gemini achieves a comparatively higher accuracy rate of 40.0% for the entire dataset, while Claude obtains 34.50%. In comparison, the expert provers

---

Published as a conference paper at ICLR 2026
Table 1: Pass@ 16 results of LeanPhysBench on 8 LLMs with (V) and without (X) PhysLib mode across different difficulty levels, including College, Competition-East (Comp-Easy) and Comp- Hard. All results are averaged over 3 runs. Best mean bolded, second-bes is underlined. Stan- dard deviation is shown unformatted.
Method
PhysL.bb
College
Comp-Easy
Comp-Hard
Overall
Open-source source models
6.09% 0.45%
8.60% + 0.76%
0.00%
0.00%
5.83% + 0.47%
DeepSeck-R1-88
2.56% 1.81%
5.91% + 0.76%
0.98% 1.39%
3.33% = 0.94%
6.41% + 0.91%
10.22% +: 1.52%
0.00%
0.00%
6.52% +: 0.81%
Qwen3-8B
2.58% 0.47%
3.23% = 0.00%
0.00% = 0.00%
2.35% = 0.25%
9.94% 0.91%
23.12% +: 1.52%
6.86% +: 1.3 1.39%
13,50% 1: 0.71% %
Kimina-Prover-8B
5.77% 0.00%
17.20% + 0.76%
5.88%
0.00%
9.33% + 0.24%
10.58% 1. 1.36%
26.34% 1 1.52%
5.88%
0.00%
14.67%
1.18%
Goedel-Prover-Ve V2-8B
6.09% 0.45%
19.35%
0.00%
4.90%
1.39%
10.00% 0.00%
DeepSeck-Prover-YV V2-7B
8.01% + 0.45%
31.18% + 1.52%
5.88%
0.00%
14.83% + 0.24%
6.09% 0.45%
22.58% 0.00%
5.88%
0.00%
11.17% 0.24%
Closed-source models
/
9.29% 1. 2.40%
30.11% 1. 2.01% %
0.00%
0.00%
14.17% 1 0.85%
GPT-4o
X
2.24% + 0.45%
4.30% + 2.01 %
0.00%
0.00%
2.50% + 0.41%
29.49% 1. 0.45%
61.83% 1 1.52%
0.00%
0.00%
34.50% 1 0.41%
Claude-Sonnet-4
X
3.21% + 1.63%
5.91% + 1.52%
0.00%
0.00%
3.50% + 1.22%
32.69% 1: 0.79%
74.19% 1: 1.32%
0.00%
0.00%
40.00% 1: 0.71%
Gemini-2.55pro
X
6.09% + 0.45%
11.29% + 1.32%
0.00%
0.00%
6.67% + 0.71%
and GPT-4o suffer from suboptimal performance with an overall accuracy rate of around 10%. Fur- thermore, the results demonstrate that with PhysLib added to the context, performance improved by 11.90% % and such improvement is consistent across all models and difficulty levels. indicates the effectiveness of our PhysLib in assisting LLMs' formal physics reasoning.
Upon closer examination, we can observe that Lean experts, which significantly outperform closed- source general LLMs in the math domain, lack the strong formal physics capabilities of these mod- els. This reveals that the expert Lean provers' capabilities are limited to the math domain and fail to transfer to other general domains, especially when these domains apply a new definition (such as the unit system in Lean4PHYS), Moreover, we found that the performance difference between expert provers is relatively marginal, indicating that significant improvement in mathematics does not guarantee large improvement in physics reasoning.
When analyzing the results from different levels of difficulty, we find that the models generally perform well on easy problems in competition problems. which are more closely aligned with math- ematical representations. However, expert models still not outperform larger closed-source mod- els, indicating the limited transfer of capability from math to physics formal reasoning in Lean4. Such finding is also true for college-level problems, where the performance of models is generally lower. However, for the competition-hart level of problems, the expert provers perform better than the closed-source models. This is because the expert models have a stronger capability to perform complex deduction, whereas large models do not.
Furthermore, adding PhysLib to the context will significantly improve the LLMs' performance. This because when adding the PhysLib, the model has better understanding of the formulation of the basic system we use to compose the proof. Without the PhysL.ib, the model can only perform basic simplification tactics like: const ructor, rw, abel, exact, aesop. By adding the PhysLib, the model can learn to perform more advanced tactics, such as simp and norm-num, based on the theorems and definitions in PhysLib.
3.3 PROBLEM FORMAT STUDY
This section presents a more detailed study of the problem format. Due to the space limit, we place the example in Figure in the Appendix and only provide the analysis result here.
7

---

Published as a conference paper at ICLR 2026
From the example of problem format, we observe that college-level statements primarily involve meric computations with a relatively wide range of physical quantities with units. These problems rarely require multi-step formula derivations, but heavily depend the unit system in PhysLib to ensure dimensional consistency. Thus, the models with weaker in-context learning perform rela- tively badly on this level of problems. This is because they cannot perform novel syntax adaptation or infer unit-handling rules from context.
The easy-level competition questions are closer transitional math problems in Lean, such as MiniF2F (Zheng et al. 202T). They involve relatively simple formula derivations, typically within two steps and often only tactics from Mathlib. Therefore, the models that are more familiar with the Lean mathematics and good at using tactics perform better than closed-source large models on these kinds of problems even without PhysT.b..
On the other hand, the hard level of competition problems demands complex symbolic reasoning, handling quantifiers, and difficult functional reasoning. For instance, this includes proving the ex- istence of a number, holding of an inequality, or deriving a functional relation. These problems combine unit casts with symbolic manipulation, further increasing the difficulty. Solving this level of problem requires careful decomposition of the problem, proving new lemmas, and diverse proof strategies with creativity. Moreover, many problems this level require calculus concepts such as limits and continuity. All the above factors combined cause the low pass rate at this level.
3.4
CASE STUDY
We present the case analysis in this section to provide a more detailed examination of the key find- ings from our main experiment. Due to the space limit, for a detailed example, please refer to Appendix E.2
Behavior of the same theorem with and without PhysLib Figure demonstrates Frnmontteee a theorem the college level, which Gemini can do both with and without PhysLib in context. From the comparison, we find that without the library, the proof is based solely on Mathlib. When the PhysLib is in the context, the proof tends to use the operations in the library and include explanatory comments. It indicates LhysLib can assist LLM's reasoning by providing a wider toolbox.
Transfer tricks in mathematics Figure 8 demonstrate problem only solved by Goedel-Prover- V2-8B in our entire cycle of experiment. We conclude that this is a good transfer of following the NL intermediate steps and performing multiple trials learned in the math Lean training. From the NL statement demonstrated in Figure 7 we can observe that most steps are presented in the statement. Following these NI. hints and many trials using try tactics, the Goedel-Provers solve the problem. indicates that, although limited, the expert prover's capability of Lean math reasoning can be applied formal physics reasoning.
successfully
Why the general model performs better To answer this question, we further analyze different topics solved by LLMs and find that general LLMs are typically better in thermo-dyne cermo-dynamies. The Gemini successfully proved 22 theorems in the field, but SaapSeek--rooee--e theorems. We present one theorem that proved by both Gemini-2.5 and DeepSeek-Prover--22 study the different behavior of their proof in Figure 6 We observe that the proof from the expert prover is more complex and tedious, while Gemini's ' proof is cleaner and more straightforward. Such difference in proving consistently shows between the expert prover and general models. It suggests that, in fields underrepresented in training, the prolonged deliberation of expert models may lead to overthinking and suboptimal performance.
only finished six Prover- to
4 RELATED WORK
4.1 FORMAL REASONING
Formal Language (FL) reasoning involves expressing mathematical statements a computer- verifiable manner. This approach mitigates ambiguity and provides a solid foundation for the rea- soning process. Researchers have developed many FLs in the last decades, such as Isabelle (Paul- son 1994), CoQ (Coq] 1996). Metamath (Megill & Wheeler 2019), and Lean (De Moura et al.
8

---

Published as a conference paper at ICLR 2026
Among these, Lean4 (Moura & Ullrich, 2021) receives significant attention from the field due to its extensive foundation library of Mathlib (mathlib Community 2020). A series of datasets and benchmarks has been developed to advance LLM Lean4 reasoning. For example, MiniF2F (Zheng et al. 2021) formalized competition- math problems across multiple proof lan- guages, ProofNet (Azerbayev al. 2023) increases the level of difficulty college-level, and Put- namBench (Gulati et al. (024) serves as college-level competition problems, with MATPBench (Hc) ct al. 2025b) taking a step further by extending formal proof into multi-modal reasoning. Mean- while, large-scale datasets have also been proposed to support LLM training, pushing the training data from 100k level (Wang et al., 2024a) to millions level (Lin et al., 2025a; Dong & Ma (025). At the same time, a series of Lean expert models are developed to perform formal math reasoning. representing works like DeepSeek- Proverr Family (Xin et al.] [0244] Ren et al. (2025). Theoreml.- lama (Wang et al., (024a), Goedel-Prover Family (Linn et al. 2025a b). LoT-SSlver (Wang et al.,
2013
2025c), Kimina-Prover (Wang et al. 2025a). BFS-Prover (Xin et al. (005), and GAR (Wang et al,,
2025d However, only few methods (Wang et al., 2025b Yao et al. 2025) tried to extend the
formal reasoning beyond verifiable languages to the natural domain.
4.2
LEAN IN SUBJECTS BEYOND MATHEMATICS
The application of Lean is gradually expanding from mathematics to a wider range of scientific fields, including chemical physics (Bobbin al. 2024), molecular simulation (Ugwuanyi et al. 2025), and electrical engineering (blacksph3re 2025). Some projects, such as [Tooby-mmith (2025), attempt to formalize mechanics and high-energy physics using tools such tensors and index nota- tion. However, most of these studies are still limited to a small-scale, non-modular level for specific theorems, and lack a standardized evaluation system. Although the Lean expert provers perform well on mathematical benchmarks, their ability to transfer their reasoning skills to other fields, such as physics, remains be examined.
4.3 PHYSICS DATASETS
In the field of physical reasoning research, the construction of data sets has long been a core is- sue. Physical problems have been extensively studied in the fields of natural language (NL) and machine learning, giving rise to several benchmarks that focus on physical understanding and rea- soning. For instance, PhysBench (Chow et al. (2225) and PHYBench (Qiu et al., (025) evaluate the physical reasoning ability of models; at the course level, UG-Physics (Xu et al. (025)) and
the PHYSICS dataset (Zheng et al.] 2025) provide thousands of textbook-style questions; at the competition level, OlympiadBenee
(He et al. 2024) includes 8,476 bilingual physics competition questions, HiPhO (Yu et al.) 2025) covers the recent international physics olympiad questions, and PhysReason (Zhang et al.] 2025) emphasizes the combination of multi-step reasoning and image understanding. Furthermore, CAMEL-Physics (Li et al.) (023) expanded the scale to tens of thou- sands of questions through automatic generation technology, providing a broader resource for model evaluation and training. Overall, these multi-level physical datasets laid the foundation for testing the physical reasoning ability of large language models under natural language conditions.
5 CONCLUSION
This paper presents Lean4PHYS, a comprehensive framework support Lean4 physics reasoning. The framework includes PhysLib, an extensible, community-driven foundation library that sets the cornerstone for units, fields, and theorems for formal physics reasoning. To evaluate LLMs' per- formance on formal physics reasoning, we propose LeanPhysBench, which is, to the best of our knowledge, the first benchmark for Lean4-based physies reasoning. Based on the Lean4PHYS, we conduct extensive experiments to provide an overview of LLMs' performance on such tasks and the effectiveness of our PhysLib. We find that expert provers do not outperform large general models in most cases of formal physics reasoning. It indicates limited transfer capability from mathematical reasoning, despite the fact that they are all Leand-based. Furthermore, the experiment shows that with Lhy in the context, LLMs' performance on LeanhhyBBench increases by 11.90% aver- age. Our work establishes a general principle for extending the formalization of physics and other natural sciences beyond mathematics into verifiable system.
9

---

Published as a conference paper at ICLR 2026
DISCUSSION & FUTURE WORK
Lean4PHYS, to the best of our knowledge, the first work focusing on LLM-bbase formal physics reasoning, paves the way for several promising directions for future studies. First, PhysLib grows, it may exceed the context length of current models. Thus, more sophisticated integration methods such as retrieval-augmented generation or tool-calling mechanisms will be necessary to select rele- vant theorems for the problem at hand. Second, since PhysLib is in its early stage with many fields and theorems yet to be implemented, developing autoformalization techniques convert existing physics knowledge into Lean4 format and integrate it into Phys/ib becomes vital. Third, our find- ings on limited cross-domain transfer suggest the need for unit-aware training strategies or adaptive reasoning techniques to bridge the gap between mathematical and physical formal reasoning. Fur- thermore, we acknowledge that the current benchmark primarily evaluates formal computation with physical units rather than deriving physical laws from first principles. Bridging this gap requires deeper integration between Lhy and efforts such as PhysLean (Tooby-Smith, (024). conclu- sion, Lean4PHYS opens up many promising future directions for Lean4 formal physies reasoning.
ACKNOWLEDGMENTS
We would like express gratitude Yifei Xia for her valuable assistance in figure plotting and helpful comments during the paper-writing process. We thank Wenyuan Wang for sharing his precious experience in the engineering aspects of formal verification. We also thank Peng Chen for generously providing original collections of high school physics problems, which served as valuable references during the design phase of Lean4PHYS.
10

---

Published as a conference paper at ICLR 2026
ETHICS STATEMENT
This work focuses on formalizing university physics problems in Lean4 and evaluating the formal physical reasoning capabilities of LLMs. To our knowledge, we strictly adhered the ethical guide- lines of the conference and considered the following aspects:
All the physics problems are derived from publicly available university text- books and competition problem collections. Appropriate citations have been provided, and no private or sensitive data has been used. In Lean LeanPhysBench, the college-level statements are formalized from the physics problems in the university textbook (Young Freedman, 2019) and the competition-leve statements formalized from the physics Olympiad practice book (Shu et al. 1999).
Data Sources:
Copyright Statement: Our work only utilizes limited portions of the original copy of Young & Freedman (2019); [hhu et al. (1999) for non-commercial research. Further- more, our approach involves referencing short excerpts with proper attribution, practice that does not substitute for original textbooks nor diminish their commercial value. As ad- vised by professional legal counsel, our method of extracting underlying physics logic and creating the Lean4 benchmark does not constitute infringement and requires explicit authorization. Nevertheless, we acknowledge that the interpretation of copyright law may vary across jurisdictions, and users of LeanPhysBench should use the benchmark in compli- ance with applicable laws. Twenty side-by-a side-by-side comparisons of our formalized statements and the source materials are provided as supplementary material.
Licensing and Attribution: The PhysLib is licensed with Apache- 2.0, of which parts come from Tao 2025) aligned with the origin repository. The BeanhhysBench is licensed with CC BY-NC 4.0,, aligned with the copyright protection range of the source materials. Addi- tionally, the LeanPhys may not be used to train, fine-tune, or evaluate any machine learning AI models, regardless of whether the is commercial non-commercial.
Responsible Use of LLMs: See A for details.
REPRODUCIBILITT STATEMENT
We have made efforts to ensure that our work is reproducible. The detailed description of the Lean4PHYS framework is presented Section with experiment details provided in Section and Appendices B D We will open source the code of Lean4PHYS, consisting of a community repository and benchmark, at prttps://eet
com Shi http../........lyyyooo///aaaaaaa

---

Published as a conference paper at ICLR 2026
REFERENCES
Anthropic. Claude sonnet 4, 2025. http://ts///...otoopp..oo.oooo/t
Accessed: 2025-09-23.
Zhangir Azerbayev. Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduatee-lvvl mathemat- ics. arXiv preprint arXiv:2302.12433, 2023.
blacksph3re. distribution factors: An attempt to formalize de loadflow equations and distribution factors in lean, 2025, URL
http://hhhhhhb.coooooooo//s/ssst factors Accessed: 2025-09-25.
Maxwell P Bobbin, Samiha Sharlin, Parivash Feyzishendi, An Hong Dang, Catherine M Wraback, and Tyler R Josephson. Formalizing chemical physics using the lean theorem prover. Digital Discovery, 3(2):264-283)) 280, 2024.
Wei Chow, Jiageng Mao, Boyi Li, Daniel Seita, Vitor Guizilini, and Yue Wang. Physbench: Bench- marking and enhancing vision-language models for physical world understanding, 2025. URL
Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Rejichiro Nakamo, Christopher Hesse, and John Schulman. Training verifiers solve math word problems. arXiv preprint arXiv:21 10.1110.444 14168, 2021.
Gheorghe Comanici, Eric Bieber, Mike Schaekermann, Ice Pasupat, Noveen Sachdeva, Inderjit Dhillon, Marcel Blistein, Ori Ram, Dan Zhang, Evan Rosen, et al. Gemini 2.5: Pushing the frontier with advanced reasoning, multimodality, long context, and next generation agentic capa- bilities. arXiv preprint arXiv:2507.06261 2025.
Projet Coq. The coq proof assistant-reference manual. INRIA Rocquencourt and ENS Lyon, version, 5, 1996.
Leonardo De Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In Automated Deduction- CArioo---ADD-55555 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25, pp- 378-388, Springer, 2015.
Kefan Dong and Tengyu Ma. Stp: Self-play IIm theorem provers with iterative conjecturing and proving, 2025. URL hhttps://axxiv.ortt
00212
Carl Edwards, Chi Han, Gawon Lee, Thao Nguyen, Bowen Jin, Chetan Kumar Prasad, Sara Szymkué, Bartosz A Grzybowski, Ying Diao, Jiawei Han, et al. melm: A function-infused and synthesis-friendly modular chemical language model. arXiv preprint arXiv:2505. 12565, 2025.
Aryan Gulati, Brando Miranda, Eric Chen, Emily Xia, Kai Fronsdal, Bruno de Moraes Dumont, and Sanmi Koyejo. Putnam-axiom: A functional and static benchmark for measuring higher level mathematical reasoning. In The 4th Workshop Mathematical Reasoning and Al at NeurlPS 24, 2024.
Daya Guo, Dejian Yang, Haowei Zhang, Junxiao Song, Ruoyu Zhang, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang, Xiao Bi, et al. Deepseek-rl: Incentivizing reasoning capability 1lms via reinforcement learning. arXiv preprint arXiv:2501. 2025.
John Harrison. Hol light: An overview. International Conference on Theorem Proving in Higher Order Logics, pp. 60 66. Springer, 2009.
Chaoqun He, Renjie Luo, Yuzhuo Bai, Shengding Hu, Zhen Leng Thai, Junhao Shen, Jinyi Hu, Xu Han, Yujie Huang, Yuxiang Zhang, al. Olympiadbench: A challenging benchmark for promoting agi with olympiad-level bilingual multimodal scientific problems. arXiv preprint arXiv:2402. 14008, 2024.
12

---

Published as a conference paper at ICLR 2026
Qi He, Cheng Qian, Xiusi Chen, Bingxiang He, Yi R. Fung, and Heng Ji. Veri-rl: Toward pre-
cise and faithful claim verification via online reinforcement learning, 2025a. URL https:
7/arxiv org. abs/ 22100/210..00 01932
Zhitao He, Zongwei Lyu, Dazhong Chen, Dadi Guo, and Yi R. Fung. Matp-bench: Can mllm be a good automated theorem prover for multimodal problems?, 2025b. URL https://arxiv.
org/abs/2500 2506. 06034
Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. Measuring mathematical problem solving with the math dataset. arXiv preprint arIiv:2103..mm 03874, 2021.
Guohao Li, Hasan Abed Al Kader Hammoud, Hani Itani, Dmitrii Khizbullin, and Bernard Ghanem. Camel: Communicative agents for "mind" exploration of large scale language model society, 2023.
Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, and Chi Jin. Goedel-prover: frontier model for open-source automated theorem proving, 2025a. URL
wtw.oorg/abbb//aoee 07640
Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, al. froeel--prveeryy Scaling formal theorem proving with scaffolded data synthesis and self-correction. arXiv preprint S.Kiv:2508.0361111 2025b.
The mathlib Community. The lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pp. 367-381, New York, NY, USA, 2020. Association for Computing Machinery. ISBN 9781 9781450370974. doi: 10.1145/
3372885.3373824. URL http::ttt://ettt org/ 1ee.e1114133331 3373822
Norman Megill and David A Wheeler. Metamath: computer language for mathematical proofs. Lulu. com, 2019.
Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In Automated Deduction-CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings 28, pp. 625-635. Springer, 2021.
David B Newell, Eite Tiesinga, et al. The international system of units (si). NIST Special Publica- fion, 330(1), 2019.
Aaron Hurst OpenAl, Adam Lerer, Adam P Goucher, Adam Perelman, Aditya Ramesh, Aidan Clark, AJ Ostrow, Akila Welihinda, Alan Hayes, Alcc Radford, et al. Gpt-40 system card. arXiv preprint arXiv:2410.21276, 1(2)3, 2024.
Lawrence C Paulson. Isabelle: A generic theorem prover. Springer, 1994.
Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning. arXiv preprint arXiv:2202.01344 01344, 2022.
Shi Qiu, Shaoyang Guo, Zhuo
Zhuo-Yang Yang Song, Yunbo Sun, Zeyu Cai, Jiashen Wei, Tianyu Luo, Yix- uan Yin, Haoxu Zhang, Yi Hu, Chenyang Wang, Chencheng Tang. Haoling Chang, Qi Liu, Ziheng Zhou, Tianyu Zhang, Jingtian Zhang, Zhangyi Liu, Minghao Li, Yuku Zhang, Boxuan Jing, Xianqi Yin. Yutong Ren, Zizhuo Fu, Jiaming Ji, Weike Wang, Xudong Tian, Anqi Lv, Laifu Man, Jianxiang Li, Feiyu Tao, Qihua Sun, Zhou Liang, Yushu Mu, Zhongxuan Li, Jing- Jun Zhang, Shutao Zhang, Xiaotian Li, Xingqi Xia, Jiawei Lin, Zheyu Shen, Jiahang Chen, Qi- uhao Xiong, Binran Wang, Fengyuan Wang, Ziyang Ni, Bohan Zhang, Fan Cui, Changkun Shao, Qing-Hong Cao, Ming xing Luo, Yaodong Yang. Muhan Zhang, and Hua Xing Zhu. Phybench: Holistic evaluation of physical perception and reasoning large language models, 2025. URL ht.tps://arxiv.ott
16074
ZZ Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, et al. Deepseek-provers Advancing formal mathematical rea- soning via reinforcement learning for subgoal decomposition. arXiv preprint arXiv:2504.2880, 2025.
13

---

Published as a conference paper at ICLR 2026
Tanik Saikh, Tirthankar Ghosal, Amish Mittal, Asif Ekbal, and Pushpak Bhattacharyya. Scienceqa: A novel resource for question answering on scholarly articles. International Journal on Digital Libraries, 23(3):289-300 2022.
Yousheng Shu, Wangyu Hu, and Bingqian Chen. Selected Advanced Physics Problems, Volume II. Higher Education Press, Beijing, 1999. ISBN 7040069997.
Zhaochen Su, Peng Xia, Hangyu Guo, Zhenhua Liu, Yan Ma, Xiaoye Qu, Jiaqi Liu, Yanshu Li, Kaide Zeng, Zhengyuan Yang. Linjie Li. Yu Cheng, Heng Ji, Junxian He, and Yi R. Fung. Think- ing with images for multimodal reasoning: Foundations, methods, and future frontiers, 2025.
URL httph:://txxiiiieee org/ absa 2506. 23918
Mirac Suzgun, Nathan Scales, Nathanael Schärli, Sebastian Gehrmann, Yi Tay, Hyung Won Chung, Aakanksha Chowdhery, Quoc V Le, Ed H Chi, Denny Zhou, et al. Challenging big-bench tasks and whether thain-of-thought can solve them. arXiv preprint arXiv:2210.09261, 2022.
Alon Talmor, Jonathan Herzig, Nicholas Lourie, and Jonathan Berant. Commonsenseqar A question answering challenge targeting commonsense knowledge. arXiv preprint
2018. Terence Tao. A lean companion to analysis ltttp:://gtthbb. httpa///tttttttt//aayi..... 2025. URL
http:/uuww.cocm/ttttt///aaaaaaaa GitHub repository, accessed:
2025-08-31.
Qwen Team. Qwen3, April 2025.
Joseph Tooby-Smith. Formalization of physics index notation in lean 4. arXiv preprint arXiv:2411.07667, 2024.
Joseph Tooby-Smith. Heplean: Digitalising high energy physics. Computer Physics Communica- tions, 308:109457, 2025.
Ejike D Ugwuanyi, Colin T Jones, John Velkey, and Tyler R Josephson. Benchmarking energy calculations using formal proofs. Molecular Physics, pp. e2539421, 2025.
Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung. Marina Vinyes, Zhenzhe Ying, Zekai Zhu, et al. Kimina-prover preview: Towards large formal reasoning models with reinforcement learning. arXiv preprint arXiv:2504.11355 2025a.
Ruida Wang, Jipeng Zhang, Yizhen Jia, Rui Pan, Shizhe Diao, Renjie Pi, and Tong Zhang. Theorem- Ilama: Transforming general- pprrro- Ilms into lean4 experts. arXiv preprint arXiv:2407.03203, 2024a.
Ruida Wang, Yuxin Li, Yi R Fung, and Tong Zhang. Let's reason formally: Natural-formal hybrid reasoning enhances Ilm's math capability. arXiv preprint arXiv:2505.23703, 2025b.
Ruida Wang, Rui Pan, Yuxin Li, Jipeng Zhang, Yizhen Jia, Shizhe Diao, Renjie Pi, Junjie Hu, and Tong Zhang. Ma-lot: Model-collaboration lean-based long chain-of-thought reasoning enhances formal theorem proving. arXiv preprint wxXi:2503.003205 2025c.
Ruida Wang, Jiarui Yao, Rui Pan, Shizhe Diao, and Tong Zhang. Gar: Generative adversarial reinforcement learning for formal theorem proving. arXiv preprint arXiv:2510. 1769, 2025d.
Yubo Wang, Xueguang Ma, Ge Zhang, Yuansheng Ni, Abhranil Chandra, Shiguang Guo, Weiming Ren, Aaran Arulraj, Xuan He, Jiang, et al. Mmlu-pro: pro: A more robust and challenging multi- task language understanding benchmark. Advances Neural Information Processing Systems, 011992666952990 2024b.
Huajian Xin, 7Z Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang. Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, et al. Deepseek-provert prover-vl. 5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. arXiv preprint vrXivv2408.08755 2024.
Ran Xin, Chenguang Xi, Jie Yang, Feng Chen, Hang Wu, Xia Xiao, Yifan Sun, Shen Zheng, and Kai Shen. Bfs-prover, Scalable best-first tree search for I1m- based automatic theorem proving. arXiv preprint arXiv:2502.0m 254300388, 2025.
14

---

Published as a conference paper at ICLR 2026
Xin Xu, Qiyun Xu, Tong Xiao, Tianhao Chen, Yuchen Yan, Jiaxin Zhang, Shizhe Diao, Can Yang, and Yang Wang. Ugphysics: A comprehensive benchmark for undergraduate physics reasoning with large language models. arXiv preprint arX1v:2502.0033: 2025.
Jiarui Yao, Ruida Wang, and Tong Zhang. Fans-formal answer selection for natural language math reasoning using lean4, arXiv preprint urXiv:2503.03255: 2025.
Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen. Lean workbook: A large-scale lean problem set formalized from natural language math problems. arXiv preprint arXiv:2406.03844 2024.
Hugh D. Young and Roger A. Freedman. University Physics with Modern Physics, Global Edition. Pearson Education, 15th edition, 2019. ISBN 9781292314815.
Fangehen Yu, Haiyuan Wan, Qianjia Cheng, Yuchen Zhang, Jiacheng Chen, Fujun Han, Yulun Wu, Junchi Yao, Ruilizhen Hu, Ning Ding, al. Hipho: How far (m) Ilms from humans in the latest high school physics olympiad benchmark? arXiv preprint 250.v22500.07894, 2025.
Xinyu Zhang, Yuxuan Dong, Yanrui Wu, Jiaxing Huang, Chengyou Jia, Basura Fernando, Mike Zheng Shou, Lingling Zhang, and Jun Liu. Physreason: A comprehensive benchmark towards physics-based reasoning, 2025. URL
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. Minif2f: systemm benchmark for formal olympiad-level mathematics. arXiv preprint arXiv:2 10, 2021.
Shenghe Zheng, Qianjia Cheng, Junchi Yao, Mengsong Wu, Haonan He, Ning Ding, Yu Cheng, Shuyue Hu, Lei Bai, Dongzhan Zhou et al. Scaling physical reasoning with the physics dataset. arXiv preprint arXiv:2506.00022, 2025.
15

---

Published as a conference paper at ICLR 2026
A
USE OF LLMS
LLMs are used to assist in the development and verification of physics problems. Specifically, they generate detailed step-by-step solutions to help annotators better understand the reasoning process and calculation steps of the problems, as well as check the correctness and completeness of natural language answers. However, all the outputs were subsequently reviewed and verified by human annotators to ensure accuracy and reliability. Furthermore, LLMs are also utilized to enhance the clarity and readability of the manuscripts, including correcting grammar and sentence structures, as well as maintaining the consistency of chart titles with the layout of the tables.
B IMPLEMENTATION DETAIL
The generation configuration for the LLM roll-out of the experiment is as follows:
Top-p: 0.95
Temperature: 0.8
Maximum tokens per generation: 16,384
Repetition penalty: 1.0
Open-source models are tested under 4-card H20 server. The entire open-source LLM roll-out process costs about 2 days. After the release of our initial draft, we found that two problems in Hard"" problems have unintended trivial shorteuts. We have fixed the problems ensure the correctness of our benchmark. It caused the updated main experiment results in Section 3.2 differ from those in initial draft.
C COMPARISON WITH PHYSLEAN (TOOBY-SMITH, 2024
This section aims to provide an explicit comparison between Lean4PHYS and PhysLean Tooby- Smith (2024), works that all aim to formalize physics reasoning in Lean4. We regard two works as highly complementary efforts of different perspectives and domains.
In the initial development stage of Lean4PHYS, we tried to formalize the problems based on the PhysLean repository. However, such initial attempts failed. This is because PhysLean excels formalizing advanced theoretical physics (e.g.. high-energy physics, quantum field theory) with so- phisticated mathematical structures, such fiber bundles and index notation. This design naturally differs from our target of developing Lean4PHYS, which focuses on foundational, college-level physics reasoning with an emphasis on creating general- purpose infrastructure and benchmark for LLM evaluation. The key distinction is that Lean4PHYS aims to establish foundation for automated reasoning by LLMs, while PhysLean focuses on expert-driven formalization of advanced theories. In summary, we acknowledge the efforts of PhyslLean (Tooby-Smith) (024) in pioneer- ing physics formalization Lean4, while highlighting the unique role of Lean4PHYS in bridging physics formalization with LLM-based automated reasoning in formal physics of Lean4.
16

---

Published as a conference paper at ICLR 2026
D LLM PROMPT TEMPLATES
We provide the prompt templates used to guide LLMs in generating Lean4 proofs.
With PhysLib:
Please first learn the new library besides mathlib and usage examples before answering the question. You should refer to the new unit system.
[PhysLib)
Complete the following Lean code.
Provide your response in two parts, each enclosed in separate
4 markdown code blocks:
'plan
Prroff Plan
Outline the main proof steps and strategies.
Highlight key intermediate lemmas and structures.
Describe how to connect them to form the final proof.
... "lean4 _
--- NNL s -/
iiean_stttteeent
Without PhysLib:
Complete the following Lean code.
Provide your response in two parts, each enclosed in separate
4 markdown code blocks:
'pplan
Proof Plan
Outline the main proof steps and strategles.
Highlight key intermediate lemmas and structures.
Describe how to connect them to form the final proof.
"leenn [Lean4_header)
/-- statement -/
[eean_statteentt)
17

---

Published as a conference paper at ICLR 2026
E EXPERIMENT
E
FORMAT STUDY
This appendix, based on the example shown in Figure provides more detailed analysis of the problem format described in Section 3.3 with a particular focus on the characteristics of the ques- tions themselves.
Taking a college-level problem as an example, the upper left part of Figure shows force calcu- lation problem involving two point charges on the x-axis. This problem involves various physical quantities, including charges, distances, and forces, and explicitly uses SI units such as nanocoulomb and m. The problem mainly relies on numerical calculations, and the magnitude of the force can be computed directly using Coulomb's 's law, with almost need for multiple-step formula derivations. However, due to the potential for dimensional issues when combining different physical quantities in calculations, the solution to this problem requires maintaining unit consistency, which underscores the importance of the unit system in PhysLib for formal calculations. Such problems are typical of the "formula application type" and suitable for verifying the model's ability in basic numerical reasoning and unit handling.
For the simple problem of the competition (Competition-Fasy) the problem of the parallel plate capacitor shown in the lower left corner of Figure 4 is typical example. The core formula of the problem is C q/V and only one or two steps of substitution are required for the calculation. The problem provides values for charge, voltage, and plate spacing and requires sequential substitution into the formula complete the solution. Therefore, it involves combining numbers and symbols. This type of problem belongs to the "transitional derivation problem", similar to the intermediate math problems Lean's 's MiniF2F, mainly testing the model's 's ability to perform algebraic operations and to substitute formulas. Compared to college-level problems, it has slightly increased logical reasoning requirements.
And the competition-hant problems CoameettioonHHadd)) such the pulley law problem shown in the right column Figure 4 significantly increase the difficulty. The problem involves contin- uous function of tension varying with angle and requires deriving the final result by integration or logarithmic relationships. Besides the multi-step formula derivation, the problem also involves relationships and function expressions among multiple physical quantities, requiring an understand- ing of the dependencies and combination rules among the model's symbols. Solving such issues not only requires multi-step logical analysis but also involves function operations and advanced symbolic reasoning, which are typically highly difficult, and testing the model's 's ad advanced physical reasoning ability.
18

---

Published as a conference paper at ICLR 2026
College
Competition-Ilard
point charges ace located of coordinate system: ql - 1.0 nC 1s
Capstan
zope confficient of felction wraps tuzna (8_cotal 2an) around post, the tenaton ratioo between the heavy side and the light side satisfies
+2.C
-3.0 15
x -4.0 cm. Nhat is the total
q1 and 92 theoren: #lectremagnetistt 3eaeetiism__uiiveeeeeeee
electric force exested
(2
charge
5.0 University
10g assuming > m and P
[q] q² q3 : charge) (x] x2
Tangthh)
(hgl qi $I.3ano (1 cculcmb))
theoren Ch2_01 (M Kass)
(hg2 q2 $1.J0no (-3 coulomb)
thg3
SI,aano (5 coulomb))
(j : R)
((0.02:R) moter);
(n R)
thx? x² (10.04:R) meter))
(0_toral : R
Real.pl
(hx
(2 2orce)
R + Pozce)
(LE : T- q3 (ql (xl x3) "
(h_ 0 M.va. A m.val A D
e2 (x2 x3)"211 1-22:Q1/32) nonton ((9:R) (10:R) by simp mp [+Scalaar lar.val inn, hF, hql, hq?
(XK_E__ M.val a.val)
(T (I_light_def TT0-0 g)
(T_heavy_def (copstan caapssn_diiferentii.
l_total
V R, deriv
hg3, Exl,, 1x2, Ex3, X, SI.nano, coulamb, netes, newton] norm_num
(fun 0' (I (').val) - IT }.val)
(capstan : Real.log ((T 8 1I val) # (_iotal) (theta_def 8_ootal - Real.pi n
[otel)
Competition-Faay
/ Rea Real.pt m.val)
()) Real.
The platea of a parallel-plate capacitor are 2.50 nm apart, and each carrias The plates are in vacuun. The electric the plates magn' tude of (44.00 Vtimes what is the
reases popos with (hM, hm, hmu) seal.log [(T d_iotal). (T
chazge magnitude
0) vaal)
Real.log (() g).vel im
field
vvvl) := is rM (T_haavy_dos, [Liight_def]]
10" (6) (text(V/=))
have h2
1og (MM g) veil Real.log IM.val vaval) by
capacitance?
theoren, thl3 wtw.ellloooeeettioo....oooo. 8
have h3 (M g) vaal / im gt vval M.val m.vai :- by
(ivoltage) IC:Scaler
capacitance_ _nntt) (q:Charge)
riele_aimpr sing_nf; simps ring [h3]
(#:Scalar
"toree_untt-charge.uu
(d: Length)
have h3 Real.log (M.val / m.vol) = linsrith
(h: sspasttacee_uitt-charrg....o
ttotll ceapsten_integrel
voltage_unit)
hi, 42]
(bC:0=19/V) cast h) (2g:g=S2.nano 180
have h4 : seal. seal.lop log (M.val m.val)
(2 seal.pi n)
[theta_def]
(NV:V-B-d) (hE:B= 1416::R) Standarothit
at h3; Linerith
mhdrd-SI.ailli (12.5:R). meter!):
have a5 F have h6 Real.pi $
by linerith
C- / 125000003000:QQ) StandardUni:
have h7 seal. (M.val / m.val)
Resl.pi_ne_zer
== by have hC_expanded [he, hv]
te/ (Evd) (.dd).eaae reatt
have h8
Real.pi (Real. (M.val m.vol))
linarith [bd]
[hc_expanded, hg, h5, hd]
12 Resl.pi #² s by sield linarith rw [h8]; rieid_simgr ring field_simp; ring
simp [nanc, milli, coulamb, meter, + Scelar.va:_int norm_num
Figure 4: Three sampled physics questions from College Textbook, Competition-Fan Competition- Hard problems. Each example shows the natural language problem statement followed by its corre- sponding Lean formalization with verified proof.
19

---

Published as a conference paper at ICLR 2026
E.2 CASE STUDY
Behavior of the same theorem with and without PhysLib Sillutailllsstrtees the different proof strategies employed by Gemini-2.5-pro when solving the same college-level mechanics problem, with and without Pby Without Physt the proof is relatively concise and almost entirely re- lies on the assumptions ha and hT'. For the accelcration a, the proof is completed by substituting the assumption into [ha] and then using basic simplification and mullippiication/dvviiion commuta- tive laws (s imp and mul-diiv.... www.grtgt.coo.o... to transform the algebraic expression. This indicates that in the absence of domain-specifer libraries, LLM relies the general tacties of Mathlib to gen- erate proofs, which are rather mechanical but can still accomplish the task correctly. When PhysLib is introduced, the proof becomes more structured and systematic. After substituting the assump- tion the proof utilizes the Scalar, val-inn lemma from PhysLib to transform the goal into an equation in the underlying real numbers, enabling LLM to handle algebraic operations of physical quantities more directly. Subsequently, the proof is completed by applying simplification (simp) and ring tactics to prove the algebraic identity. Overall, the proof with Phystib demonstrates a richer use of tools and more robust reasoning path.
Transfer tricks in mathematics During the process of solving the problem depicted in Figure and Figure Prever demonstrated a variety of systematic proof strategies, which originated from its accumulated experience in mathematical Lean problems and were successfully transferred to formal proof' in physics. Firstly, the Prover would break down the overall proof goal into multiple sub- uub-goals, such as proving μe 0.46 first, then proving 14 0.40, and finally combining them into a logical conjunction (p, = 0.46) A (F& = 0.40). This sub-goal decomposition strategy enables the Prover to handle complex problems step by step, with each sub-goal being independently verifiable and provable, thereby enhancing the reliability and success rate of automated proofs. This strategy is directly borrowed from the experience of handling complex theorems in mathematical Lean.
Within each sub-goal, the Prover will conduct a step-by-step verification of intermediate arith- metic or type values. For instance, it will first verify that Scal ar. . vaal f_s_max 230, then 500, and subsequently calculate (n, R) 0.46 based on these intermedi- ate results. This step-by-ster verification method ensures that each stage is correct and error-free, preventing
Scalar, val
accumulation and forming reliable proof chain, which is exactly the same as the step-by-step verification of sub-conclusions in the Lean mathematical problems. When dealing with auxiliary steps such type conversion or arithmetic simplification, Prover employs multiple attempts strategy, such as using try field.sing at or try norm-cast at *. These lightweight strategies enable Prover to automatically handle potential obstacles without requiring in-depth domain knowledge. The effectiveness of this strategy also stems from the experience of handling auxiliary steps through different tacties in Lean problems, achieving cross-domain trans- fer.
Finally, after completing the proofs of each sub-goal, the Prover uses the logical constructor to inte- grate the results, such as exact <h4, h7>, combining the proofs of each sub-goal into an overall theorem. This method typical approach in mathematical Lean proofs and also applicable in physical formalization problems, demonstrating the universality of the proof strategy and its ability for cross-disciplinary transfer.
Why the general model performs better We analyzed the proof style depicted in Figure 6 to ex- plain why general-purpose models (such as Gemini-2.5-pro) can outperform expert theorem provers in under-trained domains. The theorem Ch1 0ut.ustuutttteeeeeeeee ion_4 discussed involves calculating the thermodynamic index & based on the known pressures Pı, P2. volumes V/1 V2. and temperatures Ti, T2. Although both SpepSeek-Prover- V2 and -emmini-2.5-pmo can complete the proof, their proof methods differ significantly. DeepSeek-Provers
generates a highly step-by-step proof, gradually substituting and simplifying, explicitly introducing auxiliary steps such as hy and fiz, and repeat- edly invoking simplification strategies for intermediate calculations; while Gemini-2.5-pm generates concise proof by directly using all the assumptions once and leveraging advanced simplification strategies to directly reduce the target to a numerical equation, omitting the lengthy intermediate steps.
From the perspective of the complexity of the steps, the proof of DeepSeek-Prow -eroverr-P- V2 involves over twenty nested operations, while Gemini-2.5-pp can complete the proof through only two main
20

---

Published as a conference paper at ICLR 2026
strategies. This indicates that although expert proofers ensure the rigor of the form, in this type of domain that mainly relies on numerical calculations and has less symbolic reasoning, their step- by-step operations appear cumbersome and lengthy. Further analysis reveals that DeepSeek-Prover- V2 adopts fine-grained approach, explicitly handling each substitution and simplification, while Gemini-2.5-pro conducts reasoning higher abstract level and uses the built-in simplification rules in the system to quickly complete the proof. In thermodynamic problems, higher-level abstraction can reduce unnecessary complex calculations and improve efficiency.
Furthermore, the expert prover mainly focuses on pure mathematical theorems during training. Therefore, in application fields such thermodynamics, it is prone to introduce additional inter- mediate steps. This "overthinking" ensures rigor but may result in lengthy proofs and even increase the risk of errors complex substitutions. In contrast, general large models possess flexible reason- ing capabilittes and can efficiently combine simplification rules with numerical calculations. In this case, Gemini-2.5- 2.5-pro successfully mapped all hypotheses numerical verification through a single immp call, demonstrating its adaptability to training deficiencies.
21

---

Published as a conference paper at ICLR 2026
Gemini-2.5-pro without PhysLib
theorem Mechanics 73 University
Force) (m_1 m_2 Mass) (a : Acceleration)
(ha : = 2 q / (m m
(hT T (m] * 2) / (m_ m_ * gg):
(a (m_ (m_1 mL21) AAT A (m_1 m2 / (m_1 m2) ;
by constructor
rw [ha]
ext simp [mi1_div_right_oo
exact hT
Gemini-2.5 2.5-pro with PhysLib
theoren. Mechanics_ 2______7__niiisstty
(T Force) (m_1 m_2 Mass) (a : Acceleration)
(ha m_2
(m_ m_2))
(hT T [m_ * m_ / (m_ m_ :g):
(a 2m / (m 21) g (m1 2) (m_1 1 2) g) =
by constructor
The first goal is prove the rearranged expression for acceleration 'a'. -- We start by substituting 'a' with its given definition from hypothesis 'ha', [ha]
The goal is 'Sealar' expressions,
prove algebraic equivalence between
We use the "Scalar.val_ Temma to transform this into an equality of their
underiying real values. This is a standard technique in the Physlib library.
simp only [+ Scalar, val_ivallnjn
Now, with the goal being an equality real numbers, we can use "sime" to apply
- the library's 's rules for how v.val' distributes over arithmetic operations.
simp
The resulting goal 2m.2.vl g.val / (m_ val 2.2.vll) m_2.val / lavl.al + m_2.va1) * g. val.
-- This is a standard algebraic identity which the "ring" tactic can solve.
ring
The second goal prove the expression for tension 'T which identical to the hypothesis 'hT'.
exact hT
Figure 5: Two examples from LeanPhysBench demonstrating different proofs of the same college- level problem, generated by Gemini-2.5-pro with and without PhysLib.
22

---

Published as a conference paper at ICLR 2026
DeepSeek-Prover--V.
theorem. Ch10 question__
P2:Pressure) (V1 v2:Volume)
T2: Temperatur)) (k:R)
(hV1:V1= 13. StandardUnit _
(1. :R) kelvin)
kelvin)
(BP1:22=((1.0)110"":::)) pascal)
(hP2:P2= 868 pascal)
IaV2:V2-V1.12+P111TT. (TL=22)) (TIxP2))
(bk:k=Real. (V2/V1) .vll (I1)
X-Real.rpox (10832250 / 144739) (1 / 3) :- by
have h_main
Real. rpow (10832250 / 144739) (1 3) by
have h [hi]
Real.Ipow
vi).val ((1
R) by [bk]
have h2 : (V2 vl).val (10832250 144739 : R) : by -- Simplify the expression for V2 / V1
simp all [Pressure, Volume, Temperature, add assoc, add_comm, add_lefttcomm mul_assoc, mul_comm, mul_left_commn,
div div_eg_mul_iny, mul_iny_cance__lef,
<;> ring_nf at <;> norm_num at
<;> sild_ssmpp (StandardUnit, mul_assoc, mul_comm,
mul_left_come at
<;> ring
<,> norm num num at
<;> nlinarith
rw [h2]
<,> simp [Real. [
<;> norm_num
<;> ring_nf
<;> norm_ num
<;> field_simp
</> ring_nf
norm_num
<;> nlinarith
exact h main
2.5-pi-2.5-pro
theorem Ch10_question__
(P1 P2:Pressure) (V1 V2:Volume) (I1 12:Temperature) (k:R)
[hvl:vl= 13- Standardunit kelvin)
(hTI:TI- (11.11710((1.11115773...1.. :R) keivin)
(11::P1-(11.001111"))1.1 pascal)
(hP2:P2- 868 pascal)
nV2.12--11-22211(11.222
(kk:k-Real.rpow (V2/V1) ((1/3) :R)): k-Real. (10832250 / 144739) (1 / 3) := by
Use all hypotheses to substitute the variabies and simplify the expression.
"simp" will use "hk" substitute "K,, "hV2" substitute 'V2', and the other hypotheses to substitute the numerical values. The "0[simp]" lemmas in the UnitsSystem library will handle the v.val" operations.
simp [hk, EV2, hV1, hT1, hT2, hP1, hP2]
The goal is verify it.
purely numerical equality, Use 'norm_num" to
norm_num
Figure 6: Comparison of Proof Styles by DeepSeek-Prover- V2 and Gemini-2.55ppm
23

---

Published as a conference paper at ICLR 2026
Goedel-Prover with PhysLib (nature statement)
Question 74: You want move 500 N crate across level floor. To start the crate moving, you have to pull with 230 N horizontal force. Once the crate starts to move, you can keep it moving constant velocity with only 200 N. What are the coefficients of static and kinetic friction? Follow the process: Just before the crate starts to move, we have:
FF.IT+ (- mmxx) so (fe)max T 230
Σ Fn (-w)
so
500 N
Now we solve (fa)max Mg, for the value of ue:
(fx)
230 N
Ps
= 0.46
500 N
After the crate starts to move, we have:
=== 0 so f:. = T = 200 N
FF, (-w) = so 12 W 500 N
Using f& 14,,, find:
fk
200 N
0.40
500 N
show that the coefficients static is μss 0.46 and kinetic friction is l 0.40.
Figure Natural Language Statement of Problem Solved Exclusively by Goedel-Prover.
24

---

Published as a conference paper at ICLR 2026
Goedel-Prover with PhysLib (Lean4 statement)
theorem Mechanics 74 University_0
(f_s_max f_k w Force) I/L MLk (hw = 500 newton)
Q)
(hn w)
(hf_s_max f_s_max 230 newton)
(hf_k f_k -200 newton)
(hp_3 p_s Scalar.val val f_s_max / Scalar.val n)
(hyCk p.k Scalar. __k Scalar.val n)
(p_s (0.46 Q) A p.k (0.40 Q)) == by
have : scalar.val f_s_max 230 by rw [hf_s_max] simp [Scalar. val smul, nexton]
have h2 Scalar.val
500 by have h2 : 500 nexton by rw [hn, hw]
IW [h21] simp [Scalar. val val__mul, newton]
have h3 (p R (0.46 R) by
have h31 : (p R) Scalar, val f max / Scalar, val := by horm_cast at hyss zw [h31]
[hl, h2] nerm_cum
have : 1_3 (0.46 Q :- by
have h41 : (p_.5 : R) = (0.46
R) := h3
nom at h41 T
nerm_num
(try field simp at x)
(try cast at *)
have h5 Scalar. val f_k 200 : by [hf_ simp [Scalar, val smul, newton]
have h6 : (p_k k : R) (0.40 : R) :- by
have h61 : (p_k : R)
Scalar.val f_k / Scalar, : by
horm_cast at huck + [h61]
[h5, h2]
nerm rum
have h7 nLk (0.43 ( :- by
have h7: ( k R) = (0.40 R) h6
norm_rum h71 |-
(try field_simp at x)
(try norm_cast at +)
have h8 (n_s (0.46 : ()) A p (0.40 (1) : by
exact (24, h7)
exact h8
end Mechanics
Figure 8: Lean4 Formalization and Proof of the Problem Shown in Figure 7 by Goedel-Provee
25


Reviews:
[{"review_id": "C5VFMjlGNr", "reviewer": "Reviewer_6F2Q", "summary": "The paper introduces Lean4PHYS, which is a Lean4-based framework for formal physics. Lean4PHYS includes PhysLib (a repository of a physics unit system and commonly used theorems) and LeanPhysBench (a benchmark of 200 hand-crafted theorems from high school competitions to elementary college level).", "questions": "- Did the authors attempt to compare the accuracy of the models in this Lean 4-based setup vs natural setup (i.e., asking the model the question in natural language)?\n    - This would be important to check if the bottleneck is in the physics understanding or in the Lean 4 code understanding\n- I would expect PhysLib to be used by the model in a tool-calling fashion such that we do not need to present all the available concepts to the model in the context window. Is that the case?\n- L377-379: “models with weaker in-context learning perform reatively badly on this level of problems. It is because they cannot infer the new out-of-distribution syntax or unit-handling rules from context.” → This seems to be an overclaiming since none of the experiments are checking the in-context capabilities. Not to mention, we cannot confidently say that this data is OOD because we do not have access to the pretraining data of the models. Am I understanding the sentence properly?", "limitations": "", "rating": 2, "confidence": 3, "soundness": 2, "presentation": 2, "contribution": 3, "strengths": "The first framework for physics problems in Lean4 for LLM. This may be of significant interest to the community that studies LLM applications to physics. The PhysLib library and LeanPhysBench test dataset can be a useful artefact for future studies.", "weaknesses": "- Copyright infringement.\n    - **Due to this issue, I decide to assign a very low score to the paper albeit the important contribution. However, I am very open to changing my score once this issue is clarified/addressed.**\n    - The authors mentioned that “rather than copying the questions verbatim, we reformulated and rephrased them based on the underlying physics ideas\", however, I am not certain that this is sufficient. The key issue hinges on \"substantial similarity\" and whether the original work's creative expression has been copied, even in a modified form. Given that the underlying physics idea of the questions are copied (perhaps to the point that there exists a one-to-one mapping between the textbooks and the dataset questions), this seems to constitute substantial similarity. The authors may need to ask for **explicit permission** from the publishers.\n- Statistical robustness\n    - Given that the evaluations were done with non-zero temperature, the authors should report the stochasticity of the results (e.g., standard error).\n- Lack of implementation elaboration\n    - How do the authors present PhysLib to the model? Would it fit into the context window?\n    - For non-experts, it is challenging to understand what the task looks like, particularly because the prompt asks the model to “complete the following Lean4 code” instead of the commonly known question-answering setup.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "HPaYTuYLd2", "reviewer": "Reviewer_SHVy", "summary": "This paper introduces a comprehensive framework named Lean4PHYS, designed for formal reasoning on university-level physics problems using the Lean4 proof assistant. The framework consists of two core components: PhysLib, a community-driven library that provides a foundational unit system and commonly used theorems for formal physics reasoning; and LeanPhysBench, a benchmark dataset of 200 problems manually constructed and formalized from university textbooks and physics competitions. Based on this framework, the authors evaluate the performance of several mainstream large language models (including both general-purpose models and those specialized in Lean mathematical proofs). The experimental results show that general-purpose LLMs generally outperform math-specialized models on physics reasoning tasks, revealing a potential overfitting issue of the latter to the mathematics domain. Furthermore, the study demonstrates that using PhysLib as contextual information significantly improves the performance of all tested models.", "questions": "1.  The experimental results indicate that providing PhysLib as context to the models significantly improves their performance. Given that PhysLib, as a foundational library, could be quite large, the paper seems to lack a specific description of how it was effectively integrated into the model's prompt context window. Did the authors provide the entire library's content, or was some form of retrieval mechanism used to select relevant theorems and definitions? Clarifying this implementation detail is crucial for the reproducibility and understanding of the results.", "limitations": "", "rating": 8, "confidence": 3, "soundness": 3, "presentation": 4, "contribution": 3, "strengths": "*   **Significant Contribution to the Research Community:** This paper contributes two extremely valuable resources: **PhysLib**, a modular and extensible foundational library for physics, and **LeanPhysBench**, the first benchmark dedicated to evaluating formal reasoning capabilities in physics. These two achievements provide a solid infrastructure and a fair evaluation standard for subsequent researchers to enter and work in this field, which will undoubtedly promote the development of the entire community.\n*   **Exhaustive Experiments and Deep Insights:** The paper's experimental design is very comprehensive, not only testing multiple top-tier general-purpose LLMs but also comparing them with several Lean-specialized models that excel in mathematics. The results reveal an important finding that \"specialized models have limited cross-domain (from math to physics) generalization ability,\" prompting deep reflection on model generalization and domain overfitting. At the same time, the experiments clearly quantify the effectiveness of the PhysLib library in assisting models with physics reasoning, proving its design value.", "weaknesses": "*   **Insufficient Discussion of Related Work:** The \"Related Work\" section mentions Lean's application in physics and other non-mathematical fields but fails to deeply discuss the differences and connections with some directly related works. For example, the paper mentions the `PhysLean` [Tooby-Smith & contributors (2024)] project but only briefly describes it as \"theorem-specific, small-scale, and non-modular.\" Considering that `PhysLean` also aims to formalize physics in Lean4, the authors should have elaborated more on the fundamental differences and specific advantages of Lean4PHYS in terms of design philosophy, implementation methods (such as the construction of the unit system), coverage, and modular design compared to `PhysLean`. Adding such in-depth comparative analysis would better highlight the uniqueness and irreplaceable contribution of this work.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "HE7KZlDAN2", "reviewer": "Reviewer_VJbK", "summary": "This paper presents Lean4PHYS, a Lean4-based framework for formalizing college-level physics problems.   It includes PhysLib, a modular library with a systematic unit system and reusable theorems, and LeanPhysBench, a benchmark of 200 formalized physics problems.   The authors propose a pipeline to convert natural language physics questions into Lean4 proofs.   Experiments compare Lean-oriented provers with general-purpose LLMs on LeanPhysBench.   Results show LLMs outperform provers, with improved performance around 40.5% accuracy when using PhysLib context, highlighting the need for domain-specific knowledge in formal reasoning.", "questions": "see Weaknesses", "limitations": "", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "- The paper pioneers formal physics reasoning in Lean and introduces the first large-scale Lean4 physics benchmark covering topics from mechanics to modern physics. \n\n- PhysLib provides a modular, SI-based unit system and topic-structured theorems, ensuring dimensional consistency and extendability for accurate physical reasoning.\n\n- Comprehensive experiments show that PhysLib context consistently boosts model performance.  LLMs outperform specialized Lean provers, revealing that current Lean provers, trained for math, struggle with physics tasks.", "weaknesses": "- The paper lacks an explanation of the advantages of PhysLib's modular structure over organizing theorems by specific physics domains.  It also does not clarify how this hierarchical organization aids in retrieval and reasoning.\n- What defines the boundary between mathematical and physical problems, and why do Lean provers, which perform well in mathematics, fail to transfer their capabilities to the physics domain?\n- Would including non-competition problems, such as physics questions from middle school or high school exams, in the experiments provide a more comprehensive comparison?", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Meta-review: Conditions for acceptance have been satisfied.
Decision: Accept (Poster)