Digitalizing Physics
in Lean 4
An open-source, community project to digitalize results from physics into Lean 4.
(formerly PhysLean & Lean-QuantumInfo)
About Lean
A theorem prover that guarantees correctness.
Lean is an interactive theorem prover where you write mathematical definitions, theorems, and proofs — and the system verifies correctness using type theory, with no gaps or hand-waving.
Increasingly used by AI labs and mathematicians, Lean is now making its way into physics through Physlib.
theorem wicks_theorem : (φs : List 𝓕.FieldOp) → 𝓣(ofFieldOpList φs) =
∑ (φsΛ : WickContraction φs.length), φsΛ.wickTerm
| [] => by
rw [timeOrder_ofFieldOpList_nil]
simp only [map_one, List.length_nil, Algebra.smul_mul_assoc]
rw [sum_WickContraction_nil]
simp only [wickTerm_empty_nil]
| φ :: φs => byMission
Create a library of digitalized physics results in Lean 4, useful to the broad physics community.
Comprehensive repository of fundamental physics definitions, theorems, and calculations.
Interface between experimental data, simulations, and formal theoretical frameworks.
Extensive, physics-focused documentation to support adoption.
Accessible to physicists at all levels — especially those new to formal methods.
An intuitive setup that aligns with how physicists think and work.
A large, active team with the potential for high-energy-physics-style collaborations.
Values
Built on principles.
Welcoming
Contributors of all academic backgrounds and experience levels are valued, supported, and empowered to make meaningful contributions.
Open & Transparent
Physlib is openly accessible, freely available, and developed with full transparency for the benefit of both communities.
Accessible & Practical
Designed to be intuitive and well-documented, directly useful to physicists regardless of their familiarity with formal methods.
Beneficiaries
For physicists and
formal-methods researchers.
Academic
Researchers & Students
- —Students in physics, mathematics, or computer science
- —Research physicists formalizing theoretical results
- —AI researchers verifying mathematical theorems
- —Educators creating novel teaching approaches
Industrial
Companies & Labs
- —Companies leveraging AI for formal reasoning at scale
- —Organizations proving correctness of physical processes
- —Teams building verified simulation frameworks
- —Enterprises ensuring theoretical soundness of models
Impact
Why formalize physics?
Make it easier to find and reference existing results across physics.
Enable AI and machine learning to automate discovery of new results.
Check papers and results for mathematical correctness automatically.
Create new avenues through which physics can be taught and explored.
Open new ways to interface between theory and computer programs.
Build a shared, standardized foundation for the whole physics community.
Join Physlib
Help build the future
of physics.
Whether you're a physicist, a Lean developer, or just curious — there's a place for you in Physlib.
Read the paper: arXiv:2405.08863