🔗

Does a research decision follow the rules and measurements recorded before it? Slean helps someone preparing or reviewing a case check that consistency and trace each part of the decision.

Here, a case is a JSON file with the question, frozen protocol, observations, a decision, and an event journal. This manual's example is entirely invented; you can understand it without installing Lean.

Read the result in one minute

• Rule fixed before measurement: promote only if synthetic_delta is strictly greater than 0.001 ratio, with cost no higher than 10.00 cpu_s.

• What was recorded: an observation of 0.002 ratio and a cost of 2.50 cpu_s.

• What Slean checks: the observation has the right metric and unit, follows the rule, and precedes the assessment; 0.002 > 0.001 and cost stays below the cap.

• What the case declares: assessment pass, then decision promote. Slean checks that this chain is consistent. It does not make the author's decision.

If the observation's unit changes, Slean reports metric_unit at event-4. If the measurement is missing, its value is null and the decision is defer: missing data is not zero. The checked case shows the two useful commands; read the decision explains the chain and its limits; AND and OR gates add the recorded links in schema 0.3.

Slean checks case shape, references, order, and local rules. It does not run the experiment, authenticate the sensor, or prove that a measurement is true.

Development preview · schema 0.3.0 · Lean 4.28.0. No tag is selected for this build.

Try it in a local checkout

If you have repository access and Lean installed, run from its root:

lake build
lake exe slean validate examples/valid.json

The second command prints exactly:

{"case_id":"synthetic-decision-1","events":10,"ok":true}

ok: true means the case passes the checks Slean supports. It does not certify the source data or the truth of the conclusion.