verified-nondim

Nondimensionalize ODE models automatically, and let Lean 4 check the result.

pip install verified-nondim

Three parameters, one that matters

from nondim import Model, nondimensionalize

sir = Model.from_strings(
    "SIR",
    equations={"S": "-beta*S*I", "I": "beta*S*I - gamma*I"},
    params="beta gamma N",
    same_units=[("S", "N"), ("I", "N")],  # S and I are counted in the same units as N
)
reduced = nondimensionalize(sir, ["gamma", "N"], names={"t": "tau", "S": "X", "I": "Y", "beta": "R0"})
print(reduced.summary())

    tau = gamma*t
    X = S/N
    Y = I/N
    R0 = N*beta/gamma
  reduced system:
    dX/dtau = -R0*X*Y
    dY/dtau = Y*(R0*X - 1)
  parameters 3 -> 1: R0

The tool reads the equations, finds every change of units they allow, and uses those to set parameters to 1. The number it can remove is a matrix rank, so it is the best possible.

Ask for what you want

from nondim import solve

print(solve(sir, eliminate_at_least=2, keep=["beta"]))
print(solve(sir, eliminate_at_least=3))
print(solve(sir, want={"x": "beta*N"}))

SAT: normalize ['gamma', 'N'] (removes 2 >= 2).
UNSAT: only 2 independent scaling direction(s) act on ['beta', 'gamma', 'N'], so at most 2 of them can be removed (asked for 3).
UNSAT: x = N*beta is not dimensionless: scaling #2 multiplies it by lambda^1.

Ask what data can tell you

from nondim import analyze_identifiability

observed = Model.from_strings(
    "SIR_reported",
    equations={"S": "-beta*S*I", "I": "beta*S*I - gamma*I"},
    params="beta gamma rho",
    outputs={"y": "rho*I"},  # we only see a fraction rho of cases
)
print(analyze_identifiability(observed).summary())

  NOT identifiable (moved by a scaling): ['beta', 'rho']
  parameter groups the data can see:     ['gamma', 'rho/beta']

Let Lean check it

nondim init-lean proofs        # a Lean 4 + Mathlib project with the certificates
cd proofs && lake exe cache get && lake build

Every claim above becomes a theorem that Lean re-proves. From the SIR certificate:

theorem symmetries : Amat * Kmat = 0 := by decide +kernel
theorem rank_Apar : Apar.rank = 2 := by unfold Apar; eval_rank
theorem constraint2_unsat : 3 > Acand2.rank := by have h := constraint2_rank; omega

The Python code is never trusted: if it were wrong, the Lean build would fail.

More

• nondim tour walks through all of this in seven steps; nondim list shows the built-in models.
• Guide · the math by hand · design decisions and sources · testing · examples
• Scope: right-hand sides built from products, quotients and sums of powers (no exp or log). Results are verified relative to the equations and unit links you supply.

MIT license.