What is proven, and what is not

Tier 1, the dimensional layer. Each exported map node is declared as a physics dimension: five rational exponents over length, time, mass, charge, and temperature. Each executable edge becomes a theorem stating that the edge's output dimension equals the product of its input dimensions. The Lean compiler checks every one against physlib (Lean 4.31.0); a file that compiles with zero errors and zero sorrys is the proof.

Tier 2, the operator identities. The map's executable identities are stated as theorems over real numbers and checked against Mathlib. A composition theorem substitutes an upstream identity into a downstream one and proves the chained form equals the flat form; a law theorem states a single identity's formula as a well-typed real equation.

Scope. physlib's Dimension has five bases and no base for amount of substance, electric current, or luminous intensity, so map nodes whose dimension needs a mole, ampere, or candela base are omitted from the export. Extending the dimension system upstream is a later tier. The coverage counts below state exactly how much of the map this leaves in.

Honest limits: a theorem here checks dimensional consistency or an algebraic identity, mechanically. It does not check that a formula is the right physics, that a code implements it faithfully, or that any value attached to the map is accurate. Those live in the evidence and agreement views.

Coverage

Counting from data/lean.json and data/graph.json…

Edge theorems (Tier 1)

One theorem per verified executable edge: the output's dimension equals the product of its inputs' dimensions. Node names link to the quantity on the map; every theorem lives in the generated lean/OpenMaterials.lean.

Operator identities (Tier 2)

Each identity is a theorem over real numbers, checked against Mathlib; the statement below is the generated source, verbatim, from lean/OpenMaterialsIdentities.lean.

Nodes

Every exported map node and its proven dimension, as five exponents in physlib field order (length, time, mass, charge, temperature). Where a node has a counterpart formalized in physlib itself, the crosswalk entry appears under it.

Reproduce this

Every pull request that touches the map or the generators recompiles the full proof against physlib in CI, with warnings promoted to errors, so the badge above is the live state of the claim on this page.

lean/ is a standalone lake package (library OpenMaterials) on toolchain Lean 4.31.0, depending on physlib pinned by rev in lakefile.toml. The files are generated from the live map and re-checked two ways: the Lean compiler proves them, and the Python suite re-derives every dimensional identity so a regression fails fast even without a Lean toolchain. From lean/README.md:

git clone https://github.com/openmaterials-ai/openmaterials-ai.git
cd openmaterials/lean

lake exe cache get   # fetch the mathlib build cache (first build only)
lake build           # compiles every generated module; zero errors, zero sorries

# the Python re-check (no Lean toolchain needed), from the repo root:
pip install -e . && python -m pytest tests/test_physlean_export.py tests/test_lean_tier2.py -q

The generated sources: OpenMaterials.lean (Tier 1 dimensions and edge theorems), OpenMaterialsIdentities.lean (Tier 2 identities), OpenMaterialsDimensions.lean (the seven-base dimensional closure), OpenMaterialsUnits.lean (the units bridge).