PaperlayerView exact revision on arXiv

Source-linked AI summary

Lean4Physics: Comprehensive Reasoning Framework for College-level Physics in Lean4

Yuxin Li, Minghao Liu, Ruida Wang, Wenzhao Ji, Zhitao He, Rui Pan, Junming Huang, Tong Zhang, Yi R. Fung

arXiv:2510.26094v1cs.AIcs.LG

TL;DR

Formal reasoning studies have largely focused on mathematics, while physics lacks comprehensive foundational support and thorough evaluation of formal reasoning capabilities. Lean4PHYS combines PhysLib with LeanPhysBench, a benchmark of formalized college-level physics problems. The authors report suboptimal model performance, with open-source expert provers not outperforming closed-source general models, and an average performance improvement of 11.75% with PhysLib.

  • Problem

    Formal-reasoning studies largely focus on mathematics, while physics lacks comprehensive foundational support and thorough evaluation of models’ formal capabilities.

    Source: §1 · p. 1, §4.2 · p. 9

  • Method

    Lean4PHYS combines PhysLib, a physics foundation library, with LeanPhysBench, a benchmark of formalized college-level physics problems for evaluating LLM reasoning.

    Source: §1 · pp. 2–3

  • Results

    Current models show suboptimal Lean4 physics reasoning: the best expert prover achieves 15.00% and the large general model 39.50%, while PhysLib improves performance by 11.75% on average.

    Source: §1 · p. 3, §5 · p. 9

  • Takeaways & Limitations

    Lean4PHYS provides an extensible foundation library and a benchmark for evaluating formal physics reasoning, where open-source expert provers do not outperform closed-source general models.

    Source: §5 · p. 9

Abstract

from arXiv · show

We present **Lean4PHYS**, a comprehensive reasoning framework for college-level physics problems in Lean4. **Lean4PHYS** includes *LeanPhysBench*, a college-level benchmark for formal physics reasoning in Lean4, which contains 200 hand-crafted and peer-reviewed statements derived from university textbooks and physics competition problems. To establish a solid foundation for formal reasoning in physics, we also introduce *PhysLib*, a community-driven repository containing fundamental unit systems and theorems essential for formal physics reasoning. Based on the benchmark and Lean4 repository we composed in **Lean4PHYS**, we report baseline results using major expert Math Lean4 provers and state-of-the-art closed-source models, with the best performance of DeepSeek-Prover-V2-7B achieving only 16% and Claude-Sonnet-4 achieving 35%. We also conduct a detailed analysis showing that our *PhysLib* can achieve an average improvement of 11.75% in model performance. This demonstrates the challenging nature of our *LeanPhysBench* and the effectiveness of *PhysLib*. To the best of our knowledge, this is the first study to provide a physics benchmark in Lean4.

1 INTRODUCTION

Formal logical systems can verify reasoning steps and final answers, but physics remains understudied in Lean4 formal reasoning. Lean4PHYS addresses this gap with a foundation library and benchmark for college-level physics.

1 INTRODUCTION

  • Formal-reasoning studies largely focus on mathematics, leaving physics without comprehensive foundational support or thorough evaluation of models’ formal capabilities.Physics formalization requires unit systems and domain-specific theorems, while existing foundations are absent or fragmented.Source: §1 · p. 2
  • PhysLib provides a foundation for Lean4 physics reasoning, including unit systems, mathematical structures, dimensional transformations, and an extendable collection of formalized physics theorems.The library builds on Tao’s dedicated UnitSystem.Source: §1 · p. 2
  • LeanPhysBench contains 200 manually crafted, peer-reviewed Lean4 theorems spanning competition and college-textbook physics problems.Its construction transforms natural-language problems into verifiable Lean4 statements by extracting conditions and physical laws and defining proof targets.Source: §1 · pp. 2–3
  • 15.00% for the best expert prover and 39.50% for the large general model; integrating PhysLib improves model performance by 11.75% on average.The authors report these results as evidence of suboptimal formal-physics reasoning performance and PhysLib's effectiveness.Source: §1 · p. 3
  • Lean4PHYS extends LLM-based formal reasoning beyond mathematics to a more general domain, with the stated aim of formalizing progressively more subjects.The authors describe LeanPhysBench as the first benchmark for evaluating LLMs’ formal physics reasoning capabilities.Source: §1 · p. 3

2 THE LEAN4PHYS FRAMEWORK

Lean4PHYS combines PhysLib, a foundational library for formal physics, with LeanPhysBench, a benchmark for evaluating Lean4 physics reasoning. The framework builds a physics unit system, organizes topic theorems, and formalizes problems into verifiable Lean4 statements.

2.1 PHYSLIB

  • PhysLib provides an extensible foundation library for units, fields, and theorems, while LeanPhysBench evaluates LLMs’ formal physics reasoning.The framework’s core idea is to provide a foundation and then evaluate formal physics reasoning.Source: §2.1 · p. 3, §2 · p. 3

2.1.1 FOUNDATION OF PHYSICS: UNIT SYSTEM

  • The physics unit system extends Mathlib4 and Lean4 UnitSystem with seven basic units and mathematical structures needed for physics problems and proofs.The work also defines conversions between physics and mathematical quantities and dimension casts that preserve mathematical propriety.Source: §2.1.1 · pp. 3–4

2.1.2 TOPIC-BASED THEOREM DEVELOPMENT

  • PhysLib organizes topic-specific units, rules, and theorems across mechanics, waves and acoustics, thermodynamics, electromagnetism, optics, and modern physics.Mechanics is implemented in detail as an example, with other topics set up for development.Source: §2.1.2 · p. 4

2.1.3 COMMUNITY-DRIVEN AND EXTENSIBILITY

  • PhysLib uses a three-layer structure of foundation units, topic-specific units, and topic-specific theorems, designed for community extension.The current repository’s mechanics implementation serves as an example, and the layered design is presented as applicable beyond physics and to other proving systems based on the same logic.Source: §2.1.3 · p. 4

2.2.1 DATA COLLECTION & PREPROCESSING

  • LeanPhysBench addresses the lack of a benchmark for evaluating LLMs’ Lean4 physics reasoning, collecting college-textbook and Olympiad problems with distinct reasoning emphases.College problems cover broader concepts and cross-model reasoning; Olympiad problems emphasize multi-step reasoning within a field. Figure 2 illustrates examples at different difficulty levels.Source: §2.2 · p. 4, §2.2.1 · p. 4, Figure 2 · p. 5

2.2.2 FORMALIZATION PIPELINE

  • The formalization pipeline aligns question-answering problems with proof statements, extracts laws and conditions, defines targets, then codes and verifies Lean4 theorems.Experts in physics and Lean check theorem completeness after code compilation.Source: §2.2.2 · p. 5
  • Competition problems are split by PhysLib theorem use: easy problems rely more on Mathlib4, while hard problems require more PhysLib theorems and definitions.The split is intended to assess whether models can use out-of-distribution theorems supplied in context.Source: §2.2.2 · p. 6

2.2.3 BENCHMARK STATISTICS

  • 200 Lean4 statements comprise 104 college-level problems and 96 competition problems, including 62 easy and 34 hard competition problems.Figure 3 shows distributions by difficulty level and topic.Source: §2.2.3 · p. 6

3 EXPERIMENT

Experiments evaluate models proving LeanPhysBench statements with and without PhysLib in context. Overall performance is low, while results vary by model type and problem difficulty, and case studies illustrate differences in library use and reasoning behavior.

3.1 EXPERIMENT SETUP

  • Models receive natural-language and Lean4 statements and must produce Lean4 proofs; experiments compare eight LLMs with and without PhysLib in context.The study includes closed- and open-source general models as well as expert Lean4 provers, and generally allows long chain-of-thought reasoning.Source: §3.1 · p. 7

3.2 MAIN RESULT

  • 40.50% accuracy across the entire dataset is reported for large general models, while leading open-source models achieve at most 14.50%.With PhysLib in context, Gemini achieves higher overall accuracy, while smaller models show less significant enhancement. Lean expert provers do not outperform closed-source general models as they do in math; on competition-hard problems, experts outperform closed-source models, which achieve zero performance. PhysLib’s gains are attributed to better unit-system understanding and theorem selection, and access to it is associated with use of tactics such as simp and norm_num.Source: §3.2 · p. 7

3.3 PROBLEM FORMAT STUDY

  • College-level problems mainly involve numeric computations across varied physical quantities and depend on PhysLib’s unit system for dimensional consistency.Models weaker at in-context learning perform poorly when they cannot infer unfamiliar syntax or unit-handling rules.Source: §3.3 · p. 8
  • Easy competition problems typically require formula derivations within two steps and often use Mathlib tactics, favoring models familiar with Lean mathematics.The passage reports these models can outperform closed-source large models even without PhysLib.Source: §3.3 · p. 8
  • Hard competition problems combine symbolic reasoning, quantifiers, functional reasoning, unit casts, and sometimes calculus, requiring decomposition and multiple proof strategies.The paper attributes the low pass rate at this level to these combined demands.Source: §3.3 · p. 8

3.4 CASE STUDY

  • A theorem solved by Gemini with and without PhysLib shows library context shifting proofs from Mathlib-only toward PhysLib operations and explanatory comments.The authors interpret this as PhysLib providing a wider toolbox.Source: §3.4 · p. 8
  • Goedel-Prover-V2-8B solved one problem through following natural-language intermediate steps and multiple try-tactic trials learned in Lean math training.The case study presents this as limited transfer of expert-prover mathematical reasoning to formal physics.Source: §3.4 · p. 8
  • In thermodynamics, Gemini proved 22 theorems compared with six for DeepSeek-Prover-V2, and its proof in a shared example was cleaner and more straightforward.The authors suggest prolonged deliberation may lead expert models to overthink in fields underrepresented in training.Source: §3.4 · p. 8

4 RELATED WORK

Related work spans formal reasoning benchmarks and expert provers in Lean, emerging Lean projects in other sciences, and natural-language physics datasets. The paper situates its contribution at the intersection of formal physics reasoning and evaluation.

4.1 FORMAL REASONING

  • Lean research includes formal reasoning benchmarks from competition-level to college-level problems, large training datasets, and expert provers developed for mathematical reasoning.Examples include MiniF2F, ProofNet, PutnamBench, and MATPBench, alongside several expert prover families.Source: §4.1 · pp. 8–9

4.2 LEAN IN SUBJECTS BEYOND MATHEMATICS

  • Lean is expanding into fields including chemical physics, molecular simulation, and electrical engineering, but cited projects remain small-scale and lack standardized evaluation.The transfer of Lean expert provers’ mathematical reasoning to other subjects such as physics remains to be examined.Source: §4.2 · p. 9

4.3 PHYSICS DATASETS

  • Natural-language physics resources include model-reasoning benchmarks, textbook-style datasets, competition collections, and automatically generated questions.The cited datasets range from course-level collections to Olympiad and multi-step, image-understanding resources.Source: §4.3 · p. 9

5 CONCLUSION

The conclusion presents Lean4PHYS as a framework for formal physics reasoning and reports both benchmark results and an average performance increase with PhysLib.

5 CONCLUSION

  • Lean4PHYS combines community-driven PhysLib with LeanPhysBench, and experiments report an 11.75% average performance increase when PhysLib is in context.The authors report suboptimal current performance and limited transfer from mathematical reasoning, and frame the work as a general principle for formalizing physics and other natural sciences in verifiable systems.Source: §5 · p. 9

A DATA SOURCES

The questions draw on university-textbook concepts, UGPhysics, and physics competition materials, with textbook questions rephrased rather than copied verbatim.

A DATA SOURCES

  • Textbook-level questions adapt concepts from Young and Freedman and UGPhysics, while Olympiad-Easy questions derive from intermediate competition-solution steps.Olympiad-Hard questions draw on problem-solving ideas from a physics Olympiad practice book; textbook questions are rephrased to respect copyright.Source: A DATA SOURCES · p. 14

B IMPLEMENTATION DETAIL

The LLM rollout uses a specified generation configuration and open-source hardware setup.

B IMPLEMENTATION DETAIL

C LLM PROMPT TEMPLATES

The prompts ask models to learn the new library and unit system, then produce a proof plan and Lean4 code.

C LLM PROMPT TEMPLATES

D.1 FORMAT STUDY

Figure 4 samples three problem types, ranging from numerical formula use to symbolic, multistep derivation. Their differing demands include unit consistency, algebraic substitution, and function operations.

D.1 FORMAT STUDY

  • The college-level point-charge force problem primarily tests numerical calculation with Coulomb’s law, while requiring consistent units across physical quantities.It exemplifies formula application and basic numerical reasoning with unit handling.Source: §D.1 · p. 16
  • Competition-Easy capacitor problems require one or two substitutions into C = q/V, combining numbers and symbols through algebraic operations.These transitional derivation problems have slightly greater logical-reasoning demands than college-level examples.Source: §D.1 · p. 16
  • Competition-Hard pulley problems require multistep derivations involving integration or logarithmic relationships and symbolic dependencies among physical quantities.They are described as highly difficult symbolic-reasoning problems requiring function operations and advanced physical reasoning.Source: §D.1 · p. 16
  • Figure 4 presents three sampled questions alongside their Lean formalizations and verified proofs.Source: Figure 4 · p. 17

D.2 CASE STUDY

The case studies contrast proof styles across models and show how PhysLib changes Gemini’s proof path. Goedel-Prover also applies Lean mathematics strategies to physics proofs, including decomposition, intermediate checks, and combining subgoals.

D.2 CASE STUDY

  • Goedel-Prover decomposes the friction problem into independently provable subgoals, checks intermediate arithmetic and types, and retries lightweight tactics for auxiliary steps.The example verifies values such as Scalar.val f s max = 230 and Scalar.val n = 500 before calculating µs = 0.46.Source: §D.2 · p. 18
  • After proving each subgoal, Goedel-Prover combines them into the theorem with a logical constructor, a mathematical Lean strategy also applied to physics formalization.Source: §D.2 · p. 18
  • For the analyzed thermodynamics theorem, DeepSeek-Prover-V2 explicitly builds intermediate substitutions and simplifications, while Gemini-2.5-pro applies assumptions together and simplifies directly.DeepSeek introduces auxiliary steps; Gemini reduces the target directly to a numerical equation.Source: §D.2 · p. 18
  • DeepSeek-Prover-V2 uses over twenty nested operations, while Gemini-2.5-pro completes the thermodynamics proof through two main strategies.The analysis attributes Gemini’s shorter proof to higher-level abstraction that reduces unnecessary complex calculations.Source: §D.2 · pp. 18–19
  • Figure 5 contrasts Gemini’s proof of the same mechanics problem with and without PhysLib; the library version uses Scalar.val inj to expose real-number algebra.Without PhysLib, the proof relies on assumptions and general Mathlib tactics; with it, the proof is more structured and uses simplification and ring tactics.Source: §D.2 · p. 18, Figure 5 · p. 19
  • Figures 7 and 8 present a natural-language problem and its Lean4 formalization and proof, a problem solved exclusively by Goedel-Prover.Source: Figure 7 · p. 22, Figure 8 · p. 23

Related papers

Loading 2510.26094v1…