An open-source, community, project to digitalize results from physics into Lean 4

Requirements of the project

🎯 The project shall contain results (definitions, theorems, lemmas and calculations) from physics formalized (or digitalized) into the interactive theorem prover Lean 4.

🎯 The project shall be organized by physics.

🎯 Each definition in the project shall carry a physics-based documentation.

🎯 Each module (file) in the project shall carry a physics-based documentation.

🎯 The project shall contain Physics Lean tactics, notation and syntax for physicists.

🎯 The project shall not be tied to physics axiomizations (e.g. axiomatic QFT), but rather lexiable enough to accommodate different approaches and starting points.

🎯 The content of the project shall be carefully reviewed and curated, to ensure reusability, readability and fit.

🎯 The project shall be completely open-source, community run and independent from any company or organization.

🎯 The project shall not be tied to any specific AI model or tool.

🎯 The project shall be for main-stream physics only.

How to get involved

See the Get Involved for more details. Some suggestions:

📣 write informal results - no need to learn Lean for this - see the Getting Started page for more details,

📣 tackle a TODO item,

📣 or, start formalizing an area that you find interesting.

Feel free to come to the PhysLean zulip to ask questions and advice.

Note

When making contributing to PhysLean it is much better to do it with small steps. This makes it easier for us to review, and allows you to get feedback sooner.

Places in the project to start

Good places to start an exploration of the project.

• 🗂️ 💻 Maxwell's equations in electromagnetism.
• 🗂️ 💻 Quantum Harmonic Oscillator in quantum mechanics.
• 🗂️ 💻 The two state canonical ensemble in statistical mechanics.
• 🗂️ 💻 The tight-binding model in condensed matter physics
• 🗂️ 💻 The twin paradox in special relativity.
• 🗂️ 💻 The two-Higgs doublet model in particle physics
• 🗂️ 💻 Wick's theorem in quantum field theory.

Associated media and publications

• 📄 Joseph Tooby-Smith, HepLean: Digitalising high energy physics, Computer Physics Communications, Volume 308, 2025, 109457, ISSN 0010-4655, https://doi.org/10.1016/j.cpc.2024.109457. [arXiv:2405.08863]
• 📄 Joseph Tooby-Smith, Formalization of physics index notation in Lean 4, arXiv:2411.07667
• 📄 Joseph Tooby-Smith, Digitalizing Wick's Theorem, arXiv:2505.07939
• 🎥 Lean Together 2025: Joseph Tooby-Smith, Physics and Lean
• 🎥 Seminar recording of "HepLean: Lean and high energy physics" by J. Tooby-Smith

Papers referencing PhysLean

• Hu, Jiewen, Thomas Zhu, and Sean Welleck. "miniCTX: Neural Theorem Proving with (Long-) Contexts." arXiv preprint arXiv:2408.03350 (2024). Project page

How PhysLean (then called HepLean) was used: Theorems from the space-time files of HepLean were included in a data set used to evaluate the ability of models to prove theorems from real-world repositories, which requires working with definitions, theorems, and other context not seen in training.

Contributing

We would love to have you involved! See the Get Involved page to see how you can get involved. Any contributions are welcome! If you have any questions or want permission permission to create a pull-request for this repository contact Joseph Tooby-Smith on the Lean Zulip, or email.

Installation

If you want to play around with PhysLean, but do not want to download Lean, then you can use GitPod.

Installing Lean 4

Installation instructions for Lean 4 can be found:

• https://lean-lang.org/lean4/doc/quickstart.html

or

• https://leanprover-community.github.io/get_started.html

Installing PhysLean

• Clone this repository (or download the repository as a Zip file)
• Open a terminal at the top-level in the corresponding directory.
• Run lake exe cache get. The command lake should have been installed when you installed Lean.
• Run lake build.
• Open the directory (not a single file) in Visual Studio Code (or another Lean compatible code editor).