Physlib: a community effort to turn physics results into Lean 4 theorems

The project requirement, written as a list of aims

Physlib describes itself as an open-source, community, project to digitalize results from physics into Lean 4, and it states its requirements as a list of shall statements, which is a distinctive way to write a charter.

The first requirement is that the project shall contain results, meaning definitions, theorems, lemmas and calculations, from physics, including quantum information, formalized into the interactive theorem prover Lean 4. The second is that the project shall be organized by physics, so the directory structure follows the subject rather than the logic.

The next three are documentation requirements. Each definition shall carry a physics-based documentation, and each module, meaning a file, shall carry a physics-based documentation. That is a stronger requirement than most formalisation projects make, and it is the one that decides whether a physicist can use the library without reading the Lean source.

The project shall also contain Physics Lean tactics, notation and syntax for physicists, which is the part that makes the output pleasant to read for the intended audience. It shall not be tied to physics axiomizations such as axiomatic QFT, but be flexible enough to accommodate different approaches and starting points, which is a deliberate constraint against the usual failure mode of a formalisation project that picks one philosophy and locks out the others.

The content 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, it shall not be tied to any specific AI model or tool, and it shall be for mainstream physics only.

Three libraries with three different review standards

The repository diagram shows the shape of the effort, with Mathlib upstream and the project itself below it in three columns.

Physlib is the core library, described as physics digitalizations reviewed and curated to a high standard, built for long-term reuse, readability, trust and maintenance.

PhyslibAlpha exists for the rapid development of physics digitalizations, enabled by a lighter review process built to handle large-scale, human- or AI-generated contributions.

QuantumInfo is quantum information theory, currently a distinct codebase with its own conventions and review norms, with work underway to bring it closer to Physlib.

The Alpha layer is the interesting design decision, and the documentation is explicit about its cost. Its review standard is lower than Physlib, which makes it easier to contribute large pull requests, AI-generated content, or formalisations which are not quite perfect. Pull requests for PhyslibAlpha must pass basic linter checks, and must undergo a light one-look review checking three things: whether the content is mainstream physics, whether it looks reasonable in the sense of no axioms and easy to read, and whether it is in the right place within PhyslibAlpha by mirroring its place in Physlib.

And then the sentence that matters for anyone depending on it: because of the lower review bar for PhyslibAlpha, the project cannot promise to maintain contributions when they break, and will simply record when this happens. That is a candid statement of what a fast lane costs, and the reason to keep anything you rely on in the reviewed core.

A separate project, CSLib, is marked as adjacent, with the arrow pointing away from Physlib.

Building the project with lake

Installing Lean 4 is a prerequisite, and the documentation points at the Lean 4 quickstart or at the community get started page.

Installing Physlib itself is a list of steps. You clone the repository, or download it as a zip file, open a terminal at the top level of the corresponding directory, run `lake exe get_cache` to download the cached artifacts from the internet, and then run `lake build`.

The cache step is optional in effect even though it is listed as a step. The documentation says it will speed up the next step drastically, and that you need not worry if it fails because you can still run lake build, it will just be much slower. That is the honest framing of an optimisation step, and it is a common one in Lean projects where the build cache is large.

After the build you open the directory, not a single file, in Visual Studio Code or another Lean compatible code editor. The distinction matters because Lean 4 resolves imports across the project, and opening one file leaves the editor without the project context.

Once set up, `lake build` only recompiles files you have actually changed, plus anything importing them, which is the incremental behaviour that makes the build usable at all.

Two build targets and the merging still in progress

The repository is currently divided into two essentially disjoint halves, Physlib and QuantumInfo. These were two repositories that merged in an effort to create a more cohesive ecosystem for physics in Lean, and there is ongoing effort to integrate them more deeply and share code.

At the moment they offer two separate build targets, Physlib and QuantumInfo, as specified in the lakefile.lean. Both are default targets, so `lake build` builds both. If you only want one, `lake build Physlib` or `lake build QuantumInfo` targets just that one.

The documentation gives two reasons this is useful: if you are working on one part or the other and want to see that all your changes worked, and if you are only interested in having one or the other as a dependency in your project.

That second reason is the one that matters for adoption. The two halves are separate build targets precisely so that a downstream project can depend on Physlib without pulling in QuantumInfo, and the eventual goal is for the split to disappear. A repository that has already merged once and is still mid-integration is a normal state for a project of this kind, and the build target split is the mechanism that keeps it usable in the meantime.

The top-level entries reflect the structure, with a Physlib.lean, PhyslibAlpha.lean and QuantumInfo.lean root file, the corresponding directories, a lean-toolchain file, a lakefile.toml with a lake-manifest.json, a lake-cache.toml, a scripts directory, a docs directory and an AGENTS.md alongside an AI-POLICY.md and a CITATION.cff.

Contributing and the review loop

Physlib is open-source and community run, and contributions are welcome from anyone. The process is that you open a pull-request with your changes and a team of maintainers reviews it and iterates with you on feedback until it can be merged.

There is one instruction about what to include, and it is specific: add references to the References section at the top of the file and add them to the .bib file. That is a small requirement with a large consequence, because a formalised result without a citation to the paper it comes from is a statement nobody can check the meaning of.

If you are unsure where you would like to contribute, the documentation points at four places: the open issues, a todo list on the project website, a Get Involved page, and the quantum information todo page in the docs directory.

And there is a note about where to ask when you are stuck, which is a large collection of people on the Physlib channel of the Lean prover Zulip.

The project also runs a Zulip discussion channel, publishes a TODO list and a statistics page on its website, and links a Gitpod badge marked ready to code, so a contributor can get a working environment without setting up Lean locally first.

Where Physlib is the wrong choice

The first limitation is that formalising physics is slow work. A result that a physicist can derive in an afternoon may take a week to turn into a Lean proof with the right level of documentation, and the project demands that documentation. A group that wants one theorem checked and then discarded is paying for a structure that does not suit them, and the honest answer for a one-off is to use Lean 4 with Mathlib directly, which is what the upstream dependency is for.

The second is the mainstream physics restriction. The project shall be for mainstream physics only, and a review checks whether content is mainstream physics. A result in a speculative or heavily formalised corner of the field may be difficult to place, and the requirement not to be tied to physics axiomizations while covering mainstream physics is a real tension that the maintainers have to resolve case by case.

The third is the dependency on the toolchain. Lean 4 is a moving target, the badge pins the current version at 4.35.0, and Mathlib upstream is a large project with its own release cycle. A downstream project that depends on Physlib inherits that cadence, and the ongoing merge of the two halves is exactly the kind of structural change that occasionally breaks a dependency for a release.

The comparison with the alternatives is not really about formalisation projects, since there are few. It is about whether you want a checked statement or a trusted derivation. Lean gives you the former. A physicist reading a paper can follow the argument and see the intuition; a Lean proof tells you the statement is derivable from the axioms but not why it is true. For a project whose value is in sharing physics with the formal community, that trade is worth making, and for one that needs a working derivation, it is not.

Editorial conclusion

Physlib fits a mathematical physicist who wants to check a derivation in Lean 4, or a group building a shared formal vocabulary for a subfield of physics, and who is prepared to write documentation in terms a physicist would recognise. It does not fit a group that wants a quick formalisation of one paper, or a physicist who wants a working derivation rather than a checked statement. Before contributing, read the requirement that every definition and every module carries physics-based documentation, and note that the Alpha library explicitly does not promise to maintain contributions when they break, so anything you rely on should live in the reviewed core.

Frequently asked questions

Official sources

1. Issues
2. leanprover-community/physlib on GitHub
3. License: Apache-2.0
4. Project website
5. README