Lean

What is proven, and what is not

A formula counts as proven when a compiled bridge states and proves something about it: that the catalog formula equals a quantity of an actual Physlib model under stated conditions, together with the model's limits, signs and witnesses. Where Physlib has no model, as for elastic solids, a local proof over Mathlib states the formula's properties directly; these are counted apart from the results that cite Physlib declarations. The bridge page lists every such theorem, its conditions and its build record.

A closed-form formula is not restated as a theorem. Writing Y = N/D as a hypothesis and concluding Y*D = N, or substituting one definition into another and normalizing, certifies nothing about the physics, so the package contains no such statements. The roadmap marks these formulas as definitions. A theorem about one must state a property, such as a limit, a bound or a reduction to another model.

Each node's dimension is a Physlib Dimension ISQDimensionBase definition over mass, length, time, temperature, amount, current and luminous intensity. These are declarations, not theorems. Nodes with an opaque dimension, such as a potential or a crystal structure, have none.

Limits: a theorem holds for the model and conditions it states. It does not show that a code implements the formula correctly, that a numerical producer converged, or that a value on the map is accurate. The agreement page carries the evidence for those questions.

Coverage

Operator formulas with a compiled proof

·

of which citing Physlib declarations

·

of which local proofs over Mathlib

·

Node dimensions declared

·

Physlib revision

·

Lean toolchain

·

Map version

·

Node dimensions

Every encoded field of every map node, with its dimension in ISQ base symbols (M, L, T, Θ, N, I, J) and its declaration in the generated lean/bridge/OMAIPhyslibDimensions.lean. Node names link to the quantity on the map.

Reproduce this

Every pull request that touches the bridge, its bindings or its generators rebuilds the package with warnings promoted to errors and checks every binding against the build; each run is public. The commands below are from lean/bridge/README.md.

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

lake exe cache get   # fetch the Mathlib build cache (first build only)
lake build --wfail   # every module; zero errors, zero warnings, no sorry

# check every binding against the build, from the repo root:
cd ../.. && pip install -e . && python -m omai.formula_bindings --check \
  --physlib-path lean/bridge/.lake/packages/physlib --lean-package lean/bridge