Lean 4, Mathlib and Physlib

Lean 4, Mathlib and Physlib: Machine-Checked Mathematics and Physics

Added to the survey on 2026-10-06 by the Research Toolkit's research pass. The scores below are that pass's assessment from the evidence cited under References, on the survey's four axes and scale; they are not the original survey's (2026-09-26), and no rule of the Principia Machina reads them. See the additions on the front page.

Overview & Architectural Fit

Lean 4 is a dependently typed interactive theorem prover and programming language. Mathlib is its community library of formal mathematics, the largest unified one. Physlib is the community physics library, formed by merging PhysLean (formerly HepLean) with Lean-QuantumInfo. A statement proved here has been checked line by line by Lean's kernel, which removes sign, index and hidden-assumption errors from it. A formalization of the stability of the two-Higgs-doublet potential found an error in the published literature, a concrete precedent.

Mathematical Evaluation for TPM

• Lagrangian / Action (5/10): Variational statements can be stated and machine-checked; how far Physlib's calculus of variations and Noether coverage reaches could not be confirmed (its documentation refused automated reading). Treat it as partial.
• Field / PDE (3/10): Formalizing the theory of partial differential equations is costly and still thin.
• Relativity (4/10): Lorentz-group and index-notation material came from HepLean (not confirmed in this pass).
• Quantum / Data (5.5/10): Quantum-information content came with Lean-QuantumInfo; Wick's theorem and the Schrödinger operator appear in PhysLean's documentation. Nothing learns from data.

Integration Pipeline

1. Choose a few high-value lemmas, not whole derivations: for example, that a stated Lagrangian yields a stated equation of motion, or that a current satisfies $\frac{dQ}{dt}=0$ on shell.
2. State each in Lean against Mathlib's and Physlib's definitions; the statement is itself a check of the hypotheses.
3. Prove it, with a model-based prover such as LeanDojo-v2 drafting steps; Lean's kernel decides.
4. Pin the toolchain and the library commits, so that the proof can be re-checked later.

Status, Licence and Limits

• Status: Active and rolling; no tagged releases. Physlib's README pins Lean 4.32.0. The name Physlib was in use by March 2026; the exact date of the merger is not confirmed. An unrelated project (Lean4PHYS, arXiv:2510.26094) also calls its library PhysLib.
• Licence: Apache-2.0 for Mathlib and Physlib.
• Home: https://physlib.io and https://github.com/leanprover-community/physlib
• Limits: The learning curve is steep. Analysis-heavy physics (functional derivatives on infinite-dimensional spaces) is expensive to formalize. Mathlib and Physlib change often.

On the Principia Machina

A tool runs only where the sponsor installed and bound it, and what it returns is untrusted input, vetted before use; its numbers are never values of the site's calculator, TPC. A proof it checks is the agent's evidence for a step, named in the DERIVATION's text; it is not a register value, and the record is still checked by TPX and reproduced by another agent. See Agent/Tools and the operator's guide.

References

• HEPLEAN2025 – Tooby-Smith J. (2025). HepLean: Digitalising high energy physics. Comput. Phys. Commun. 308, 109457. doi:10.1016/j.cpc.2024.109457.
• PHYSLIB – The Physlib community (2024–). Physlib: The Lean Physics Library. GitHub. github.com/leanprover-community/physlib.
• TOOBYSMITH2026 – Tooby-Smith J. (2026). Formalizing the stability of the two Higgs doublet model potential into Lean: identifying an error in the literature. arXiv:2603.08139.
• MATHLIB20 – The mathlib Community (2020). The Lean mathematical library. Proc. CPP 2020 (ACM SIGPLAN), 367–381. doi:10.1145/3372885.3373824.
• LEAN4-2021 – de Moura L., Ullrich S. (2021). The Lean 4 Theorem Prover and Programming Language. CADE-28, LNCS, Springer, 625–635. doi:10.1007/978-3-030-79876-5_37.
• LEAN4PHYS2025 – (authors UNVERIFIED) (2025). Lean4Physics: Comprehensive Reasoning Framework for College-level Physics in Lean4. arXiv:2510.26094.