LeanBio: claims, grounded and ranked for Lean
Claims distilled from the literature become nanopubs. Each one is grounded to ontology identifiers, typed as a subject–relation–object statement, and given a belief score from its independent evidence. The best-supported claims that have a mathematical form go to a queue, and from there to a Lean 4 statement in the law registry. A person accepts a law; the pipeline never does.
Belief scores
Belief = E × (1 − R), with E from supporting and R from contradicting evidence in INDRA's SimpleScorer form, each source counted once. The parameters are set by hand and not fitted, so treat belief as an order, not a probability. Most claims have only two elicited model opinions, which is why so many share one value.
Records by belief
How a score is made
P_wrong(s) = min(1, syst_s + rand_s ^ n_s) E = 1 - PROD P_wrong (supporting) R = 1 - PROD P_wrong (contradicting) belief = E * (1 - R)
| source class | rand | syst |
|---|---|---|
| pre-registered test | 0.10 | 0.05 |
| thread evidence draft | 0.25 | 0.10 |
| cited literature | 0.30 | 0.10 |
| language-model opinion | 0.45 | 0.25 |
| Lean conflict (against) | 0.20 | 0.10 |
From pipeline/leanbio/belief-params.json. A Lean proof is not counted: it proves a model's consequence, not that organisms obey the model.
Laws in the registry
Laws by status
Statement types
INDRA's molecular types fire only when a gene, protein or chemical is grounded on both sides; the rest are our law types. Typing is regex rules with unmeasured precision.
Grounding coverage
Gilda (INDRA's grounder) reads each claim; MyGene.info, OLS4 and the repo's taxon inventory cover zebrafish genes and taxa that Gilda does not index, and check identifiers that drafts declare. Low-scoring synonym hits are rejected; near-ties are flagged as ambiguous and never resolved automatically.
Mentions found in text
Entities declared by drafts
Not grounded
Ambiguous mentions
The formalization queue
Records with belief ≥ 0.5, a relation that has a mathematical form, no law in the registry yet, and no reviewer decision against them. Theorem-shaped relations come first, then belief. Being on the queue means “worth a look”, not “formalizable”: a reviewer often finds there is nothing to state.
Decisions on the queue
Every queue item a person or agent looked at, including the ones where no correct Lean statement exists.
How to contribute
Propose a LeanBio law
- A sourced nanopub draft or claim in the repo, with resolvable identifiers.
- Grounded entities and a belief at or above 0.5 (node pipeline/leanbio/run.mjs).
- A Lean statement with named hypotheses: no axiom, no sorry, a non-vacuity witness, a scope.
- node lean/registry/propose.mjs law.lean --meta meta.json --write: builds, checks axioms, rejects statement mutants, checks joint consistency.
- node lean/registry/check-exposed.mjs green.
- A person accepts it, by role, in a new lawset.
Full criteria: CONTRIBUTING-LEANBIO.md. Open the PR with the leanbio.md template; CI runs the checks.
Harvest nanopubs and query
Read-only SPARQL on the public Knowledge Pixels query service: node pipeline/leanbio/harvest.mjs --count. A harvested nanopub is a candidate; it enters the pipeline as a claim or draft that cites it.
Agents: MCP tools leanbio_queue, leanbio_ground (text to ontology ids), leanbio_claim (claim to nanopub draft, belief and linked laws), once the hub registers them.
Nothing is ever signed or published from a pull request. The held-out exam clade is excluded everywhere.