mlsanityData to 14 Oct 2026

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

arXiv 2510.26094 ↗First posted 30 Oct 2025cs.AI cs.LGcited by 5

Not on the map. Why?

Abstract (arXiv)

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.

Key facts. Cited by 5 papers in the map (data through 14 Oct 2026). Builds on 33 of its 54 references that are in the map. First posted on arXiv 30 Oct 2025.

Builds on

33 of 54 references.

References · 33

  1. 2021Training Verifiers to Solve Math Word Problemscited by 10,109
  2. 2025DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learningcited by 6,330
  3. 2021Measuring Mathematical Problem Solving With the MATH Datasetcited by 5,371
  4. 2024GPT-4o System Cardcited by 4,588
  5. 2025Gemini 2.5: Pushing the Frontier with Advanced Reasoning, Multimodality, Long Context, and Next Generation Agentic Capabilitiescited by 3,796
  6. 2024MMLU-Pro: A More Robust and Challenging Multi-Task Language Understanding Benchmarkcited by 1,848
  7. 2018CommonsenseQA: A Question Answering Challenge Targeting Commonsense Knowledgecited by 1,822
  8. 2022Challenging BIG-Bench Tasks and Whether Chain-of-Thought Can Solve Themcited by 1,807
  9. 2024OlympiadBench: A Challenging Benchmark for Promoting AGI with Olympiad-Level Bilingual Multimodal Scientific Problemscited by 1,136
  10. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 391
  11. 2025DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decompositioncited by 287
  12. 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 197
21 more
  1. 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 192
  2. 2025Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learningcited by 180
  3. 2025Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correctioncited by 154
  4. 2022Formal Mathematics Statement Curriculum Learningcited by 142
  5. 2019The Lean mathematical librarycited by 134
  6. 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Provingcited by 133
  7. 2024Lean Workbook: A large-scale Lean problem set formalized from natural language math problemscited by 122
  8. 2025BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Provingcited by 84
  9. 2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Provingcited by 79
  10. 2024TheoremLlama: Transforming General-Purpose LLMs into Lean4 Expertscited by 59
  11. 2025PhysReason: A Comprehensive Benchmark towards Physics-Based Reasoningcited by 59
  12. 2025AdaCtrl: Towards Adaptive and Controllable Reasoning via Difficulty-Aware Budgetingcited by 50
  13. 2025UGPhysics: A Comprehensive Benchmark for Undergraduate Physics Reasoning with Large Language Modelscited by 48
  14. 2025MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Provingcited by 24
  15. 2025HiPhO: How Far Are (M)LLMs from Humans in the Latest High School Physics Olympiad Benchmark?cited by 19
  16. 2025Scaling Physical Reasoning with the PHYSICS Datasetcited by 13
  17. 2025MATP-BENCH: Can MLLM Be a Good Automated Theorem Prover for Multimodal Problems?cited by 13
  18. 2025Let's Reason Formally: Natural-Formal Hybrid Reasoning Enhances LLM's Math Capabilitycited by 11
  19. 2024HepLean: Digitalising high energy physicscited by 10
  20. 2022Formalizing Chemical Physics using the Lean Theorem Provercited by 9
  21. 2025Veri-R1: Toward Precise and Faithful Claim Verification via Online Reinforcement Learningcited by 5

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2026: 5.

5 papers.

  1. 2026Code as Agent Harnesscited by 47
  2. 2026RebuttalAgent: Strategic Persuasion in Academic Rebuttal via Theory of Mindcited by 6
  3. 2026PhysProver: Advancing Automatic Theorem Proving for Physicscited by 3
  4. 2026Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectorycited by 1
  5. 2026AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanicscited by 1